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 : B⟦y1,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 : A⟦x1,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 : B⟦y1,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 : A⟦x1,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 : B⟦y1,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 : A⟦x1,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 : B⟦y1,y2⟧) (g2 : B⟦y2,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 : A⟦x1,x2⟧) (f2 : A⟦x2,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)) ).
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 : B⟦y1,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 : A⟦x1,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 : B⟦y1,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 : A⟦x1,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 : B⟦y1,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 : A⟦x1,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 : B⟦y1,y2⟧) (g2 : B⟦y2,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 : A⟦x1,x2⟧) (f2 : A⟦x2,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.
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.
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 : A⟦x1,x2⟧}
{g : B⟦y1,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 : A⟦x1,x2⟧}
{g : B⟦y1,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 : A⟦x1,x2⟧)
(g : B⟦y1,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 : A⟦x1,x2⟧)
(g : B⟦y1,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.
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.
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}
(dα : ∏ (x : A)
(y : B)
(xx : DA x)
(yy : DB y),
xx ⊗⊗_{DF} yy -->[α x y] xx ⊗⊗_{DG} yy)
: disp_binat_trans_data α DF DG
:= dα.
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}
(dα : disp_binat_trans_data α DF DG)
: UU
:= (∏ (x : A)
(y1 y2 : B)
(g : B⟦y1,y2⟧)
(xx : DA x)
(yy1 : DB y1) (yy2 : DB y2)
(gg : yy1 -->[g] yy2),
((xx ⊗⊗^{DF}_{l} gg) ;; (dα _ _ xx yy2)
=
transportb
_
(pr1 (pr2 α) x y1 y2 _)
((dα _ _ xx yy1) ;; (xx ⊗⊗^{DG}_{l} gg))))
×
(∏ (x1 x2 : A)
(y : B)
(f : A⟦x1,x2⟧)
(xx1 : DA x1) (xx2 : DA x2)
(yy : DB y)
(ff : xx1 -->[f] xx2),
((ff ⊗⊗^{DF}_{r} yy) ;; (dα _ _ xx2 yy)
=
transportb
_
(pr2 (pr2 α) x1 x2 y _)
((dα _ _ 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}
{dα : disp_binat_trans_data α DF DG}
(dαn : is_disp_binat_trans dα)
(x1 x2 : A)
(y1 y2 : B)
(f : A⟦x1,x2⟧)
(g : B⟦y1,y2⟧)
(xx1 : DA x1) (xx2 : DA x2)
(yy1 : DB y1) (yy2 : DB y2)
(ff : xx1 -->[f] xx2)
(gg : yy1 -->[g] yy2)
: (ff ⊗⊗^{DF} gg) ;; (dα _ _ xx2 yy2)
=
transportb
_
(full_naturality_condition (pr2 α) f g)
((dα _ _ xx1 yy1) ;; (ff ⊗⊗^{DG} gg)).
Show proof.
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
:= ∑ (dα : disp_binat_trans_data α DF DG), is_disp_binat_trans dα.
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}
(dα : disp_binat_trans_data α DF DG)
(H : is_disp_binat_trans dα)
: disp_binat_trans α DF DG
:= (dα,,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}
(dα : 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 dα x y xx yy).
End DisplayedWhiskeredBinaturaltransformation.
{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).
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).
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 : A⟦x1,x2⟧}
{g : B⟦y1,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 : A⟦x1,x2⟧}
{g : B⟦y1,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 : A⟦x1,x2⟧)
(g : B⟦y1,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 : A⟦x1,x2⟧)
(g : B⟦y1,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.
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).
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}
(dα : ∏ (x : A)
(y : B)
(xx : DA x)
(yy : DB y),
xx ⊗⊗_{DF} yy -->[α x y] xx ⊗⊗_{DG} yy)
: disp_binat_trans_data α DF DG
:= dα.
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}
(dα : disp_binat_trans_data α DF DG)
: UU
:= (∏ (x : A)
(y1 y2 : B)
(g : B⟦y1,y2⟧)
(xx : DA x)
(yy1 : DB y1) (yy2 : DB y2)
(gg : yy1 -->[g] yy2),
((xx ⊗⊗^{DF}_{l} gg) ;; (dα _ _ xx yy2)
=
transportb
_
(pr1 (pr2 α) x y1 y2 _)
((dα _ _ xx yy1) ;; (xx ⊗⊗^{DG}_{l} gg))))
×
(∏ (x1 x2 : A)
(y : B)
(f : A⟦x1,x2⟧)
(xx1 : DA x1) (xx2 : DA x2)
(yy : DB y)
(ff : xx1 -->[f] xx2),
((ff ⊗⊗^{DF}_{r} yy) ;; (dα _ _ xx2 yy)
=
transportb
_
(pr2 (pr2 α) x1 x2 y _)
((dα _ _ 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}
{dα : disp_binat_trans_data α DF DG}
(dαn : is_disp_binat_trans dα)
(x1 x2 : A)
(y1 y2 : B)
(f : A⟦x1,x2⟧)
(g : B⟦y1,y2⟧)
(xx1 : DA x1) (xx2 : DA x2)
(yy1 : DB y1) (yy2 : DB y2)
(ff : xx1 -->[f] xx2)
(gg : yy1 -->[g] yy2)
: (ff ⊗⊗^{DF} gg) ;; (dα _ _ xx2 yy2)
=
transportb
_
(full_naturality_condition (pr2 α) f g)
((dα _ _ 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.
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
:= ∑ (dα : disp_binat_trans_data α DF DG), is_disp_binat_trans dα.
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}
(dα : disp_binat_trans_data α DF DG)
(H : is_disp_binat_trans dα)
: disp_binat_trans α DF DG
:= (dα,,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}
(dα : 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 dα x y xx yy).
End DisplayedWhiskeredBinaturaltransformation.