The precategory of groups
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.
Created on 2022-03-17.
Last modified on 2023-06-25.
module group-theory.precategory-of-groups where
Imports
open import category-theory.large-precategories open import foundation.universe-levels open import group-theory.groups open import group-theory.homomorphisms-groups
Definition
instance Group-Large-Precategory : Large-Precategory lsuc (_⊔_) obj-Large-Precategory Group-Large-Precategory = Group hom-Large-Precategory Group-Large-Precategory = hom-Group comp-hom-Large-Precategory Group-Large-Precategory {X = G} {H} {K} = comp-hom-Group G H K id-hom-Large-Precategory Group-Large-Precategory {X = G} = id-hom-Group G associative-comp-hom-Large-Precategory Group-Large-Precategory {X = G} {H} {K} {L} = associative-comp-hom-Group G H K L left-unit-law-comp-hom-Large-Precategory Group-Large-Precategory {X = G} {H} = left-unit-law-comp-hom-Group G H right-unit-law-comp-hom-Large-Precategory Group-Large-Precategory {X = G} {H} = right-unit-law-comp-hom-Group G H
Recent changes
- 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-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).