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 2024-03-11.

module group-theory.precategory-of-groups where

open import category-theory.full-large-subprecategories
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

open import group-theory.groups
open import group-theory.precategory-of-semigroups

Definition

The precategory of groups as a full subprecategory of the precategory of semigroups

Group-Full-Large-Subprecategory :
  Full-Large-Subprecategory (λ l → l) Semigroup-Large-Precategory
Group-Full-Large-Subprecategory = is-group-prop-Semigroup

The large precategory of groups

Group-Large-Precategory : Large-Precategory lsuc (_⊔_)
Group-Large-Precategory =
  large-precategory-Full-Large-Subprecategory
    ( Semigroup-Large-Precategory)
    ( Group-Full-Large-Subprecategory)

The small precategories of groups

Group-Precategory : (l : Level) → Precategory (lsuc l) l
Group-Precategory = precategory-Large-Precategory Group-Large-Precategory

Recent changes

• 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
• 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
• 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).