Large semigroups

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-07.
Last modified on 2023-08-01.

module group-theory.large-semigroups where
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import group-theory.semigroups


A large semigroup with universe indexing function α : Level → Level consists of:

  • For each universe level l a set X l : UU (α l)
  • For any two universe levels l1 and l2 a binary operation μ l1 l2 : X l1 → X l2 → X (l1 ⊔ l2) satisfying the following associativity law:
  μ (l1 ⊔ l2) l3 (μ l1 l2 x y) z = μ l1 (l2 ⊔ l3) x (μ l2 l3 y z).


record Large-Semigroup (α : Level  Level) : UUω where
    set-Large-Semigroup :
      (l : Level)  Set (α l)
    mul-Large-Semigroup :
      {l1 l2 : Level} 
      type-Set (set-Large-Semigroup l1) 
      type-Set (set-Large-Semigroup l2) 
      type-Set (set-Large-Semigroup (l1  l2))
    associative-mul-Large-Semigroup :
      {l1 l2 l3 : Level}
      (x : type-Set (set-Large-Semigroup l1))
      (y : type-Set (set-Large-Semigroup l2))
      (z : type-Set (set-Large-Semigroup l3)) 
      mul-Large-Semigroup (mul-Large-Semigroup x y) z 
      mul-Large-Semigroup x (mul-Large-Semigroup y z)

open Large-Semigroup public

module _
  {α : Level  Level} (G : Large-Semigroup α)

  type-Large-Semigroup : (l : Level)  UU (α l)
  type-Large-Semigroup l = type-Set (set-Large-Semigroup G l)

  is-set-type-Large-Semigroup :
    {l : Level}  is-set (type-Large-Semigroup l)
  is-set-type-Large-Semigroup = is-set-type-Set (set-Large-Semigroup G _)

Small semigroups from large semigroups

module _
  {α : Level  Level} (G : Large-Semigroup α)

  semigroup-Large-Semigroup : (l : Level)  Semigroup (α l)
  pr1 (semigroup-Large-Semigroup l) = set-Large-Semigroup G l
  pr1 (pr2 (semigroup-Large-Semigroup l)) = mul-Large-Semigroup G
  pr2 (pr2 (semigroup-Large-Semigroup l)) = associative-mul-Large-Semigroup G

Recent changes