Definition is_weak_equiv {C D : category} (H : functor C D) : UU := essentially_surjective H × fully_faithful H.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecompEquivalence.