proposition: Corollary equivalence_homtype_property (E : adj_equivalence_of_cats F) (P : UU → hProp) (prop : ∏ a b : ob C, P (C⟦a, b⟧)) : (∏ a b : ob D, P (D⟦a, b⟧)).
proof: Proof. apply ff_es_homtype_property. - apply fully_faithful_from_equivalence; assumption. - apply functor_from_equivalence_is_essentially_surjective; assumption. - assumption. 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