Definition equiv_Pushout2 {a b c : C} (f : C⟦a, b⟧) (g : C⟦a, c⟧) : Limits.Pushouts.Pushout f g <- Pushout C f g. Proof. intros X. exact (Limits.Pushouts.make_Pushout f g (PushoutObject C X) (PushoutIn1 C X) (PushoutIn2 C X) (PushoutSqrCommutes C X) (equiv_isPushout2 _ _ _ _ _ (isPushout_Pushout C X))). Defined.
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.