Proposition idtoiso_twosided_disp_functor' {C₁ C₁' C₂ C₂' : category} {F : C₁ ⟶ C₁'} {G : C₂ ⟶ C₂'} {D : twosided_disp_cat C₁ C₂} {D' : twosided_disp_cat C₁' C₂'} (FG : twosided_disp_functor F G D D') {x : C₁} {y : C₂} {xy xy' : D x y} (p : xy = xy') : #2 FG (idtoiso_twosided_disp (idpath x) (idpath y) p) = transportb_disp_mor2 (functor_id F _) (functor_id G _) (pr1 (idtoiso_twosided_disp (idpath (F x)) (idpath (G y)) (maponpaths (λ xy, FG x y xy) p))). Proof. induction p ; cbn. rewrite twosided_disp_functor_id. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness.