Definition iso_prod_of_twosided_disp_cat_pr2 {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : z_iso x₁ x₂} {g : z_iso y₁ y₂} {xy₁₁ : D₁ x₁ y₁} {xy₁₂ : D₂ x₁ y₁} {xy₂₁ : D₁ x₂ y₂} {xy₂₂ : D₂ x₂ y₂} (fg : @iso_twosided_disp _ _ prod_of_twosided_disp_cat _ _ _ _ f g (xy₁₁ ,, xy₁₂) (xy₂₁ ,, xy₂₂)) : iso_twosided_disp f g xy₁₂ xy₂₂. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr21 fg). - exact (pr212 fg). - abstract (refine (maponpaths dirprod_pr2 (pr122 fg) @ _) ; cbn ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite !transportf_dirprod_fam ; apply idpath). - abstract (refine (maponpaths dirprod_pr2 (pr222 fg) @ _) ; cbn ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite !transportf_dirprod_fam ; apply idpath). 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.