This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The category of concrete groups

module group-theory.category-of-concrete-groups where

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 = {!!}