The category of concrete groups
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Julian KG, fernabnor and louismntnu.
Created on 2022-09-19.
Last modified on 2023-06-25.
module group-theory.category-of-concrete-groups where
Imports
Definitions
The category of concrete groups
-- is-category-Concrete-Group-Large-Precategory : -- is-large-category-Large-Precategory Concrete-Group-Large-Precategory -- is-category-Concrete-Group-Large-Precategory = {!!}
Recent changes
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import(#497).