Library UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids

In this file, the category of monoids internal to a monoidal category is defined

Note: after refactoring on March 10, 2023, the prior Git history of this development is found via git log -- UniMath/CategoryTheory/Monoidal/CategoriesOfMonoidsWhiskered.v (git log -- UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.v gives information on a prior development for the "tensored" format of monoidal categories)

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.Core.NaturalTransformations.

Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Import BifunctorNotations.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.

Local Open Scope cat.

Section Category_of_Monoids.

  Context {C : category} (M : monoidal C).

  Notation "x ⊗ y" := (x ⊗_{M } y).
  Notation "x ⊗l f" := (x ⊗^{M }_{l } f) (at level 31).
  Notation "f ⊗r y" := (f ⊗^{M }_{r } y) (at level 31).
  Notation "f ⊗⊗ g" := (f ⊗^{M } g) (at level 31).

  Let I : C := monoidal_unit M.
  Let lu : leftunitor_data M (monoidal_unit M) := monoidal_leftunitordata M.
  Let ru : rightunitor_data M (monoidal_unit M) := monoidal_rightunitordata M.
  Let α : associator_data M := monoidal_associatordata M.

  Definition monoid_data (x : C) : UU
    := C ⟦x ⊗ x , x ⟧ × C ⟦I , x ⟧.

  Definition monoid_data_multiplication {x : C} (m : monoid_data x)
    : C ⟦x ⊗ x , x ⟧
    := pr1 m.
  Notation "μ_{ m }" := (monoid_data_multiplication m).

  Definition monoid_data_unit {x : C} (m : monoid_data x)
    : C ⟦I , x ⟧
    := pr2 m.
  Notation "η_{ m }" := (monoid_data_unit m).

  Definition monoid_laws_assoc {x : C} (m : monoid_data x) : UU
    := α x x x · (x ⊗l μ_{m }) · μ_{m } = μ_{m } ⊗r x · μ_{m }.

  Definition monoid_laws_unit_left {x : C} (m : monoid_data x) : UU
    := (η_{m } ⊗r x ) · μ_{m } = lu x.
  Definition monoid_laws_unit_right {x : C} (m : monoid_data x) : UU
    := (x ⊗l η_{m }) · μ_{m } = ru x.

  Definition monoid_laws {x : C} (m : monoid_data x) : UU
    := monoid_laws_unit_left m × monoid_laws_unit_right m × monoid_laws_assoc m.

  Lemma isaprop_monoid_laws {x : C} (m : monoid_data x)
    : isaprop (monoid_laws m).
  Show proof.

repeat (apply isapropdirprod) ; apply homset_property.

  Definition monoid (x : C) : UU
    := ∑ m : monoid_data x , monoid_laws m.

  Definition make_monoid
    {x : C} (μ : C ⟦x ⊗ x , x ⟧) (η : C ⟦monoidal_unit M , x ⟧)
    (p_ul : (η ⊗r x ) · μ = lu x)
    (p_ur : (x ⊗l η ) · μ = ru x)
    (p_assoc : α x x x · (x ⊗l μ ) · μ = μ ⊗r x · μ)
    : monoid x.
  Show proof.

    simple refine ((_ ,, _) ,, (_ ,, _ ,, _)).
    - exact μ.
    - exact η.
    - exact p_ul.
    - exact p_ur.
    - exact p_assoc.

  Definition monoid_to_monoid_data {x : C} (m : monoid x)
    : monoid_data x := pr1 m.
  Coercion monoid_to_monoid_data : monoid >-> monoid_data.

  Definition monoid_to_monoid_laws {x : C} (m : monoid x)
    : monoid_laws m := pr2 m.

  Definition monoid_to_unit_left_law {x : C} (m : monoid x)
    : monoid_laws_unit_left m := pr1 (monoid_to_monoid_laws m).

  Definition monoid_to_unit_right_law {x : C} (m : monoid x)
    : monoid_laws_unit_right m := pr12 (monoid_to_monoid_laws m ).

  Definition monoid_to_assoc_law {x : C} (m : monoid x)
    : monoid_laws_assoc m := pr22 (monoid_to_monoid_laws m ).

  Definition is_monoid_mor_mult {x y : C}
             (mx : monoid x) (my : monoid y) (f : C ⟦x ,y ⟧) : UU
    := (f ⊗⊗ f ) · μ_{my } = μ_{mx } · f.

  Definition is_monoid_mor_unit {x y : C}
             (mx : monoid x) (my : monoid y) (f : C ⟦x ,y ⟧) : UU
    := η_{mx } · f = η_{my }.

  Definition is_monoid_mor {x y : C}
             (mx : monoid x) (my : monoid y) (f : C ⟦x ,y ⟧) : UU
    := is_monoid_mor_mult mx my f × is_monoid_mor_unit mx my f.

  Lemma isaprop_is_monoid_mor {x y : C}
        (mx : monoid x) (my : monoid y) (f : C ⟦x ,y ⟧)
    : isaprop (is_monoid_mor mx my f).
  Show proof.

apply isapropdirprod ; apply homset_property.

Definition monoid_disp_cat_ob_mor : disp_cat_ob_mor C.
Show proof.

exists (λ x , monoid x).
exact (λ x y mx my f , is_monoid_mor mx my f).

  Lemma id_is_monoid_mor {x : C} (xx : monoid x)
    : is_monoid_mor xx xx (identity x).
  Show proof.

    split.
    - refine (_ @ ! id_right _).
      etrans. {
        apply maponpaths_2, bifunctor_distributes_over_id.
        apply (bifunctor_leftid M).
        apply (bifunctor_rightid M).
      }
      apply id_left.
    - apply id_right.

  Lemma comp_is_monoid_mor {x y z : C}
        {f : C ⟦ x , y ⟧} {g : C ⟦ y , z ⟧}
        {xx : monoid x} {yy : monoid y} {zz : monoid z}
        (pf : is_monoid_mor xx yy f) (pg : is_monoid_mor yy zz g)
    : is_monoid_mor xx zz (f · g).
  Show proof.

    split.
    - etrans. {
        apply maponpaths_2.
        apply bifunctor_distributes_over_comp.
        apply (bifunctor_leftcomp M).
        apply (bifunctor_rightcomp M).
        apply (bifunctor_equalwhiskers M).
      }
      etrans.
      1: apply assoc'.
      etrans.
      1: apply maponpaths, (pr1 pg).
      etrans.
      1: apply assoc.
      etrans.
      1: apply maponpaths_2, (pr1 pf).
      apply assoc'.
    - unfold is_monoid_mor_unit.
      etrans.
      1: apply assoc.
      etrans.
      1: apply maponpaths_2, (pr2 pf).
      apply (pr2 pg).

  Definition monoid_disp_cat_id_comp
    : disp_cat_id_comp C monoid_disp_cat_ob_mor.
  Show proof.

    split.
    - intro ; intro ; apply id_is_monoid_mor.
    - intros x y z f g xx yy zz pf pg.
      exact (comp_is_monoid_mor pf pg).

Definition monoid_disp_cat_data : disp_cat_data C.
Show proof.

exists monoid_disp_cat_ob_mor.
exact monoid_disp_cat_id_comp.

  Definition monoid_disp_cat_axioms
    : disp_cat_axioms C monoid_disp_cat_data.
  Show proof.

repeat split ; intro ; intros ; try (apply isaprop_is_monoid_mor).
apply isasetaprop ; apply isaprop_is_monoid_mor.

Definition monoid_disp_cat : disp_cat C.
Show proof.

exists monoid_disp_cat_data.
exact monoid_disp_cat_axioms.

  Definition category_of_monoids_in_monoidal_cat : category
    := total_category monoid_disp_cat.

  Let MON : category := category_of_monoids_in_monoidal_cat.

  Definition monoid_carrier
             (X : MON)
    : ob C := pr1 X.

  Definition monoid_struct (X : MON)
    : monoid (monoid_carrier X)
    := pr2 X.

  Definition monoid_multiplication (X : MON)
    : C ⟦monoid_carrier X ⊗_{ M } monoid_carrier X , monoid_carrier X ⟧
    := monoid_data_multiplication (monoid_struct X).

  Definition monoid_unit (X : MON)
    : C ⟦I , monoid_carrier X ⟧
    := monoid_data_unit (monoid_struct X).

  Definition monoid_left_unit_law (X : MON)
    : monoid_laws_unit_left (monoid_struct X)
    := monoid_to_unit_left_law (monoid_struct X).

  Definition monoid_right_unit_law (X : MON)
    : monoid_laws_unit_right (monoid_struct X)
    := monoid_to_unit_right_law (monoid_struct X).

  Definition monoid_assoc_law (X : MON)
    : monoid_laws_assoc (monoid_struct X)
    := monoid_to_assoc_law (monoid_struct X).
End Category_of_Monoids.

Definition unit_monoid
  (V : monoidal_cat)
  : monoid V (monoidal_unit V).
Show proof.

  use make_monoid.
  - exact (monoidal_leftunitordata V (monoidal_unit V)).
  - exact (identity (monoidal_unit V)).
  - etrans. {
      apply maponpaths_2.
      apply (bifunctor_rightid V).
    }
    apply id_left.
  - etrans. {
      apply maponpaths_2.
      apply (bifunctor_leftid V).
    }
    refine (id_left _ @ _).
    apply unitors_coincide_on_unit.
  - apply maponpaths_2.
    etrans.
    2: { rewrite unitors_coincide_on_unit.
         apply monoidal_triangleidentity. }
    apply idpath.