Lemma ff_es_homtype_weq (FFF : fully_faithful F) (FES : essentially_surjective F) : (∏ d d' : ob D, ∥ ∑ c c' : ob C, C⟦c, c'⟧ ≃ D⟦d, d'⟧ ∥). Proof. intros d d'. apply (squash_to_prop (FES d)); [apply isapropishinh|]; intros c. apply (squash_to_prop (FES d')); [apply isapropishinh|]; intros c'. apply hinhpr. exists (pr1 c), (pr1 c'). intermediate_weq (D ⟦ F (pr1 c), F (pr1 c') ⟧). - apply weq_from_fully_faithful; assumption. - intermediate_weq (D ⟦ F (pr1 c), d' ⟧). + eapply make_weq. apply z_iso_comp_left_isweq. Unshelve. exact (pr2 c'). + eapply make_weq. apply z_iso_comp_right_weq. Unshelve. exact (z_iso_inv_from_is_z_iso (pr1 (pr2 c)) (pr2 (pr2 c))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core.