proposition: Proposition eq_twosided_disp_functor_help {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 : pr11 FG₁ = pr11 FG₂) (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 _) (toforallpaths _ _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ p x₂) y₂) xy₂) = transportf_disp_mor2 (id_left _ @ !(id_right _)) (id_left _ @ !(id_right _)) (idtoiso_twosided_disp (idpath _) (idpath _) (toforallpaths _ _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ p x₁) y₁) xy₁) ;;2 (#2 FG₂ fg))) : FG₁ = FG₂.
proof: Proof. use subtypePath. { intro. apply isaprop_twosided_disp_functor_laws. } induction FG₁ as [ [ FG₁o FG₁m ] FG₁H ]. induction FG₂ as [ [ FG₂o FG₂m ] FG₂H ]. cbn in *. induction p ; cbn in q. apply maponpaths. use funextsec ; intro x₁. use funextsec ; intro x₂. use funextsec ; intro y₁. use funextsec ; intro y₂. use funextsec ; intro xy₁. use funextsec ; intro xy₂. use funextsec ; intro f. use funextsec ; intro g. use funextsec ; intro fg. specialize (q x₁ x₂ f y₁ y₂ g xy₁ xy₂ fg). rewrite id_two_disp_left in q. rewrite id_two_disp_right in q. unfold transportb_disp_mor2 in q. rewrite transport_f_f_disp_mor2 in q. refine (!(transportbf_disp_mor2 (!(id_right _)) (!(id_right _)) _) @ maponpaths (transportb_disp_mor2 _ _) (_ @ q @ _) @ transportbf_disp_mor2 _ _ _). - use transportf_disp_mor2_eq. apply idpath. - use transportf_disp_mor2_eq. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Total