proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core