Lemma two_sided_disp_cat_iso_path_mor_alt {x₁ x₂ y₁ y₂ : C} (xx := (x₁ ,, y₁) : category_binproduct C C) (yy := (x₂ ,, y₂) : category_binproduct C C) {f : x₁ --> x₂} {g : y₁ --> y₂} (h := (f ,, g) : xx --> yy) {xy₁ : D₂ x₁ y₁} {xy₂ : D₂ x₂ y₂} (fg : xy₁ -->[ f ][ g ] xy₂) (fg' := #2 G fg : @mor_disp _ (twosided_disp_cat_to_disp_cat C C D₁) xx yy (G x₁ y₁ xy₁) (G x₂ y₂ xy₂) h) : (♯F fg' = transportf_disp_mor2 (id_right _ @ id_left (pr1 h)) (id_right _ @ id_left (pr2 h)) (idtoiso_twosided_disp (idpath _) (idpath _) (two_sided_disp_cat_iso_path_ob_alt xy₁) ;;2 fg ;;2 idtoiso_twosided_disp (idpath _) (idpath _) (!(two_sided_disp_cat_iso_path_ob_alt xy₂))))%mor_disp. Proof. etrans. { apply (path_twosided_disp_functor_mor (z_iso_disp_after_inv_mor HF)). } cbn -[idtoiso_twosided_disp]. etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. apply (transportb_disp_cat_of_strict_twosided_disp_cat_mor _ _ _ (id_left (C := cat_of_setcategory) (functor_identity C))). } 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. 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. use transportf_disp_mor2_eq. use idtoiso_twosided_disp_triple_concat. 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.