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. 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.
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. Require Import UniMath.CategoryTheory.Limits.Pushouts.