proposition: Proposition ump_limit_construct_proper (a z : C) (H : IsALimit F z) : Proper (equiv ==> equiv) (ump_limit_construct a z H).
proof: Proof. repeat(intro). unfold ump_limit_construct. apply uniqueness. simpl. intro j. set (k := (unique_property (ump_limit {| vertex_obj := a ; coneFrom := y |}))). destruct x, y; simpl in X. simpl in *; rewrite X; apply k. Qed.
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.Instance.Sets Category.Structure.UniversalProperty Category.Structure.Cone Category.Structure.Limit Category.Functor.Hom.Yoneda