The precategory of semigroups
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-03-17.
Last modified on 2023-09-26.
module group-theory.precategory-of-semigroups where
Imports
open import category-theory.large-precategories open import foundation.universe-levels open import group-theory.homomorphisms-semigroups open import group-theory.semigroups
Idea
Semigroups and semigroup homomorphisms form a precategory.
Definition
The precategory of semigroups
instance Semigroup-Large-Precategory : Large-Precategory lsuc (_⊔_) obj-Large-Precategory Semigroup-Large-Precategory = Semigroup hom-set-Large-Precategory Semigroup-Large-Precategory = hom-set-Semigroup comp-hom-Large-Precategory Semigroup-Large-Precategory {X = G} {H} {K} = comp-hom-Semigroup G H K id-hom-Large-Precategory Semigroup-Large-Precategory {X = G} = id-hom-Semigroup G associative-comp-hom-Large-Precategory Semigroup-Large-Precategory {X = G} {H} {K} {L} = associative-comp-hom-Semigroup G H K L left-unit-law-comp-hom-Large-Precategory Semigroup-Large-Precategory {X = G} {H} = left-unit-law-comp-hom-Semigroup G H right-unit-law-comp-hom-Large-Precategory Semigroup-Large-Precategory {X = G} {H} = right-unit-law-comp-hom-Semigroup G H
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-05-06. Egbert Rijke. Big cleanup continued (#597).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).