This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The precategory of monoids

module group-theory.precategory-of-monoids where
Imports 
open import category-theory.large-precategories
open import category-theory.large-subprecategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import group-theory.homomorphisms-monoids
open import group-theory.monoids
open import group-theory.precategory-of-semigroups

Idea

The precategory of monoids consists of monoids and homomorphisms of monoids.

Definitions

The precategory of monoids as a subprecategory of the precategory of semigroups

Monoid-Large-Subprecategory :
  Large-Subprecategory (λ l → l) (λ l1 l2 → l2) Semigroup-Large-Precategory
Monoid-Large-Subprecategory =
  λ where
    .subtype-obj-Large-Subprecategory l →
      is-unital-prop-Semigroup {l}
    .subtype-hom-Large-Subprecategory G H is-unital-G is-unital-H →
      preserves-unit-hom-prop-Semigroup (G , is-unital-G) (H , is-unital-H)
    .contains-id-Large-Subprecategory G is-unital-G →
      preserves-unit-id-hom-Monoid (G , is-unital-G)
    .is-closed-under-composition-Large-Subprecategory
      G H K g f is-unital-G is-unital-H is-unital-K unit-g unit-f →
      preserves-unit-comp-hom-Monoid
        ( G , is-unital-G)
        ( H , is-unital-H)
        ( K , is-unital-K)
        ( g , unit-g)
        ( f , unit-f)

The large precategory of monoids

Monoid-Large-Precategory : Large-Precategory lsuc (_⊔_)
Monoid-Large-Precategory =
  large-precategory-Large-Subprecategory Monoid-Large-Subprecategory

The precategory of small monoids

Monoid-Precategory : (l : Level) → Precategory (lsuc l) l
Monoid-Precategory = precategory-Large-Precategory Monoid-Large-Precategory