monoids and comonoids in a monoidal category

theories/Algebra/Categorical/MonoidObject.v

@@ -0,0 +1,197 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor
+  WildCat.NatTrans WildCat.Opposite WildCat.Products.
+Require Import abstract_algebra.
+
+(** * Monoids and Comonoids *)
+
+(** Here we define a monoid internal to a monoidal category. Various algebraic theories such as groups and rings may also be internalized, however these specifically require a cartesian monoidal structure. The theory of monoids however has no such requirement and can therefore be developed in much greater generality. This can be used to define a range of objects such as R-algebras, H-spaces, Hopf algebras and more. *)
+
+(** * Monoid objects *)
+
+Section MonoidObject.
+  Context {A : Type} {tensor : A -> A -> A} {unit : A}
+    `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
+    `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.
+
+  (** An object [x] of [A] is a monoid object if it comes with the following data: *)
+  Class IsMonoidObject (x : A) := {
+    (** A multiplication map from the tensor product of [x] with itself to [x]. *)
+    mo_mult : tensor x x $-> x;
+    (** A unit of the multplication. *)
+    mo_unit : unit $-> x;
+    (** The multiplication map is associative. *)
+    mo_assoc : mo_mult $o fmap10 tensor mo_mult x $o associator x x x
+        $== mo_mult $o fmap01 tensor x mo_mult;
+    (** The multiplication map is left unital. *)
+    mo_left_unit : mo_mult $o fmap10 tensor mo_unit x $== left_unitor x;
+    (** The multiplication map is right unital. *)
+    mo_right_unit : mo_mult $o fmap01 tensor x mo_unit $== right_unitor x;
+  }.
+
+  Context `{!Braiding tensor}.
+
+  (** An object [x] of [A] is a commutative monoid object if: *)
+  Class IsCommutativeMonoidObject (x : A) := {
+    (** It is a monoid object. *)
+    cmo_mo :: IsMonoidObject x;
+    (** The multiplication map is commutative. *)
+    cmo_comm : mo_mult $o braid x x $== mo_mult;
+  }.
+
+End MonoidObject.
+
+Arguments IsMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _} x.
+Arguments IsCommutativeMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _ _} x.
+
+Section ComonoidObject.
+  Context {A : Type} (tensor : A -> A -> A) (unit : A)
+    `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
+    `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.
+
+  (** A comonoid object is a monoid object in the opposite category. *)
+  Class IsComonoidObject (x : A)
+    := ismonoid_comonoid_op :: IsMonoidObject (A:=A^op) tensor unit x.
+
+  (** We can build comonoid objects from the following data: *)
+  Definition Build_IsComonoidObject (x : A)
+    (** A comultplication map. *)
+    (co_comult : x $-> tensor x x)
+    (** A counit. *)
+    (co_counit : x $-> unit)
+    (** The comultiplication is coassociative. *)
+    (co_coassoc : associator x x x $o fmap01 tensor x co_comult $o co_comult
+        $== fmap10 tensor co_comult x $o co_comult)
+    (** The comultiplication is left counital. *)
+    (co_left_counit : left_unitor x $o fmap10 tensor co_counit x $o co_comult $== Id x)
+    (** The comultiplication is right counital. *)
+    (co_right_counit : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x)
+    : IsComonoidObject x.
+  Proof.
+    snrapply Build_IsMonoidObject.
+    - exact co_comult.
+    - exact co_counit.
+    - nrapply cate_moveR_eV.
+      symmetry.
+      nrefine (cat_assoc _ _ _ $@ _).
+      rapply co_coassoc.
+    - simpl; nrefine (_ $@ cat_idr _).
+      nrapply cate_moveL_Ve.
+      nrefine (cat_assoc_opp _ _ _ $@ _).
+      exact co_left_counit.
+    - simpl; nrefine (_ $@ cat_idr _).
+      nrapply cate_moveL_Ve.
+      nrefine (cat_assoc_opp _ _ _ $@ _).
+      exact co_right_counit.
+  Defined.
+
+  (** Comultiplication *)
+  Definition co_comult {x : A} `{!IsComonoidObject x} : x $-> tensor x x
+   := mo_mult (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x).
+
+  (** Counit *)
+  Definition co_counit {x : A} `{!IsComonoidObject x} : x $-> unit
+    := mo_unit (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x).
+
+  Context `{!Braiding tensor}.
+
+  (** A cocommutative comonoid objects is a commutative monoid object in the opposite category. *)
+  Class IsCocommutativeComonoidObject (x : A)
+    := iscommuatativemonoid_cocomutativemonoid_op
+      :: IsCommutativeMonoidObject (A:=A^op) tensor unit x.
+
+  (** We can build cocommutative comonoid objects from the following data: *)
+  Definition Build_IsCocommutativeComonoidObject (x : A)
+    (** A comonoid. *)
+    `{!IsComonoidObject x}
+    (** Together with a proof of cocommutativity. *)
+    (cco_cocomm : braid x x $o co_comult $== co_comult)
+    : IsCocommutativeComonoidObject x.
+  Proof.
+    snrapply Build_IsCommutativeMonoidObject.
+    - exact _.
+    - exact cco_cocomm.
+  Defined.
+
+End ComonoidObject.
+
+(** ** Monoid enrichment *)
+
+(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. Equivalently, a hom [x $-> y] in a cartesian category where [x] is a comonoid object has the structure of a monoid. *)
+
+Section MonoidEnriched.
+  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}
+    (unit : A) `{!IsTerminal unit} {x y : A}
+    `{!HasMorExt A} `{forall x y, IsHSet (x $-> y)}.
+
+  Section Monoid.
+    Context `{!IsMonoidObject _ _ y}.
+
+    Local Instance sgop_hom : SgOp (x $-> y)
+      := fun f g => mo_mult $o cat_binprod_corec f g.
+
+    Local Instance monunit_hom : MonUnit (x $-> y) := mo_unit $o mor_terminal _ _.
+
+    Local Instance associative_hom : Associative sgop_hom.
+    Proof.
+      intros f g h.
+      unfold sgop_hom.
+      rapply path_hom.
+      refine ((_ $@L cat_binprod_fmap01_corec _ _ _)^$ $@ _).
+      nrefine (cat_assoc_opp _ _ _ $@ _).
+      refine ((mo_assoc $@R _)^$ $@ _).
+      nrefine (_ $@ (_ $@L cat_binprod_fmap10_corec _ _ _)).
+      refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc _ _ _).
+      nrapply cat_binprod_associator_corec.
+    Defined.
+
+    Local Instance leftidentity_hom : LeftIdentity sgop_hom mon_unit.
+    Proof.
+      intros f.
+      unfold sgop_hom, mon_unit.
+      rapply path_hom.
+      refine ((_ $@L (cat_binprod_fmap10_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
+      nrefine (((mo_left_unit $@ _) $@R _) $@ _).
+      1: nrapply cate_buildequiv_fun.
+      unfold trans_nattrans.
+      nrefine ((((_ $@R _) $@ _) $@R _) $@ _).
+      1: nrapply cate_buildequiv_fun.
+      1: nrapply cat_binprod_beta_pr1.
+      nrapply cat_binprod_beta_pr2.
+    Defined.
+
+    Local Instance rightidentity_hom : RightIdentity sgop_hom mon_unit.
+    Proof.
+      intros f.
+      unfold sgop_hom, mon_unit.
+      rapply path_hom.
+      refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
+      nrefine (((mo_right_unit $@ _) $@R _) $@ _).
+      1: nrapply cate_buildequiv_fun.
+      nrapply cat_binprod_beta_pr1.
+    Defined.
+
+    Local Instance issemigroup_hom : IsSemiGroup (x $-> y) := {}.
+    Local Instance ismonoid_hom : IsMonoid (x $-> y) := {}.
+
+  End Monoid.
+
+  Context `{!IsCommutativeMonoidObject _ _ y}.
+  Local Existing Instances sgop_hom monunit_hom ismonoid_hom.
+
+  Local Instance commutative_hom : Commutative sgop_hom.
+  Proof.
+    intros f g.
+    unfold sgop_hom.
+    rapply path_hom.
+    refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _ $@ (cmo_comm $@R _)).
+    nrapply cat_binprod_swap_corec. 
+  Defined.
+
+  Local Instance iscommutativemonoid_hom : IsCommutativeMonoid (x $-> y) := {}.
+
+End MonoidEnriched.
+
+
+
+

theories/WildCat/Adjoint.v

@@ -388,7 +388,7 @@ Proof.
   snrapply Build_Adjunction_natequiv_nat_right.
   { intros y.
     refine (natequiv_compose (natequiv_adjunction_l adj _) _).
-    rapply (natequiv_postwhisker _ (natequiv_op _ _ e)). }
+    rapply (natequiv_postwhisker _ (natequiv_op e)). }
   intros x.
   rapply is1natural_comp.
 Defined.

theories/WildCat/Bifunctor.v

@@ -1,6 +1,7 @@
 Require Import Basics.Overture Basics.Tactics.
 Require Import Types.Forall Types.Prod.
-Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.Square.
+Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans
+  WildCat.Square WildCat.Opposite.
 
 (** * Bifunctors between WildCats *)
 
@@ -14,6 +15,11 @@
   is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
 }.
 
+Arguments Is0Bifunctor {A B C _ _ _} F.
+Arguments is0functor_bifunctor_uncurried {A B C _ _ _} F {_}.
+Arguments is0functor01_bifunctor {A B C _ _ _} F {_} a : rename.
+Arguments is0functor10_bifunctor {A B C _ _ _} F {_} b : rename.
+
 (** We provide two alternate constructors, allowing the user to provide just the first field or the last two fields. *)
 Definition Build_Is0Bifunctor' {A B C : Type}
   `{Is01Cat A, Is01Cat B, IsGraph C} (F : A -> B -> C)
@@ -32,7 +38,7 @@
   : Is0Bifunctor F.
 Proof.
   (* The first condition follows from [is0functor_prod_is0functor]. *)
   rapply Build_Is0Bifunctor.
 Defined.
 
 (** *** 1-functorial action *)
@@ -72,6 +78,9 @@
 
 Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
 Arguments Build_Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_} _ _ _ _ _.
+Arguments is1functor_bifunctor_uncurried {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _}.
+Arguments is1functor01_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} a : rename.
+Arguments is1functor10_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} b : rename.
 Arguments fmap11_is_fmap01_fmap10 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
   {Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.
 Arguments fmap11_is_fmap10_fmap01 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
@@ -285,14 +294,14 @@
   `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
   (F : A -> B -> C) {bf : Is0Bifunctor F}
   (G : C -> D) `{!Is0Functor G}
-  : Is0Bifunctor (fun a b => G (F a b))
+  : Is0Bifunctor (fun a b => G (F a b)) | 10
   := {}.
 
 Global Instance is1bifunctor_postcompose {A B C D : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
   (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
   `{!Is0Bifunctor F} {bf : Is1Bifunctor F}
-  : Is1Bifunctor (fun a b => G (F a b)).
+  : Is1Bifunctor (fun a b => G (F a b)) | 10.
 Proof.
   snrapply Build_Is1Bifunctor.
   1-3: exact _.
@@ -306,7 +315,7 @@
   `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E}
   (G : A -> B) (K : E -> C) (F : B -> C -> D)
   `{!Is0Functor G, !Is0Bifunctor F, !Is0Functor K}
-  : Is0Bifunctor (fun a b => F (G a) (K b)).
+  : Is0Bifunctor (fun a b => F (G a) (K b)) | 10.
 Proof.
   snrapply Build_Is0Bifunctor.
   - change (Is0Functor (uncurry F o functor_prod G K)).
@@ -322,7 +331,7 @@
   (G : A -> B) (K : E -> C) (F : B -> C -> D)
   `{!Is0Functor G, !Is1Functor G, !Is0Bifunctor F, !Is1Bifunctor F,
     !Is0Functor K, !Is1Functor K}
-  : Is1Bifunctor (fun a b => F (G a) (K b)).
+  : Is1Bifunctor (fun a b => F (G a) (K b)) | 10.
 Proof.
   snrapply Build_Is1Bifunctor.
   - change (Is1Functor (uncurry F o functor_prod G K)).
@@ -372,10 +381,8 @@
 (** We can show that an uncurried natural transformation between uncurried bifunctors by composing the naturality square in each variable. *)
 Global Instance is1natural_uncurry {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C)
-  `{!Is0Bifunctor F, !Is1Bifunctor F}
-  (G : A -> B -> C)
-  `{!Is0Bifunctor G, !Is1Bifunctor G}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  (G : A -> B -> C) `{!Is0Bifunctor G, !Is1Bifunctor G}
   (alpha : uncurry F $=> uncurry G)
   (nat_l : forall b, Is1Natural (flip F b) (flip G b) (fun x : A => alpha (x, b)))
   (nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y)))
@@ -389,3 +396,71 @@
   2: rapply (fmap11_is_fmap01_fmap10 G).
   exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
 Defined.
+
+(** Flipping a natural transformation between bifunctors. *)
+Definition nattrans_flip {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
+  : NatTrans (uncurry F) (uncurry (flip G))
+    -> NatTrans (uncurry (flip F)) (uncurry G).
+Proof.
+  intros [alpha nat].
+  snrapply Build_NatTrans.
+  - exact (alpha o equiv_prod_symm _ _).
+  - intros [b a] [b' a'] [g f].
+    exact (nat (a, b) (a', b') (f, g)).
+Defined.
+
+Definition nattrans_flip' {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
+  : NatTrans (uncurry (flip F)) (uncurry G)
+    -> NatTrans (uncurry F) (uncurry (flip G))
+  := nattrans_flip (F:=flip F) (G:=flip G).
+
+(** ** Opposite Bifunctors *)
+
+(** There are a few more combinations we can do for this, such as profunctors, but we will leave those for later. *)
+
+Global Instance is0bifunctor_op A B C (F : A -> B -> C) `{Is0Bifunctor A B C F}
+  : Is0Bifunctor (F : A^op -> B^op -> C^op).
+Proof.
+  snrapply Build_Is0Bifunctor.
+  - exact (is0functor_op _ _ (uncurry F)).
+  - intros a.
+    nrapply is0functor_op.
+    exact (is0functor01_bifunctor F a).
+  - intros b.
+    nrapply is0functor_op.
+    exact (is0functor10_bifunctor F b).
+Defined.
+
+Global Instance is1bifunctor_op A B C (F : A -> B -> C) `{Is1Bifunctor A B C F}
+  : Is1Bifunctor (F : A^op -> B^op -> C^op).
+Proof.
+  snrapply Build_Is1Bifunctor.
+  - exact (is1functor_op _ _ (uncurry F)).
+  - intros a.
+    nrapply is1functor_op.
+    exact (is1functor01_bifunctor F a).
+  - intros b.
+    nrapply is1functor_op.
+    exact (is1functor10_bifunctor F b).
+  - intros a0 a1 f b0 b1 g; cbn in f, g.
+    exact (fmap11_is_fmap10_fmap01 F f g).
+  - intros a0 a1 f b0 b1 g; cbn in f, g.
+    exact (fmap11_is_fmap01_fmap10 F f g).
+Defined.
+
+Global Instance is0bifunctor_op' A B C (F : A^op -> B^op -> C^op)
+  `{IsGraph A, IsGraph B, IsGraph C, Fop : !Is0Bifunctor (F : A^op -> B^op -> C^op)}
+  : Is0Bifunctor (F : A -> B -> C)
+  := is0bifunctor_op A^op B^op C^op F.
+
+Global Instance is1bifunctor_op' A B C (F : A^op -> B^op -> C^op)
+  `{Is1Cat A, Is1Cat B, Is1Cat C,
+    !Is0Bifunctor (F : A^op -> B^op -> C^op), !Is1Bifunctor (F : A^op -> B^op -> C^op)}
+  : Is1Bifunctor (F : A -> B -> C)
+  := is1bifunctor_op A^op B^op C^op F.

theories/WildCat/Equiv.v

@@ -413,6 +413,13 @@ Proof.
   apply cate_inv_adjointify.
 Defined.
 
+Definition cate_inv_compose' {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c)
+  : cate_fun (f $oE e)^-1$ $== e^-1$ $o f^-1$.
+Proof.
+  nrefine (_ $@ cate_buildequiv_fun _).
+  nrapply cate_inv_compose.
+Defined.
+
 Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
   : cate_fun (e^-1$)^-1$ $== cate_fun e.
 Proof.