Lemma ff_es_homtype_property (FFF : fully_faithful F) (FES : essentially_surjective F) (P : UU → hProp) (prop : ∏ a b : ob C, P (C⟦a, b⟧)) : (∏ a b : ob D, P (D⟦a, b⟧)). Proof. intros a b. apply (squash_to_prop (ff_es_homtype_weq FFF FES a b)); [apply propproperty|]; intros H. use transportf. - exact (P (C⟦(pr1 H), (pr1 (pr2 H))⟧)). - apply maponpaths. apply weqtopaths. exact (pr2 (pr2 H)). - apply prop. 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.