Proposition is_z_iso_disp_strict_twosided_disp_cat_to_ff : disp_functor_ff F. Proof. intros x y xx yy f. use isweq_iso. - exact (λ ff, transportf_disp_mor2 (id_right _ @ id_left _) (id_right _ @ id_left _) (idtoiso_twosided_disp (idpath _) (idpath _) (!(two_sided_disp_cat_iso_path_ob _)) ;;2 #2 G ff ;;2 idtoiso_twosided_disp (idpath _) (idpath _) (two_sided_disp_cat_iso_path_ob _))). - intro ff ; cbn -[idtoiso_twosided_disp]. etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. exact (two_sided_disp_cat_iso_path_mor ff). } rewrite (two_disp_post_whisker_f (D := D₁)). rewrite (two_disp_pre_whisker_f (D := D₁)). rewrite transport_f_f_disp_mor2. rewrite !assoc_two_disp_alt. rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. etrans. { do 4 apply maponpaths. apply (idtoiso_twosided_disp_concat (D := D₁)). } rewrite pathsinv0l. unfold transportb_disp_mor2. rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. etrans. { do 3 apply maponpaths. apply (id_two_disp_right (D := D₁)). } unfold transportb_disp_mor2. rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. rewrite assoc_two_disp. unfold transportb_disp_mor2. rewrite !transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply (idtoiso_twosided_disp_concat (D := D₁)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite !transport_f_f_disp_mor2. rewrite pathsinv0l. etrans. { apply maponpaths. apply (id_two_disp_left (D := D₁)). } unfold transportb_disp_mor2. rewrite !transport_f_f_disp_mor2. apply transportf_disp_mor2_idpath. - intro ff ; cbn -[idtoiso_twosided_disp]. rewrite disp_functor_transportf_disp_mor2. rewrite !disp_functor_comp_two_disp. etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. apply two_sided_disp_cat_iso_path_mor_alt. } cbn -[idtoiso_twosided_disp]. rewrite (two_disp_post_whisker_f (D := D₂)). rewrite (two_disp_pre_whisker_f (D := D₂)). rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths. apply disp_functor_idtoiso_twosided_disp. } etrans. { apply maponpaths. do 2 apply maponpaths_2. apply disp_functor_idtoiso_twosided_disp. } rewrite !(assoc_two_disp_alt (D := D₂)). rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. etrans. { do 4 apply maponpaths. apply (idtoiso_twosided_disp_concat (D := D₂)). } unfold transportb_disp_mor2. rewrite !two_disp_post_whisker_f. rewrite !transport_f_f_disp_mor2. rewrite !(assoc_two_disp (D := D₂)). unfold transportb_disp_mor2. rewrite !transport_f_f_disp_mor2. etrans. { apply maponpaths. do 2 apply maponpaths_2. apply (idtoiso_twosided_disp_concat (D := D₂)). } unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite !transport_f_f_disp_mor2. rewrite !idtoiso_twosided_disp_identity. etrans. { apply maponpaths. apply (id_two_disp_right (D := D₂)). } etrans. { do 2 apply maponpaths. apply (id_two_disp_left (D := D₂)). } unfold transportb_disp_mor2. rewrite !transport_f_f_disp_mor2. apply transportf_disp_mor2_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.