The precategory of concrete groups
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Julian KG, fernabnor and louismntnu.
Created on 2022-09-20.
Last modified on 2023-09-26.
module group-theory.precategory-of-concrete-groups where
Imports
open import category-theory.large-precategories open import foundation.universe-levels open import group-theory.concrete-groups open import group-theory.homomorphisms-concrete-groups
Definitions
The large precategory of concrete groups
Concrete-Group-Large-Precategory : Large-Precategory lsuc (_⊔_) obj-Large-Precategory Concrete-Group-Large-Precategory = Concrete-Group hom-set-Large-Precategory Concrete-Group-Large-Precategory = hom-set-Concrete-Group comp-hom-Large-Precategory Concrete-Group-Large-Precategory {X = G} {Y = H} {Z = K} = comp-hom-Concrete-Group G H K id-hom-Large-Precategory Concrete-Group-Large-Precategory {X = G} = id-hom-Concrete-Group G associative-comp-hom-Large-Precategory Concrete-Group-Large-Precategory {X = G} {Y = H} {Z = K} {W = L} h g f = eq-htpy-hom-Concrete-Group G L _ _ ( associative-comp-hom-Concrete-Group G H K L h g f) left-unit-law-comp-hom-Large-Precategory Concrete-Group-Large-Precategory {X = G} {Y = H} f = eq-htpy-hom-Concrete-Group G H _ _ ( left-unit-law-comp-hom-Concrete-Group G H f) right-unit-law-comp-hom-Large-Precategory Concrete-Group-Large-Precategory {X = G} {Y = H} f = eq-htpy-hom-Concrete-Group G H _ _ ( right-unit-law-comp-hom-Concrete-Group G H f)
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-05-06. Egbert Rijke. Big cleanup continued (#597).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).