proposition: Lemma PushoutArrowUnique {a b c d : C} (f : C⟦a, b⟧) (g : C⟦a, c⟧) (Po : Pushout f g) (e : C) (h : C⟦b, e⟧) (k : C⟦c, e⟧) (Hcomm : f · h = g · k) (w : C⟦PushoutObject Po, e⟧) (H1 : PushoutIn1 Po · w = h) (H2 : PushoutIn2 Po · w = k) : w = PushoutArrow Po _ h k Hcomm.
proof: Proof. apply path_to_ctr. use three_rec_dep; try assumption. set (X := colimInCommutes Po One Two tt). use (pathscomp0 (! (maponpaths (λ h' : _, h' · w) X))). now rewrite <- assoc; simpl; rewrite <- H1. 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 UniMath.CategoryTheory.Limits.Pushouts