Definition Pushout_from_Coequalizer_BinCoproduct_isPushout (X Y Z : C) (f : Z --> X) (g : Z --> Y) (BinCoprod : BinCoproduct X Y) (CEq : Coequalizer (f · (BinCoproductIn1 BinCoprod)) (g · (BinCoproductIn2 BinCoprod))) : isPushout f g (BinCoproductIn1 BinCoprod · CoequalizerArrow CEq) (BinCoproductIn2 BinCoprod · CoequalizerArrow CEq) (Pushout_from_Coequalizer_BinCoproduct_eq X Y Z f g BinCoprod CEq).
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.