Proposition eq_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₁ FG₂ : twosided_disp_functor F G D D') (p : ∏ (x : C₁) (y : C₂) (xy : D x y), FG₁ x y xy = FG₂ x y xy) (q : ∏ (x₁ x₂ : C₁) (f : x₁ --> x₂) (y₁ y₂ : C₂) (g : y₁ --> y₂) (xy₁ : D x₁ y₁) (xy₂ : D x₂ y₂) (fg : xy₁ -->[ f ][ g ] xy₂), #2 FG₁ fg ;;2 idtoiso_twosided_disp (idpath _) (idpath _) (p x₂ y₂ xy₂) = transportf_disp_mor2 (id_left _ @ !(id_right _)) (id_left _ @ !(id_right _)) (idtoiso_twosided_disp (idpath _) (idpath _) (p x₁ y₁ xy₁) ;;2 (#2 FG₂ fg))) : FG₁ = FG₂. Proof. use eq_twosided_disp_functor_help. - use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro xy. exact (p x y xy). - intros x₁ x₂ f y₁ y₂ g xy₁ xy₂ fg. rewrite !toforallpaths_funextsec. apply q. Qed.
Require Import UniMath.Foundations.All. 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.Total.