Lemma PullbackArrowUnique {a b c d : C} (f : C⟦b, a⟧) (g : C⟦c, a⟧) (Pb : Pullback f g) e (h : C⟦e, b⟧) (k : C⟦e, c⟧) (Hcomm : h · f = k · g) (w : C⟦e, PullbackObject Pb⟧) (H1 : w · PullbackPr1 Pb = h) (H2 : w · PullbackPr2 Pb = k) : w = PullbackArrow Pb _ h k Hcomm. Proof. apply path_to_ctr. use three_rec_dep; try assumption. set (X:= limOutCommutes Pb Three Two tt). eapply pathscomp0. eapply maponpaths, pathsinv0, X. simpl. rewrite assoc. eapply pathscomp0. apply cancel_postcomposition, H2. apply (!Hcomm). 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.