Definition to_is_z_iso_disp_strict_twosided_disp_cat_inv_data : twosided_disp_functor_data (functor_identity C) (functor_identity C) D₂ D₁. Proof. simple refine (_ ,, _). - exact (λ x y xy, invmap (φ₀ x y) xy). - exact (λ x₁ x₂ y₁ y₂ xy₁ xy₂ f g fg, invmap (φ₁ (invmap (φ₀ x₁ y₁) xy₁) (invmap (φ₀ x₂ y₂) xy₂) f g) (transportf_disp_mor2 (id_right _ @ id_left _) (id_right _ @ id_left _) (idtoiso_twosided_disp (idpath _) (idpath _) (homotweqinvweq (φ₀ x₁ y₁) _) ;;2 fg ;;2 idtoiso_twosided_disp (idpath _) (idpath _) (!(homotweqinvweq (φ₀ x₂ y₂)) _)))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.DispFunctorPair. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Section FromIso. End FromIso.