Timings for Monoidal.v
Require Import Basics.Overture Basics.Tactics Types.Forall.
Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv.
Require Import WildCat.NatTrans WildCat.Square.
(** * Monoidal Categories *)
(** In this file we define monoidal categories and symmetric monoidal categories. *)
(** ** Typeclasses for common diagrams *)
(** TODO: These should eventually be moved to a separate file in WildCat and used in other places. They can be thought of as a wildcat generalization of the classes in canonical_names.v *)
(** *** Associators *)
(** A natural equivalence witnessing the associativity of a bifunctor. *)
Class Associator {A : Type} `{HasEquivs A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
(** An isomorphism [associator] witnessing associativity of [F]. *)
associator a b c : F a (F b c) $<~> F (F a b) c;
(** The [associator] is a natural isomorphism. *)
is1natural_associator_uncurried
:: Is1Natural
(fun '(a, b, c) => F a (F b c))
(fun '(a, b, c) => F (F a b) c)
(fun '(a, b, c) => associator a b c);
}.
Coercion associator : Associator >-> Funclass.
Arguments associator {A _ _ _ _ _ F _ _ _} a b c.
Class LeftUnitor {A : Type} `{HasEquivs A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (unit : A)
(** A natural isomorphism [left_unitor] witnessing the left unit law of [F]. *)
:= left_unitor : NatEquiv (F unit) idmap.
Coercion left_unitor : LeftUnitor >-> NatEquiv.
Arguments left_unitor {A _ _ _ _ _ F _ _ unit _}.
Class RightUnitor {A : Type} `{HasEquivs A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (unit : A)
(** A natural isomorphism [right_unitor] witnessing the right unit law of [F]. *)
:= right_unitor : NatEquiv (flip F unit) idmap.
Coercion right_unitor : RightUnitor >-> NatEquiv.
Arguments right_unitor {A _ _ _ _ _ F _ _ unit _}.
(** *** Triangle and Pentagon identities *)
Class TriangleIdentity {A : Type} `{HasEquivs A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
(unit : A) `{!LeftUnitor F unit, !RightUnitor F unit}
(** The triangle identity for an associator and unitors. *)
:= triangle_identity a b
: fmap01 F a (left_unitor b)
$== fmap10 F (right_unitor a) b $o (associator (F := F) a unit b).
Coercion triangle_identity : TriangleIdentity >-> Funclass.
Arguments triangle_identity {A _ _ _ _ _} F {_ _ _} unit {_}.
Class PentagonIdentity {A : Type} `{HasEquivs A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
(** The pentagon identity for an associator. *)
:= pentagon_identity a b c d
: associator (F a b) c d $o associator a b (F c d)
$== fmap10 F (associator a b c) d $o associator a (F b c) d
$o fmap01 F a (associator b c d).
Coercion pentagon_identity : PentagonIdentity >-> Funclass.
Arguments pentagon_identity {A _ _ _ _ _} F {_ _ _}.
Class Braiding {A : Type} `{Is1Cat A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
(** A morphism [braid] witnessing the symmetry of [F]. *)
braid a b : F a b $-> F b a;
(** The [braid] is a natural transformation. *)
is1natural_braiding_uncurried
: Is1Natural
(uncurry F)
(uncurry (flip F))
(fun '(a, b) => braid a b);
}.
Coercion braid : Braiding >-> Funclass.
Arguments braid {A _ _ _ _ F _ _ _} a b.
Class SymmetricBraiding {A : Type} `{Is1Cat A}
(F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
braiding_symmetricbraiding :: Braiding F;
braid_braid : forall a b, braid a b $o braid b a $== Id (F b a);
}.
(** We could have used [::>] in [braiding_symmetricbraiding] instead however due to bug https://github.com/coq/coq/issues/18971 the coercion isn't registered, so we have to register it manually instead. *)
Coercion braiding_symmetricbraiding : SymmetricBraiding >-> Braiding.
Arguments braid_braid {A _ _ _ _ F _ _ _} a b.
(** *** Hexagon identity *)
Class HexagonIdentity {A : Type} `{HasEquivs A}
(F : A -> A -> A)
`{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F, !Braiding F}
(** The hexagon identity for an associator and a braiding. *)
:= hexagon_identity a b c
: fmap10 F (braid b a) c $o associator b a c $o fmap01 F b (braid c a)
$== associator a b c $o braid (F b c) a $o associator b c a.
Coercion hexagon_identity : HexagonIdentity >-> Funclass.
Arguments hexagon_identity {A _ _ _ _ _} F {_ _}.
(** ** Monoidal Categories *)
(** A monoidal 1-category is a 1-category with equivalences together with the following: *)
Class IsMonoidal (A : Type) `{HasEquivs A}
(** It has a binary operation [cat_tensor] called the tensor product. *)
(cat_tensor : A -> A -> A)
(** It has a unit object [cat_tensor_unit] called the tensor unit. *)
(cat_tensor_unit : A)
(** These all satisfy the following properties: *)
:= {
(** A [cat_tensor] is a 1-bifunctor. *)
is0bifunctor_cat_tensor :: Is0Bifunctor cat_tensor;
is1bifunctor_cat_tensor :: Is1Bifunctor cat_tensor;
(** A natural isomorphism [associator] witnessing the associativity of the tensor product. *)
cat_tensor_associator :: Associator cat_tensor;
(** A natural isomorphism [left_unitor] witnessing the left unit law. *)
cat_tensor_left_unitor :: LeftUnitor cat_tensor cat_tensor_unit;
(** A natural isomorphism [right_unitor] witnessing the right unit law. *)
cat_tensor_right_unitor :: RightUnitor cat_tensor cat_tensor_unit;
(** The triangle identity. *)
cat_tensor_triangle_identity :: TriangleIdentity cat_tensor cat_tensor_unit;
(** The pentagon identity. *)
cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor;
}.
(** TODO: Braided monoidal categories *)
(** ** Symmetric Monoidal Categories *)
(** A symmetric monoidal 1-category is a 1-category with equivalences together with the following: *)
Class IsSymmetricMonoidal (A : Type) `{HasEquivs A}
(** A binary operation [cat_tensor] called the tensor product. *)
(cat_tensor : A -> A -> A)
(** A unit object [cat_tensor_unit] called the tensor unit. *)
(cat_tensor_unit : A)
:= {
(** A monoidal structure with [cat_tensor] and [cat_tensor_unit]. *)
issymmetricmonoidal_ismonoidal :: IsMonoidal A cat_tensor cat_tensor_unit;
(** A natural transformation [braid] witnessing the symmetry of the tensor product such that [braid] is its own inverse. *)
cat_symm_tensor_braiding :: SymmetricBraiding cat_tensor;
(** The hexagon identity. *)
cat_symm_tensor_hexagon :: HexagonIdentity cat_tensor;
}.
(** *** Theory about [Associator] *)
Context {A : Type} {F : A -> A -> A} `{assoc : Associator A F, !HasEquivs A}.
Local Definition associator_nat {x x' y y' z z'}
(f : x $-> x') (g : y $-> y') (h : z $-> z')
: associator x' y' z' $o fmap11 F f (fmap11 F g h)
$== fmap11 F (fmap11 F f g) h $o associator x y z.
destruct assoc as [asso nat].
exact (nat (x, y, z) (x', y', z') (f, g, h)).
Local Definition associator_nat_l {x x' : A} (f : x $-> x') (y z : A)
: associator x' y z $o fmap10 F f (F y z)
$== fmap10 F (fmap10 F f y) z $o associator x y z.
refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
2: rapply (associator_nat f (Id _) (Id _)).
exact (fmap12 _ _ (fmap11_id _ _ _) $@ fmap10_is_fmap11 _ _ _).
exact (fmap21 _ (fmap10_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
Local Definition associator_nat_m (x : A) {y y' : A} (g : y $-> y') (z : A)
: associator x y' z $o fmap01 F x (fmap10 F g z)
$== fmap10 F (fmap01 F x g) z $o associator x y z.
refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
2: nrapply (associator_nat (Id _) g (Id _)).
exact (fmap12 _ _ (fmap10_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
exact (fmap21 _ (fmap01_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
Local Definition associator_nat_r (x y : A) {z z' : A} (h : z $-> z')
: associator x y z' $o fmap01 F x (fmap01 F y h)
$== fmap01 F (F x y) h $o associator x y z.
refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
2: nrapply (associator_nat (Id _) (Id _) h).
exact (fmap12 _ _ (fmap01_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
exact (fmap21 _ (fmap11_id _ _ _) _ $@ fmap01_is_fmap11 F _ _).
(** ** Theory about [SymmetricBraid] *)
Context {A : Type} {F : A -> A -> A} `{SymmetricBraiding A F, !HasEquivs A}.
(** [braid] is its own inverse and therefore an equivalence. *)
Local Instance catie_braid a b : CatIsEquiv (braid a b)
:= catie_adjointify (braid a b) (braid b a) (braid_braid a b) (braid_braid b a).
(** [braide] is the bundled equivalence whose underlying map is [braid]. *)
Local Definition braide a b
: F a b $<~> F b a
:= Build_CatEquiv (braid a b).
Local Definition moveL_braidL a b c f (g : c $-> _)
: braid a b $o f $== g -> f $== braid b a $o g.
apply (cate_monic_equiv (braide a b)).
refine ((cate_buildequiv_fun _ $@R _) $@ p $@ _ $@ cat_assoc _ _ _).
refine ((cat_idl _)^$ $@ (_^$ $@R _)).
refine ((cate_buildequiv_fun _ $@R _) $@ _).
Local Definition moveL_braidR a b c f (g : _ $-> c)
: f $o braid a b $== g -> f $== g $o braid b a.
apply (cate_epic_equiv (braide a b)).
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ (_ $@L ((_ $@L cate_buildequiv_fun _) $@ _)^$)).
refine ((_ $@L _) $@ _ $@ (cat_idr _)^$).
1: apply cate_buildequiv_fun.
Local Definition moveR_braidL a b c f (g : c $-> _)
: f $== braid b a $o g -> braid a b $o f $== g.
intros p; symmetry; apply moveL_braidL; symmetry; exact p.
Local Definition moveR_braidR a b c f (g : _ $-> c)
: f $== g $o braid b a -> f $o braid a b $== g.
intros p; symmetry; apply moveL_braidR; symmetry; exact p.
Local Definition moveL_fmap01_braidL a b c d f (g : d $-> _)
: fmap01 F a (braid b c) $o f $== g
-> f $== fmap01 F a (braid c b) $o g.
apply (cate_monic_equiv (emap01 F a (braide b c))).
refine (_ $@ cat_assoc _ _ _).
refine (_ $@ (_^$ $@R _)).
2: apply cate_buildequiv_fun.
refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
refine ((_ $@R _) $@ _)^$.
1: apply cate_buildequiv_fun.
refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
refine (_ $@ fmap2 _ _);
apply cate_buildequiv_fun.
Local Definition moveL_fmap01_braidR a b c d f (g : _ $-> d)
: f $o fmap01 F a (braid b c) $== g
-> f $== g $o fmap01 F a (braid c b).
apply (cate_epic_equiv (emap01 F a (braide b c))).
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 (_ $@ fmap2 _ _);
apply cate_buildequiv_fun.
Local Definition moveR_fmap01_braidL a b c d f (g : d $-> _)
: f $== fmap01 F a (braid c b) $o g
-> fmap01 F a (braid b c) $o f $== g.
intros p; symmetry; apply moveL_fmap01_braidL; symmetry; exact p.
Local Definition moveR_fmap01_braidR a b c d f (g : _ $-> d)
: f $== g $o fmap01 F a (braid c b)
-> f $o fmap01 F a (braid b c) $== g.
intros p; symmetry; apply moveL_fmap01_braidR; symmetry; exact p.
Local Definition moveL_fmap01_fmap01_braidL a b c d e f (g : e $-> _)
: fmap01 F a (fmap01 F b (braid c d)) $o f $== g
-> f $== fmap01 F a (fmap01 F b (braid d c)) $o g.
apply (cate_monic_equiv (emap01 F a (emap01 F b (braide 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 ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
refine ((_ $@R _) $@ _)^$.
1: apply cate_buildequiv_fun.
refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
apply cate_buildequiv_fun.
Local Definition moveL_fmap01_fmap01_braidR a b c d e f (g : _ $-> e)
: f $o fmap01 F a (fmap01 F b (braid c d)) $== g
-> f $== g $o fmap01 F a (fmap01 F b (braid d c)).
apply (cate_epic_equiv (emap01 F a (emap01 F b (braide c d)))).
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_^$ $@ (_ $@L _^$)).
2: apply cate_buildequiv_fun.
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
1: 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 _ _ _).
refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
apply cate_buildequiv_fun.
Local Definition moveR_fmap01_fmap01_braidL a b c d e f (g : e $-> _)
: f $== fmap01 F a (fmap01 F b (braid d c)) $o g
-> fmap01 F a (fmap01 F b (braid c d)) $o f $== g.
intros p; symmetry; apply moveL_fmap01_fmap01_braidL; symmetry; exact p.
Local Definition moveR_fmap01_fmap01_braidR a b c d e f (g : _ $-> e)
: f $== g $o fmap01 F a (fmap01 F b (braid d c))
-> f $o fmap01 F a (fmap01 F b (braid c d)) $== g.
intros p; symmetry; apply moveL_fmap01_fmap01_braidR; symmetry; exact p.
Local Definition braid_nat {a b c d} (f : a $-> c) (g : b $-> d)
: braid c d $o fmap11 F f g $== fmap11 F g f $o braid a b.
exact (is1natural_braiding_uncurried (a, b) (c, d) (f, g)).
Local Definition braid_nat_l {a b c} (f : a $-> b)
: braid b c $o fmap10 F f c $== fmap01 F c f $o braid a c.
refine ((_ $@L (fmap10_is_fmap11 _ _ _)^$) $@ _ $@ (fmap01_is_fmap11 _ _ _ $@R _)).
exact (is1natural_braiding_uncurried (a, c) (b, c) (f, Id _)).
(** This is just the inverse of above. *)
Local Definition braid_nat_r {a b c} (g : b $-> c)
: braid a c $o fmap01 F a g $== fmap10 F g a $o braid a b.
refine ((_ $@L (fmap01_is_fmap11 _ _ _)^$) $@ _ $@ (fmap10_is_fmap11 _ _ _ $@R _)).
exact (is1natural_braiding_uncurried (a, b) (a, c) (Id _ , g)).
(** ** 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.
Local Notation "f $== g :> A" := (GpdHom (A := A) f g)
(at level 80, 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 similtaneously. We show the finer naturality of [twist] in each argument separately as this becomes more useful in practice. *)
Local 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 _ _ _).
Local 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 _ _ _).
Local 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] *)
Local 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 _) $@ _).
Local 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.
Local 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.
Local 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.
Local 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.
Local 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.
Local 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.
Local 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. *)
Local 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. *)
Local 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. *)
Local Instance associator_twist : Associator cat_tensor.
snrapply Build_Associator.
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]. *)
Local Instance left_unitor_twist : LeftUnitor cat_tensor cat_tensor_unit.
snrapply Build_NatEquiv'.
exact (fun a => right_unitor a $o braid cat_tensor_unit a).
change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
2: rapply (isnat right_unitor f).
(** *** Triangle *)
(** The triangle identity can easily be proven by rearranging the diagram, cancelling and using naturality of [braid]. *)
Local 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.
Local 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: refine (fmap01_comp _ _ _ _ $@ (_ $@L (fmap01_comp _ _ _ _))).
2: refine (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 eachother. *)
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.
Local 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]. *)
Local Instance ismonoidal_twist
: IsMonoidal A cat_tensor cat_tensor_unit
:= {}.
(** There is a symmetric monoidal category on [A]. *)
Local 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 _ _ _).