The precategory of monoids

Content created by Egbert Rijke.

Created on 2023-05-06.
Last modified on 2023-09-21.

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

open import foundation.universe-levels

open import group-theory.homomorphisms-monoids
open import group-theory.monoids

Idea

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

Definitions

The large precategory of monoids

Monoid-Large-Precategory : Large-Precategory lsuc _⊔_
obj-Large-Precategory
  Monoid-Large-Precategory =
  Monoid
hom-Large-Precategory
  Monoid-Large-Precategory =
  hom-Monoid
comp-hom-Large-Precategory
  Monoid-Large-Precategory {X = K} {L} {M} =
  comp-hom-Monoid K L M
id-hom-Large-Precategory
  Monoid-Large-Precategory {X = M} =
  id-hom-Monoid M
associative-comp-hom-Large-Precategory
  Monoid-Large-Precategory {X = K} {L} {M} {N} =
  associative-comp-hom-Monoid K L M N
left-unit-law-comp-hom-Large-Precategory
  Monoid-Large-Precategory {X = M} {N} =
  left-unit-law-comp-hom-Monoid M N
right-unit-law-comp-hom-Large-Precategory
  Monoid-Large-Precategory {X = M} {N} =
  right-unit-law-comp-hom-Monoid M N

The precategory of small monoids

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

Recent changes