Large function semigroups

Content created by Louis Wasserman.

Created on 2025-11-16.
Last modified on 2026-03-06.

module group-theory.large-function-semigroups where
Imports 
open import foundation.function-extensionality
open import foundation.sets
open import foundation.universe-levels

open import group-theory.dependent-products-large-semigroups
open import group-theory.large-semigroups

Idea

Given a large semigroup G and an arbitrary type A, A → G forms a large semigroup.

Definition

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  {l0 : Level}
  (A : UU l0)
  (G : Large-Semigroup α β)
  where

  function-Large-Semigroup :
    Large-Semigroup (λ l → l0 ⊔ α l) (λ l1 l2 → l0 ⊔ β l1 l2)
  function-Large-Semigroup = Π-Large-Semigroup A (λ _ → G)

Recent changes