Definition BinCoproduct_z_iso_lr : BinCoproduct x₂ y₂. Proof. use make_BinCoproduct. - exact p. - exact ι₁. - exact ι₂. - intros w f g. use iscontraprop1. + apply BinCoproduct_z_iso_lr_unique. + refine (BinCoproductArrow p (l · f) (r · g) ,, _ ,, _). * abstract (unfold ι₁ ; rewrite !assoc' ; rewrite BinCoproductIn1Commutes ; rewrite !assoc ; rewrite z_iso_after_z_iso_inv ; apply id_left). * abstract (unfold ι₂ ; rewrite !assoc' ; rewrite BinCoproductIn2Commutes ; rewrite !assoc ; rewrite z_iso_after_z_iso_inv ; apply id_left). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.