Lemma MorphismsOutofPushoutEqual {a b c d : C} {f : a --> b} {g : a --> c} {in1 : b --> d} {in2 : c --> d} {H : f · in1 = g · in2} (P : isPushout f g in1 in2 H) {e} (w w': d --> e) (H1 : in1 · w = in1 · w') (H2 : in2 · w = in2 · w') : w = w'. Proof. assert (Hw : f · in1 · w = g · in2 · w). { rewrite H. apply idpath. } assert (Hw' : f · in1 · w' = g · in2 · w'). { rewrite H. apply idpath. } set (Pb := make_Pushout _ _ _ _ _ _ P). rewrite <- assoc in Hw. rewrite <- assoc in Hw. set (Xw := PushoutArrow Pb e (in1 · w) (in2 · w) Hw). intermediate_path Xw; [ apply PushoutArrowUnique; apply idpath |]. apply pathsinv0. apply PushoutArrowUnique. apply pathsinv0. apply H1. apply pathsinv0. apply H2. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors.