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 precategory of semigroups

module group-theory.precategory-of-semigroups where
Imports 
open import category-theory.large-precategories

open import foundation.universe-levels

open import group-theory.homomorphisms-semigroups
open import group-theory.semigroups

Idea

Semigroups and semigroup homomorphisms form a precategory.

Definition

The large precategory of semigroups

Semigroup-Large-Precategory : Large-Precategory lsuc (_⊔_)
Semigroup-Large-Precategory =
  make-Large-Precategory
    ( Semigroup)
    ( hom-set-Semigroup)
    ( λ {l1} {l2} {l3} {G} {H} {K} → comp-hom-Semigroup G H K)
    ( λ {l} {G} → id-hom-Semigroup G)
    ( λ {l1} {l2} {l3} {l4} {G} {H} {K} {L} →
      associative-comp-hom-Semigroup G H K L)
    ( λ {l1} {l2} {G} {H} → left-unit-law-comp-hom-Semigroup G H)
    ( λ {l1} {l2} {G} {H} → right-unit-law-comp-hom-Semigroup G H)