Definition inl_iso_map {C₁ C₂ : category} {x₁ x₂ : C₁} (f : z_iso x₁ x₂) : @z_iso (bincoprod_of_category C₁ C₂) (inl x₁) (inl x₂). Proof. use make_z_iso. - exact f. - exact (inv_from_z_iso f). - split. + exact (z_iso_inv_after_z_iso f). + exact (z_iso_after_z_iso_inv f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering.