Library UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Core.Isos.

Open Scope cat.
Open Scope mor_disp_scope.

Section DisplayedBifunctor.

  Import BifunctorNotations.

  Definition disp_bifunctor_data
             {A B C : category}
             (F : bifunctor_data A B C)
             (DA : disp_cat A)
             (DB : disp_cat B)
             (DC : disp_cat C)
    : UU
    := (Fob : (x : A) (y : B), DA x -> DB y -> DC (x _{F} y)),
       ( (x : A)
          (y1 y2 : B)
          (g : By1,y2)
          (xx : DA x)
          (yy1 : DB y1) (yy2 : DB y2),
        (yy1 -->[g] yy2)
        ->
        ((Fob _ _ xx yy1) -->[x ⊗^{F}_{l} g] (Fob _ _ xx yy2)))
       ×
       ( (x1 x2 : A)
          (y : B)
          (f : Ax1,x2)
          (xx1 : DA x1) (xx2 : DA x2)
          (yy : DB y),
        (xx1 -->[f] xx2)
        ->
        ((Fob _ _ xx1 yy) -->[f ⊗^{F}_{r} y] (Fob _ _ xx2 yy))).

  Definition make_disp_bifunctor_data
             {A B C : category}
             (F : bifunctor_data A B C)
             (DA : disp_cat A)
             (DB : disp_cat B)
             (DC : disp_cat C)
             (Fob : (x : A) (y : B), DA x -> DB y -> DC (x _{F} y))
             (dlw : (x : A)
                      (y1 y2 : B)
                      (g : By1,y2)
                      (xx : DA x)
                      (yy1 : DB y1) (yy2 : DB y2),
                    (yy1 -->[g] yy2)
                    ->
                    ((Fob _ _ xx yy1) -->[x ⊗^{F}_{l} g] (Fob _ _ xx yy2)))
             (drw : (x1 x2 : A)
                      (y : B)
                      (f : Ax1,x2)
                      (xx1 : DA x1) (xx2 : DA x2)
                      (yy : DB y),
                    (xx1 -->[f] xx2)
                    ->
                    ((Fob _ _ xx1 yy) -->[f ⊗^{F}_{r} y] (Fob _ _ xx2 yy)))
    : disp_bifunctor_data F DA DB DC
    :=
    (Fob,,dlw,,drw).

  Definition disp_bifunctor_on_objects
             {A B C : category}
             {F : bifunctor_data A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : (x : A) (y : B), DA x -> DB y -> DC (x _{F} y)
    := pr1 DF.

  Local Notation "xx ⊗⊗_{ DF } yy"
    := (disp_bifunctor_on_objects DF _ _ xx yy)
       (at level 31).

  Definition disp_leftwhiskering_on_morphisms
             {A B C : category}
             {F : bifunctor_data A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : (x : A)
        (y1 y2 : B)
        (g : By1,y2)
        (xx : DA x)
        (yy1 : DB y1)
        (yy2 : DB y2),
      (yy1 -->[g] yy2)
      ->
      ((pr1 DF _ _ xx yy1) -->[x ⊗^{F}_{l} g] (pr1 DF _ _ xx yy2))
    := pr1 (pr2 DF).

  Local Notation "xx ⊗⊗^{ DF }_{l} gg"
    := (disp_leftwhiskering_on_morphisms DF _ _ _ _ xx _ _ gg)
       (at level 31).

  Definition disp_rightwhiskering_on_morphisms
             {A B C : category}
             {F : bifunctor_data A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : (x1 x2 : A)
        (y : B)
        (f : Ax1,x2)
        (xx1 : DA x1)
        (xx2 : DA x2)
        (yy : DB y),
      (xx1 -->[f] xx2)
      ->
      ((pr1 DF _ _ xx1 yy) -->[f ⊗^{F}_{r} y] (pr1 DF _ _ xx2 yy))
    := pr2 (pr2 DF).

  Local Notation "ff ⊗⊗^{ DF }_{r} yy"
    := (disp_rightwhiskering_on_morphisms DF _ _ _ _ _ _ yy ff)
       (at level 31).

  Definition disp_bifunctor_leftidax
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : UU
    := (x : A) (y : B) (xx : DA x) (yy : DB y),
       xx ⊗⊗^{DF}_{l} (id_disp yy)
       =
       transportb _ (bifunctor_leftid F x y) (id_disp (xx ⊗⊗_{DF} yy)).

  Definition disp_bifunctor_rightidax
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : UU
    := (x : A) (y : B) (xx : DA x) (yy : DB y),
       (id_disp xx) ⊗⊗^{DF}_{r} yy
       =
       transportb _ (bifunctor_rightid F y x) (id_disp (xx ⊗⊗_{DF} yy)).

  Definition disp_bifunctor_leftcompax
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : UU
    := (x : A)
         (y1 y2 y3 : B)
         (g1 : By1,y2) (g2 : By2,y3)
         (xx : DA x)
         (yy1 : DB y1) (yy2 : DB y2) (yy3 : DB y3)
         (gg1 : yy1 -->[g1] yy2) (gg2 : yy2 -->[g2] yy3),
       (xx ⊗⊗^{DF}_{l} (gg1 ;; gg2)
       =
       transportb
         _
         (bifunctor_leftcomp F _ _ _ _ g1 g2)
         ((xx ⊗⊗^{DF}_{l} gg1) ;; (xx ⊗⊗^{DF}_{l} gg2))).

  Definition disp_bifunctor_rightcompax
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : UU
    := (x1 x2 x3 : A)
         (y : B)
         (f1 : Ax1,x2) (f2 : Ax2,x3)
         (xx1 : DA x1) (xx2 : DA x2) (xx3 : DA x3)
         (yy : DB y)
         (ff1 : xx1 -->[f1] xx2) (ff2 : xx2 -->[f2] xx3),
       ((ff1 ;; ff2) ⊗⊗^{DF}_{r} yy
       =
       transportb
         _
         (bifunctor_rightcomp F _ _ _ _ f1 f2)
         ((ff1 ⊗⊗^{DF}_{r} yy) ;; (ff2 ⊗⊗^{DF}_{r} yy)) ).

Remark:: No make_disp_functor exists in Displayedcats.Functors
  Definition leftwhiskering_dispfunctor
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
             (dbli : disp_bifunctor_leftidax DF)
             (dblc : disp_bifunctor_leftcompax DF)
    : (x : A) (xx : DA x), disp_functor (leftwhiskering_functor F x) DB DC.
  Show proof.
    intros x xx.
    use tpair.
    - use tpair.
      + intros y yy.
        exact (xx ⊗⊗_{DF} yy).
      + intros y1 y2 yy1 yy2 g gg.
        exact (xx ⊗⊗^{DF}_{l} gg).
    - use tpair.
      + intros y yy.
        exact (dbli x y xx yy).
      + intros y1 y2 y3 yy1 yy2 yy3 g1 g2 gg1 gg2.
        cbn.
        exact (dblc x y1 y2 y3 g1 g2 xx yy1 yy2 yy3 gg1 gg2).

  Definition rightwhiskering_dispfunctor
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
             (dbri : disp_bifunctor_rightidax DF)
             (dbrc : disp_bifunctor_rightcompax DF)
    : (y : B) (yy : DB y), disp_functor (rightwhiskering_functor F y) DA DC.
  Show proof.
    intros y yy.
    use tpair.
    - use tpair.
      + intros x xx.
        exact (xx ⊗⊗_{DF} yy).
      + intros x1 x2 xx1 xx2 f ff.
        exact (ff ⊗⊗^{DF}_{r} yy).
    - use tpair.
      + intros x xx.
        exact (dbri x y xx yy).
      + intros x1 x2 x3 xx1 xx2 xx3 f1 f2 ff1 ff2.
        cbn.
        exact (dbrc x1 x2 x3 y f1 f2 xx1 xx2 xx3 yy ff1 ff2).

  Definition dispfunctoronmorphisms1
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
             {x1 x2 : A}
             {y1 y2 : B}
             {f : Ax1,x2}
             {g : By1,y2}
             {xx1 : DA x1} {xx2 : DA x2}
             {yy1 : DB y1} {yy2 : DB y2}
             (ff : xx1 -->[f] xx2)
             (gg : yy1 -->[g] yy2)
    : xx1 ⊗⊗_{DF} yy1 -->[f ⊗^{F} g] xx2 ⊗⊗_{DF} yy2
    := (ff ⊗⊗^{DF}_{r} yy1) ;; (xx2 ⊗⊗^{DF}_{l} gg).

  Local Notation "ff ⊗⊗^{ DF } gg" := (dispfunctoronmorphisms1 DF ff gg) (at level 31).

  Definition dispfunctoronmorphisms2
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
             {x1 x2 : A}
             {y1 y2 : B}
             {f : Ax1,x2}
             {g : By1,y2}
             {xx1 : DA x1} {xx2 : DA x2}
             {yy1 : DB y1} {yy2 : DB y2}
             (ff : xx1 -->[f] xx2)
             (gg : yy1 -->[g] yy2)
    : xx1 ⊗⊗_{DF} yy1 -->[functoronmorphisms2 F f g] xx2 ⊗⊗_{DF} yy2
    := (xx1 ⊗⊗^{DF}_{l} gg) ;; (ff ⊗⊗^{DF}_{r} yy2).

  Local Notation "ff ⊗⊗^{ DF }_{2} gg" := (dispfunctoronmorphisms2 DF ff gg) (at level 31).

  Definition dispfunctoronmorphisms_are_equal
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : UU
    := (x1 x2 : A)
         (y1 y2 : B)
         (f : Ax1,x2)
         (g : By1,y2)
         (xx1 : DA x1) (xx2 : DA x2)
         (yy1 : DB y1) (yy2 : DB y2)
         (ff : xx1 -->[f] xx2)
         (gg : yy1 -->[g] yy2),
       ff ⊗⊗^{DF} gg
       =
       transportb _ (bifunctor_equalwhiskers F _ _ _ _ f g) (ff ⊗⊗^{DF}_{2} gg).

  Lemma dispwhiskerscommutes
        {A B C : category}
        {F : bifunctor A B C}
        {DA : disp_cat A}
        {DB : disp_cat B}
        {DC : disp_cat C}
        {DF : disp_bifunctor_data F DA DB DC}
        (dfmae : dispfunctoronmorphisms_are_equal DF)
    : (x1 x2 : A)
        (y1 y2 : B)
        (f : Ax1,x2)
        (g : By1,y2)
        (xx1 : DA x1) (xx2 : DA x2)
        (yy1 : DB y1) (yy2 : DB y2)
        (ff : xx1 -->[f] xx2)
        (gg : yy1 -->[g] yy2),
      ((ff ⊗⊗^{ DF}_{r} yy1) ;; (xx2 ⊗⊗^{ DF}_{l} gg)
      =
      transportb
        _
        (bifunctor_equalwhiskers F x1 x2 y1 y2 f g)
        ((xx1 ⊗⊗^{ DF}_{l} gg) ;; (ff ⊗⊗^{ DF}_{r} yy2))).
  Show proof.
    intros.
    apply dfmae.

  Definition is_disp_bifunctor
             {A B C : category}
             (F : bifunctor A B C)
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
    : UU
    := (disp_bifunctor_leftidax DF)
       × (disp_bifunctor_rightidax DF)
       × (disp_bifunctor_leftcompax DF)
       × (disp_bifunctor_rightcompax DF)
       × (dispfunctoronmorphisms_are_equal DF).

  Definition disp_bifunctor
             {A B C : category}
             (F : bifunctor A B C)
             (DA : disp_cat A)
             (DB : disp_cat B)
             (DC : disp_cat C)
    : UU
    := (DF : disp_bifunctor_data F DA DB DC), is_disp_bifunctor F DF.

  Definition make_disp_bifunctor
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor_data F DA DB DC)
             (H : is_disp_bifunctor F DF)
    : disp_bifunctor F DA DB DC
    := (DF,,H).

  Definition make_disp_bifunctor_locally_prop
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             {LP : locally_propositional DC}
             (DF : disp_bifunctor_data F DA DB DC)
    : disp_bifunctor F DA DB DC.
  Show proof.
    exists DF.
    abstract (repeat split ; try intro ; intros ; apply LP).

  Definition disp_bifunctordata_from_disp_bifunctor
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : disp_bifunctor_data F DA DB DC
    := pr1 DF.

  Coercion disp_bifunctordata_from_disp_bifunctor : disp_bifunctor >-> disp_bifunctor_data.

  Definition is_disp_bifunctor_from_disp_bifunctor
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : is_disp_bifunctor F DF
    := pr2 DF.

  Definition disp_bifunctor_leftid
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : disp_bifunctor_leftidax DF
    := pr1 (is_disp_bifunctor_from_disp_bifunctor DF).

  Definition disp_bifunctor_rightid
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : disp_bifunctor_rightidax DF
    := pr1 (pr2 (is_disp_bifunctor_from_disp_bifunctor DF)).

  Definition disp_bifunctor_leftcomp
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : disp_bifunctor_leftcompax DF
    := pr1 (pr2 (pr2 (is_disp_bifunctor_from_disp_bifunctor DF))).

  Definition disp_bifunctor_rightcomp
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : disp_bifunctor_rightcompax DF
    := pr1 (pr2 (pr2 (pr2 (is_disp_bifunctor_from_disp_bifunctor DF)))).

  Definition disp_bifunctor_equalwhiskers
             {A B C : category}
             {F : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (DF : disp_bifunctor F DA DB DC)
    : dispfunctoronmorphisms_are_equal DF
    := pr2 (pr2 (pr2 (pr2 (is_disp_bifunctor_from_disp_bifunctor DF)))).

End DisplayedBifunctor.

Module DisplayedBifunctorNotations.
  Notation "xx ⊗⊗_{ DF } yy" :=
    (disp_bifunctor_on_objects DF _ _ xx yy)
    (at level 31).
  Notation "xx ⊗⊗^{ DF }_{l} gg" :=
    (disp_leftwhiskering_on_morphisms DF _ _ _ _ xx _ _ gg)
    (at level 31).
  Notation "ff ⊗⊗^{ DF }_{r} yy" :=
    (disp_rightwhiskering_on_morphisms DF _ _ _ _ _ _ yy ff)
    (at level 31).
  Notation "ff ⊗⊗^{ DF } gg" :=
    (dispfunctoronmorphisms1 DF ff gg)
    (at level 31).
End DisplayedBifunctorNotations.

Section DisplayedWhiskeredBinaturaltransformation.

  Import DisplayedBifunctorNotations.

  Definition disp_binat_trans_data
             {A B C : category}
             {F : bifunctor_data A B C}
             {G : bifunctor_data A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (α : binat_trans_data F G)
             (DF : disp_bifunctor_data F DA DB DC)
             (DG : disp_bifunctor_data G DA DB DC)
    : UU
    := (x : A)
         (y : B)
         (xx : DA x)
         (yy : DB y),
       xx ⊗⊗_{DF} yy -->[α x y] xx ⊗⊗_{DG} yy.

  Definition make_disp_binat_trans_data
             {A B C : category}
             {F : bifunctor_data A B C}
             {G : bifunctor_data A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             {α : binat_trans_data F G}
             {DF : disp_bifunctor_data F DA DB DC}
             {DG : disp_bifunctor_data G DA DB DC}
             ( : (x : A)
                      (y : B)
                      (xx : DA x)
                      (yy : DB y),
                    xx ⊗⊗_{DF} yy -->[α x y] xx ⊗⊗_{DG} yy)
    : disp_binat_trans_data α DF DG
    := .

  Definition is_disp_binat_trans
             {A B C : category}
             {F : bifunctor_data A B C}
             {G : bifunctor_data A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             {α : binat_trans F G}
             {DF : disp_bifunctor_data F DA DB DC}
             {DG : disp_bifunctor_data G DA DB DC}
             ( : disp_binat_trans_data α DF DG)
    : UU
    := ( (x : A)
          (y1 y2 : B)
          (g : By1,y2)
          (xx : DA x)
          (yy1 : DB y1) (yy2 : DB y2)
          (gg : yy1 -->[g] yy2),
        ((xx ⊗⊗^{DF}_{l} gg) ;; ( _ _ xx yy2)
        =
        transportb
          _
          (pr1 (pr2 α) x y1 y2 _)
          (( _ _ xx yy1) ;; (xx ⊗⊗^{DG}_{l} gg))))
         ×
         ( (x1 x2 : A)
            (y : B)
            (f : Ax1,x2)
            (xx1 : DA x1) (xx2 : DA x2)
            (yy : DB y)
            (ff : xx1 -->[f] xx2),
          ((ff ⊗⊗^{DF}_{r} yy) ;; ( _ _ xx2 yy)
          =
          transportb
            _
            (pr2 (pr2 α) x1 x2 y _)
            (( _ _ xx1 yy) ;; (ff ⊗⊗^{DG}_{r} yy)))).


  Lemma full_disp_naturality_condition
        {A B C : category}
        {F : bifunctor A B C}
        {G : bifunctor A B C}
        {DA : disp_cat A}
        {DB : disp_cat B}
        {DC : disp_cat C}
        {α : binat_trans F G}
        {DF : disp_bifunctor_data F DA DB DC}
        {DG : disp_bifunctor_data G DA DB DC}
        { : disp_binat_trans_data α DF DG}
        (dαn : is_disp_binat_trans )
        (x1 x2 : A)
        (y1 y2 : B)
        (f : Ax1,x2)
        (g : By1,y2)
        (xx1 : DA x1) (xx2 : DA x2)
        (yy1 : DB y1) (yy2 : DB y2)
        (ff : xx1 -->[f] xx2)
        (gg : yy1 -->[g] yy2)
    : (ff ⊗⊗^{DF} gg) ;; ( _ _ xx2 yy2)
      =
      transportb
        _
        (full_naturality_condition (pr2 α) f g)
        (( _ _ xx1 yy1) ;; (ff ⊗⊗^{DG} gg)).
  Show proof.
    unfold dispfunctoronmorphisms1.
    etrans. { apply assoc_disp_var. }
    apply transportf_transpose_left.
    rewrite transport_b_b.
    rewrite (pr1 dαn).
    etrans. { apply mor_disp_transportf_prewhisker. }
    apply transportb_transpose_right.
    rewrite transport_f_f.
    apply transportf_transpose_left.
    etrans. { apply assoc_disp. }
    rewrite (pr2 dαn).
    apply transportb_transpose_right.
    rewrite transport_f_b.
    apply transportf_transpose_left.
    etrans. { apply mor_disp_transportf_postwhisker. }
    apply transportf_transpose_left.
    rewrite transport_b_b.
    rewrite assoc_disp_var.
    apply transportf_transpose_left.
    rewrite transport_b_b.
    use pathsinv0.
    apply transportf_set.
    apply homset_property.

  Definition disp_binat_trans
             {A B C : category}
             {F : bifunctor A B C}
             {G : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             (α : binat_trans F G)
             (DF : disp_bifunctor_data F DA DB DC)
             (DG : disp_bifunctor_data G DA DB DC)
    : UU
    := ( : disp_binat_trans_data α DF DG), is_disp_binat_trans .

  Definition make_disp_binat_trans
             {A B C : category}
             {F : bifunctor A B C}
             {G : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             {α : binat_trans F G}
             {DF : disp_bifunctor_data F DA DB DC}
             {DG : disp_bifunctor_data G DA DB DC}
             ( : disp_binat_trans_data α DF DG)
             (H : is_disp_binat_trans )
    : disp_binat_trans α DF DG
    := (,,H).

  Definition is_z_iso_disp
             {C : precategory}
             {D : disp_cat_data C}
             {x y : C}
             (f : z_iso x y)
             {xx : D x}
             {yy : D y}
             (ff : xx -->[f] yy)
    : UU
    := (gg : yy -->[inv_from_z_iso f] xx),
       (gg ;; ff
        =
        transportb
          _
          (z_iso_after_z_iso_inv _)
          (id_disp _))
         ×
         (ff ;; gg
          =
            transportb
              _
              (z_iso_inv_after_z_iso _)
              (id_disp _)).

  Definition is_dispbinatiso
             {A B C : category}
             {F : bifunctor A B C}
             {G : bifunctor A B C}
             {DA : disp_cat A}
             {DB : disp_cat B}
             {DC : disp_cat C}
             {α : binat_trans F G}
             (αiso : is_binatiso α)
             {DF : disp_bifunctor_data F DA DB DC}
             {DG : disp_bifunctor_data G DA DB DC}
             ( : disp_binat_trans α DF DG)
    : UU
    := (x : A)
         (y : B)
         (xx : DA x)
         (yy : DB y),
       is_z_iso_disp (α x y ,, αiso x y) (pr1 x y xx yy).
End DisplayedWhiskeredBinaturaltransformation.