proposition: Proposition ump_limit_construct_recover (w z : C) (H : IsALimit F z) (m : obj[J]) (a : ACone w F) : vertex_map limit_acone m ∘ (ump_limit_construct w z _ a) ≈ vertex_map a m.
proof: Proof. unfold ump_limit_construct. simpl. exact (unique_property (ump_limit {| vertex_obj := w; coneFrom :=a |} ) _). 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