Timings for MonoidalTwistConstruction.v
Require Import Basics.Overture Basics.Tactics Types.Forall WildCat.Monoidal.
Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv.
Require Import WildCat.NatTrans WildCat.Square WildCat.Opposite.
(** * Building Symmetric Monoidal Categories *)
(** The following construction is what we call the "twist construction". It is a way to build a symmetric monoidal category from simpler pieces than the axioms ask for.
The core observation is that the associator can be broken up into a [braid] and what we call a [twist] map. The twist map takes a right associated triple [(A, (B, C))] and swaps the first two factors [(B, (A, C)]. Together with functoriality of the tensor and the braiding, here termed [braid] we can simplify the axioms we ask for.
For instance, the hexagon identity is about associators, but if we unfold the definition and simplify the diagram, we get a diagram about only twists and braids.
This means in practice, you can show a category has a symmetric monoidal structure by proving some simpler axioms. This idea has been used in TriJoin.v to show the associativity of join for example. *)
Section TwistConstruction.
(** The aim of this section is to build a symmetric monoidal category. We do this piecewise so that the separate steps are useful in and of themselves.
Our basic starting assumption is that we have a category with equivalences, a bifunctor called the tensor product, and a unit object.*)
Context (A : Type) `{HasEquivs A}
(cat_tensor : A -> A -> A) (cat_tensor_unit : A)
`{!Is0Bifunctor cat_tensor, !Is1Bifunctor cat_tensor}
(** Next we postulate the existence of a [braid] map. This takes a tensor pair and swaps the factors. We also postulate that [braid] is natural in both factors and self-inverse. *)
(braid : SymmetricBraiding cat_tensor)
(** We postulate the existence of a [twist] map. This takes a right associated triple [(A, (B, C))] and swaps the first two factors [(B, (A, C)]. We also postulate that [twist] is natural in all three factors and self-inverse. *)
(twist : forall a b c, cat_tensor a (cat_tensor b c) $-> cat_tensor b (cat_tensor a c))
(twist_twist : forall a b c, twist a b c $o twist b a c $== Id _)
(twist_nat : forall a a' b b' c c' (f : a $-> a') (g : b $-> b') (h : c $-> c'),
twist a' b' c' $o fmap11 cat_tensor f (fmap11 cat_tensor g h)
$== fmap11 cat_tensor g (fmap11 cat_tensor f h) $o twist a b c)
(** We assume that there is a natural isomorphism [right_unitor] witnessing the right unit law. The left unit law will be derived from this one. We also assume a coherence called [twist_unitor] which determines how the right_unitor interacts with [braid] and [twist]. This is the basis of the triangle axiom. *)
(right_unitor : RightUnitor cat_tensor cat_tensor_unit)
(twist_unitor : forall a b, fmap01 cat_tensor a (right_unitor b)
$== braid b a $o fmap01 cat_tensor b (right_unitor a) $o twist a b cat_tensor_unit)
(** The hexagon identity is about the interaction of associators and braids. We will derive this axiom from an analogous one for twists and braids. *)
(twist_hexagon : forall a b c,
fmap01 cat_tensor c (braid b a) $o twist b c a $o fmap01 cat_tensor b (braid a c)
$== twist a c b $o fmap01 cat_tensor a (braid b c) $o twist b a c)
(** The 9-gon identity. TODO: explain this *)
(twist_9_gon : forall a b c d,
fmap01 cat_tensor c (braid (cat_tensor a b) d)
$o twist (cat_tensor a b) c d
$o braid (cat_tensor c d) (cat_tensor a b)
$o twist a (cat_tensor c d) b
$o fmap01 cat_tensor a (braid b (cat_tensor c d))
$== fmap01 cat_tensor c (twist a d b)
$o fmap01 cat_tensor c (fmap01 cat_tensor a (braid b d))
$o twist a c (cat_tensor b d)
$o fmap01 cat_tensor a (twist b c d))
.
(** *** Setup *)
(** Before starting the proofs, we need to setup some useful definitions and helpful lemmas for working with diagrams. *)
(** We give notations and abbreviations to the morphisms that will appear in diagrams. This helps us read the goal and understand what is happening, otherwise it is too verbose. *)
Declare Scope monoidal_scope.
Local Infix "⊗" := cat_tensor (at level 40) : monoidal_scope.
Local Infix "⊗R" := (fmap01 cat_tensor) (at level 40) : monoidal_scope.
Local Infix "⊗L" := (fmap10 cat_tensor) (at level 40) : monoidal_scope.
Local Notation "f ∘ g" := (f $o g) (at level 61, left associativity, format "f '/' '∘' g") : monoidal_scope.
(** TODO: in 8.19 this notation causes issues, when updating to 8.20 we should uncomment this. *)
(* Local Notation "f $== g :> A" := (GpdHom (A := A) f g)
(at level 70, format "'[v' '[v' f ']' '/' $== '/' '[v' g ']' '/' :> '[' A ']' ']'")
: long_path_scope. *)
Local Open Scope monoidal_scope.
(** [twist] is an equivalence which we will call [twiste]. *)
Local Definition twiste a b c
: cat_tensor a (cat_tensor b c) $<~> cat_tensor b (cat_tensor a c)
:= cate_adjointify (twist a b c) (twist b a c)
(twist_twist a b c) (twist_twist b a c).
(** *** Finer naturality *)
(** The naturality postulates we have for [twist] are natural in all their arguments simultaneously. We show the finer naturality of [twist] in each argument separately as this becomes more useful in practice. *)
Definition twist_nat_l {a a'} (f : a $-> a') b c
: twist a' b c $o fmap10 cat_tensor f (cat_tensor b c)
$== fmap01 cat_tensor b (fmap10 cat_tensor f c) $o twist a b c.
refine ((_ $@L _^$) $@ twist_nat a a' b b c c f (Id _) (Id _) $@ (_ $@R _)).
refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
Definition twist_nat_m a {b b'} (g : b $-> b') c
: twist a b' c $o fmap01 cat_tensor a (fmap10 cat_tensor g c)
$== fmap10 cat_tensor g (cat_tensor a c) $o twist a b c.
refine ((_ $@L _^$) $@ twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)).
refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
Definition twist_nat_r a b {c c'} (h : c $-> c')
: twist a b c' $o fmap01 cat_tensor a (fmap01 cat_tensor b h)
$== fmap01 cat_tensor b (fmap01 cat_tensor a h) $o twist a b c.
refine ((_ $@L _^$) $@ twist_nat a a b b c c' (Id _) (Id _) h $@ (_ $@R _)).
refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
(** *** Movement lemmas *)
(** Here we collect lemmas about moving morphisms around in a diagram. We could have created [cate_moveL_eM]-style lemmas for [CatIsEquiv] but this leads to a lot of unnecessary unfolding and duplication. It is typically easier to use a hand crafted lemma for each situation. *)
(** TODO: A lot of these proofs are copy and pasted between lemmas. We need to work out an efficient way of proving them. *)
(** **** Moving [twist] *)
Definition moveL_twistL a b c d f (g : d $-> _)
: twist a b c $o f $== g -> f $== twist b a c $o g.
apply (cate_monic_equiv (twiste a b c)).
nrefine ((cate_buildequiv_fun _ $@R _) $@ p $@ _ $@ cat_assoc _ _ _).
refine ((cat_idl _)^$ $@ (_^$ $@R _)).
refine ((cate_buildequiv_fun _ $@R _) $@ _).
Definition moveL_twistR a b c d f (g : _ $-> d)
: f $o twist a b c $== g -> f $== g $o twist b a c.
apply (cate_epic_equiv (twiste a b c)).
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ (_ $@L ((_ $@L cate_buildequiv_fun _) $@ _)^$)).
refine ((_ $@L _) $@ _ $@ (cat_idr _)^$).
1: apply cate_buildequiv_fun.
Definition moveR_twistL a b c d f (g : d $-> _)
: f $== twist b a c $o g -> twist a b c $o f $== g.
intros p; symmetry; apply moveL_twistL; symmetry; exact p.
Definition moveR_twistR a b c d f (g : _ $-> d)
: f $== g $o twist b a c -> f $o twist a b c $== g.
intros p; symmetry; apply moveL_twistR; symmetry; exact p.
Definition moveL_fmap01_twistL a b c d e f (g : e $-> _)
: fmap01 cat_tensor a (twist b c d) $o f $== g
-> f $== fmap01 cat_tensor a (twist c b d) $o g.
apply (cate_monic_equiv (emap01 cat_tensor a (twiste b c d))).
refine (_ $@ cat_assoc _ _ _).
refine (_ $@ (_^$ $@R _)).
2: apply cate_buildequiv_fun.
refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
refine (_^$ $@ (_^$ $@R _)).
2: apply cate_buildequiv_fun.
refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
apply cate_buildequiv_fun.
Definition moveL_fmap01_twistR a b c d e f (g : _ $-> e)
: f $o fmap01 cat_tensor a (twist b c d) $== g
-> f $== g $o fmap01 cat_tensor a (twist c b d).
apply (cate_epic_equiv (emap01 cat_tensor a (twiste b c d))).
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_^$ $@ (_ $@L _^$)).
2: apply cate_buildequiv_fun.
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
1: apply cate_buildequiv_fun.
refine ((_ $@L _) $@ p $@ (cat_idr _)^$).
refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
apply cate_buildequiv_fun.
Definition moveR_fmap01_twistL a b c d e f (g : e $-> _)
: f $== fmap01 cat_tensor a (twist c b d) $o g
-> fmap01 cat_tensor a (twist b c d) $o f $== g.
intros p; symmetry; apply moveL_fmap01_twistL; symmetry; exact p.
Definition moveR_fmap01_twistR a b c d e f (g : _ $-> e)
: f $== g $o fmap01 cat_tensor a (twist c b d)
-> f $o fmap01 cat_tensor a (twist b c d) $== g.
intros p; symmetry; apply moveL_fmap01_twistR; symmetry; exact p.
(** *** The associator *)
(** Using [braide] and [twiste] we can build an associator. *)
Definition associator_twist' a b c
: cat_tensor a (cat_tensor b c) $<~> cat_tensor (cat_tensor a b) c.
(** We can build the associator out of [braide] and [twiste]. *)
refine (braide _ _ $oE _).
nrefine (twiste _ _ _ $oE _).
exact (emap01 cat_tensor a (braide _ _)).
(** We would like to be able to unfold [associator_twist'] to the underlying morphisms. We use this lemma to make that process easier. *)
Definition associator_twist'_unfold a b c
: cate_fun (associator_twist' a b c)
$== braid c (cat_tensor a b) $o (twist a c b $o fmap01 cat_tensor a (braid b c)).
refine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)).
nrefine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)).
refine (cate_buildequiv_fun _ $@ fmap2 _ _).
apply cate_buildequiv_fun.
(** Now we can use [associator_twist'] and show that it is a natural equivalence in each variable. *)
Instance associator_twist : Associator cat_tensor.
snapply Build_Associator.
snapply Build_Is1Natural.
simpl; intros [[a b] c] [[a' b'] c'] [[f g] h]; simpl in f, g, h.
(** To prove naturality it will be easier to reason about squares. *)
change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
(** First we remove all the equivalences from the equation. *)
1: apply associator_twist'_unfold.
2: apply associator_twist'_unfold.
(** The first square involving [braid] on its own is a naturality square. *)
(** The second square is just the naturality of twist. *)
1,3: symmetry; rapply fmap01_is_fmap11.
(** Leaving us with a square with a functor application. *)
(** We are finally left with the naturality of braid. *)
(** We abbreviate the associator to [α] for the remainder of the section. *)
Local Notation α := associator_twist.
(** *** Unitors *)
(** Since we assume the [right_unitor] exists, we can derive the [left_unitor] from it together with [braid]. *)
Instance left_unitor_twist : LeftUnitor cat_tensor cat_tensor_unit.
exact (fun a => right_unitor a $o braid cat_tensor_unit a).
snapply Build_Is1Natural.
change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
2: exact (isnat right_unitor f).
(** *** Triangle *)
(** The triangle identity can easily be proven by rearranging the diagram, cancelling and using naturality of [braid]. *)
Instance triangle_twist : TriangleIdentity cat_tensor cat_tensor_unit.
refine (_ $@ (_ $@L _)^$).
2: apply associator_twist'_unfold.
refine (fmap02 _ a (cate_buildequiv_fun _) $@ _); cbn.
refine (fmap01_comp _ _ _ _ $@ _).
do 2 refine (_ $@ cat_assoc _ _ _).
refine ((twist_unitor _ _ $@ (_ $@R _)) $@R _).
Local Open Scope long_path_scope.
Instance pentagon_twist : PentagonIdentity cat_tensor.
clear twist_unitor right_unitor cat_tensor_unit.
refine ((_ $@@ _) $@ _ $@ ((fmap02 _ _ _ $@ _)^$ $@@ (_ $@@ (fmap20 _ _ _ $@ _))^$)).
1,2,4,6,7: apply associator_twist'_unfold.
2: exact (fmap01_comp _ _ _ _ $@ (_ $@L (fmap01_comp _ _ _ _))).
2: exact (fmap10_comp _ _ _ _ $@ (_ $@L (fmap10_comp _ _ _ _))).
(** We use a notation defined above that shows the base type of the groupoid hom and formats the equation in a way that is easier to read. *)
(** Normalize brackets on LHS *)
refine (cat_assoc _ _ _ $@ _).
refine (_ $@L (cat_assoc _ _ _) $@ _).
do 4 refine ((cat_assoc _ _ _)^$ $@ _).
(** Normalize brackets on RHS *)
refine (_ $@ (((cat_assoc _ _ _) $@R _) $@R _)).
do 2 refine (_ $@ ((cat_assoc _ _ _) $@R _)).
do 2 refine (_ $@ cat_assoc _ _ _).
(** Cancel two braids next to each other. *)
apply moveL_fmap01_fmap01_braidR.
apply moveL_fmap01_twistR.
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ ((_ $@L _) $@ cat_idr _)^$).
2: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_id _ _ _).
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ cat_assoc _ _ _).
apply moveL_fmap01_fmap01_braidR.
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ cat_assoc _ _ _).
apply moveL_fmap01_twistR.
(** Putting things back. *)
apply moveR_fmap01_twistR.
apply moveR_fmap01_fmap01_braidR.
apply moveR_fmap01_twistR.
(** There are two braids on the RHS of the LHS that can be swapped. *)
refine (cat_assoc _ _ _ $@ _).
1: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_comp _ _ _ _).
refine ((cat_assoc _ _ _)^$ $@ _).
apply moveR_fmap01_braidR.
(** Naturality of twist on the RHS of the LHS. *)
refine (cat_assoc _ _ _ $@ _).
refine ((cat_assoc _ _ _)^$ $@ _).
(** Moving some things to the RHS so that we can braid and cancel on the LHS. *)
refine (cat_assoc _ _ _ $@ _).
refine ((cat_assoc _ _ _)^$ $@ _).
refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L _) $@ cat_idr _ $@ _).
1: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_id _ _ _).
apply moveL_fmap01_braidR.
(** We are almost at the desired 9-gon. Now we cancel the inner braid on the LHS. *)
do 4 refine (_ $@ (cat_assoc _ _ _)^$).
do 3 refine (cat_assoc _ _ _ $@ _).
do 4 refine (_ $@ cat_assoc _ _ _).
refine ((cat_assoc _ _ _)^$ $@ _).
(** Now we move terms around in order to get a homotopy in [a ⊗ (b ⊗ (d ⊗ c)) $-> d ⊗ (c ⊗ (a ⊗ b))]. *)
apply moveL_fmap01_twistR.
do 2 refine (_ $@ (cat_assoc _ _ _)^$).
do 3 refine (cat_assoc _ _ _ $@ _).
refine (_ $@ cat_assoc _ _ _).
do 4 refine ((cat_assoc _ _ _)^$ $@ _).
apply moveR_fmap01_twistR.
do 3 refine (_ $@ (cat_assoc _ _ _)^$).
do 2 refine (cat_assoc _ _ _ $@ _).
apply moveL_fmap01_braidL.
do 2 refine (_ $@ cat_assoc _ _ _).
do 3 refine ((cat_assoc _ _ _)^$ $@ _).
(** And finally, this is the 9-gon we asked for. *)
Local Close Scope long_path_scope.
Instance hexagon_twist : HexagonIdentity cat_tensor.
refine (((_ $@L _) $@R _) $@ _ $@ (_ $@@ (_ $@R _))^$).
1,3,4: apply associator_twist'_unfold.
do 2 refine (((cat_assoc _ _ _)^$ $@R _) $@ _).
refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
refine (_ $@ cat_assoc _ _ _).
refine (_ $@ ((cat_assoc _ _ _)^$ $@R _)).
refine (_ $@ (((cat_idr _)^$ $@ (_ $@L _^$)) $@R _)).
refine (((braid_nat_r _)^$ $@R _) $@ _).
refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$).
refine (_ $@ cat_assoc _ _ _).
apply moveL_fmap01_braidR.
(** *** Conclusion *)
(** In conclusion, we have proven the following: *)
(** There is a monoidal structure on [A]. *)
Instance ismonoidal_twist
: IsMonoidal A cat_tensor cat_tensor_unit
:= {}.
(** There is a symmetric monoidal category on [A]. *)
Instance issymmetricmonoidal_twist
: IsSymmetricMonoidal A cat_tensor cat_tensor_unit
:= {}.
(** TODO: WIP *)
(** Here is a hexagon involving only twist *)
Definition twist_hex' a b c d
: fmap01 cat_tensor c (twist a b d)
$o twist a c (cat_tensor b d)
$o fmap01 cat_tensor a (twist b c d)
$== twist b c (cat_tensor a d)
$o fmap01 cat_tensor b (twist a c d)
$o twist a b (cat_tensor c d).
pose proof (twist_hexagon c a d $@ cat_assoc _ _ _) as p.
apply moveR_fmap01_braidL in p.
apply (fmap02 cat_tensor b) in p.
refine (_ $@ ((_ $@L p) $@R _)); clear p.
refine (_ $@ (fmap01_comp _ _ _ _)^$).
refine (_ $@ cat_assoc _ _ _).