Lemma equiv_isPushout2 {a b c d : C} (f : C⟦a, b⟧) (g : C⟦a, c⟧) (i1 : C⟦b, d⟧) (i2 : C⟦c, d⟧) (H : f · i1 = g · i2) : Limits.Pushouts.isPushout f g i1 i2 H <- isPushout C f g i1 i2 H. Proof. intros X R k h HH. set (XR := make_Pushout C f g d i1 i2 H X). use unique_exists. + use (PushoutArrow C XR). - exact k. - exact h. - exact HH. + split. - exact (PushoutArrow_PushoutIn1 C XR R k h HH). - exact (PushoutArrow_PushoutIn2 C XR R k h HH). + intros y; apply isapropdirprod; apply C. + intros y T. use (PushoutArrowUnique C _ _ XR). - exact R. - exact (pr1 T). - exact (pr2 T). 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.