proposition: Lemma PullbackEndo_is_identity {a b c : C}{f : C⟦b, a⟧} {g : C⟦c, a⟧} (Pb : Pullback f g) (k : C⟦lim Pb, lim Pb⟧) (kH1 : k · PullbackPr1 Pb = PullbackPr1 Pb) (kH2 : k · PullbackPr2 Pb = PullbackPr2 Pb) : identity (lim Pb) = k.
proof: Proof. apply lim_endo_is_identity. use three_rec_dep. - apply kH1. - unfold limOut. simpl. assert (T:= coneOutCommutes (limCone Pb) Three Two tt). eapply pathscomp0. apply maponpaths. apply (!T). rewrite assoc. eapply pathscomp0. apply cancel_postcomposition. apply kH2. apply T. - assumption. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits