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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.