Definition is_z_iso_iso_comma {x y : iso_comma} (f : x --> y) (H₁ : is_z_isomorphism (pr11 f)) (H₂ : is_z_isomorphism (pr21 f)) : is_z_isomorphism f. Proof. simple refine ((_ ,, _) ,, _). split. - exact (inv_from_z_iso (_ ,, H₁)). - exact (inv_from_z_iso (_ ,, H₂)). - abstract (cbn ; rewrite !functor_on_inv_from_z_iso ; use z_iso_inv_on_left ; rewrite assoc' ; refine (!_) ; use z_iso_inv_on_right ; cbn ; refine (!_) ; apply (pr2 f)). - split. + abstract (use eq_iso_comma_mor ; cbn ; [ apply (z_iso_inv_after_z_iso (make_z_iso' _ H₁)) | apply (z_iso_inv_after_z_iso (make_z_iso' _ H₂)) ]). + abstract (use eq_iso_comma_mor ; cbn ; [ apply (z_iso_after_z_iso_inv (make_z_iso' _ H₁)) | apply (z_iso_after_z_iso_inv (make_z_iso' _ H₂)) ]). 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.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.