Definition BinProduct_z_iso_lr : BinProduct C x₂ y₂. Proof. use make_BinProduct. - exact p. - exact π₁. - exact π₂. - intros w f g. use iscontraprop1. + apply BinProduct_z_iso_lr_unique. + refine (BinProductArrow _ p (f · l) (g · r) ,, _ ,, _). * abstract (unfold π₁ ; rewrite !assoc ; rewrite BinProductPr1Commutes ; rewrite !assoc' ; rewrite z_iso_inv_after_z_iso ; apply id_right). * abstract (unfold π₂ ; rewrite !assoc ; rewrite BinProductPr2Commutes ; rewrite !assoc' ; rewrite z_iso_inv_after_z_iso ; apply id_right). 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.