fact: Definition make_is_iso_prod_of_twosided_disp_cat {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : x₁ --> x₂} (Hf : is_z_isomorphism f) {g : y₁ --> y₂} (Hg : is_z_isomorphism g) {xy₁₁ : D₁ x₁ y₁} {xy₁₂ : D₂ x₁ y₁} {xy₂₁ : D₁ x₂ y₂} {xy₂₂ : D₂ x₂ y₂} (fg₁ : xy₁₁ -->[ f ][ g ] xy₂₁) (Hfg₁ : is_iso_twosided_disp Hf Hg fg₁) (fg₂ : xy₁₂ -->[ f ][ g ] xy₂₂) (Hfg₂ : is_iso_twosided_disp Hf Hg fg₂) : @is_iso_twosided_disp _ _ prod_of_twosided_disp_cat _ _ _ _ (xy₁₁ ,, xy₁₂) (xy₂₁ ,, xy₂₂) f g Hf Hg (fg₁ ,, fg₂).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete