Proposition to_is_z_iso_disp_strict_twosided_disp_cat_inv_laws : twosided_disp_functor_laws (functor_identity C) (functor_identity C) D₂ D₁ to_is_z_iso_disp_strict_twosided_disp_cat_inv_data. Proof. split. - intros x y xy ; cbn -[idtoiso_twosided_disp]. use (invmaponpathsweq (φ₁ _ _ _ _)). etrans. { apply homotweqinvweq. } cbn -[idtoiso_twosided_disp]. rewrite (id_two_disp_right (D := D₂)). unfold transportb_disp_mor2. rewrite (two_disp_pre_whisker_f (D := D₂)). rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply (idtoiso_twosided_disp_concat (D := D₂)). } unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. rewrite pathsinv0r. cbn. refine (!_). etrans. { exact (@disp_functor_id _ _ _ _ _ F (_ ,, _) (invmap (φ₀ x y) xy)). } cbn. refine (!_). apply transportf_disp_mor2_idpath. - intros x₁ x₂ x₃ y₁ y₂ y₃ xy₁ xy₂ xy₃ f₁ g₁ fg₁ f₂ g₂ fg₂. cbn -[idtoiso_twosided_disp]. use (invmaponpathsweq (φ₁ _ _ _ _)). etrans. { apply homotweqinvweq. } cbn -[idtoiso_twosided_disp]. refine (!_). etrans. { apply disp_functor_comp_two_disp. } etrans. { apply maponpaths. apply (homotweqinvweq (φ₁ _ _ _ _)). } etrans. { apply maponpaths_2. apply (homotweqinvweq (φ₁ _ _ _ _)). } rewrite two_disp_pre_whisker_f. rewrite two_disp_post_whisker_f. rewrite transport_f_f_disp_mor2. rewrite !(assoc_two_disp_alt (D := D₂)). rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. etrans. { do 3 apply maponpaths. rewrite !(assoc_two_disp (D := D₂)). do 2 apply maponpaths. do 2 apply maponpaths_2. apply (idtoiso_twosided_disp_concat (D := D₂)). } rewrite pathsinv0l. unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. etrans. { do 3 apply maponpaths. apply maponpaths_2. apply id_two_disp_left. } unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. apply transportf_disp_mor2_eq. apply idpath. Qed.
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.