proposition: Proposition ump_limit_construct_recover' (q w z : C) (H : IsALimit F z) (m : obj[J]) (a : ACone w F) (f : q ~> w) : vertex_map limit_acone m ∘ (ump_limit_construct w z _ a ∘ f) ≈ vertex_map a m ∘ f.
proof: Proof. now rewrite comp_assoc, ump_limit_construct_recover. 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