proposition: Proposition univ_property_respects_iso (c d : C) (iso : c ≅ d) : P c -> P d.
proof: Proof. Proof using eqP H. intro t. rapply (from (repr_equivalence d)). apply (Equivalence_Transitive (fobj[C] d) (fobj[C] c)). - exact (fobj_iso _ _ _ (iso_sym (Isomorphism_Opposite iso))). - apply (to (repr_equivalence c)). exact t. Defined.
imports: Category.Lib Category.Lib.Tactics2 Category.Theory.Category Category.Theory.Isomorphism Category.Construction.Opposite Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Hom Category.Functor.Hom.Yoneda Category.Instance.Sets Category.Construction.Groupoid