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 2024-01-17.

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

2024-01-17. Egbert Rijke. Reformatting commented blocks of code (#1004).
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).