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₂). Proof. simple refine ((_ ,, _) ,, _ ,, _). - exact (pr1 Hfg₁). - exact (pr1 Hfg₂). - abstract (cbn ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite !transportf_dirprod_fam ; use pathsdirprod ; [ apply Hfg₁ | apply Hfg₂ ]). - abstract (cbn ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite !transportf_dirprod_fam ; use pathsdirprod ; [ apply Hfg₁ | apply Hfg₂ ]). 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.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.