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
- 2023-09-21. Egbert Rijke. The classification of cyclic rings (#757).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).