# Function semigroups

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-13.

module group-theory.function-semigroups where

Imports
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

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


## Idea

Given a semigroup G and a type X, the function semigroup G^X consists of functions from X to the underlying type of G. The semigroup operation is given pointwise.

## Definition

module _
{l1 l2 : Level} (G : Semigroup l1) (X : UU l2)
where

function-Semigroup : Semigroup (l1 ⊔ l2)
function-Semigroup = Π-Semigroup X (λ _ → G)

set-function-Semigroup : Set (l1 ⊔ l2)
set-function-Semigroup = set-Π-Semigroup X (λ _ → G)

type-function-Semigroup : UU (l1 ⊔ l2)
type-function-Semigroup = type-Π-Semigroup X (λ _ → G)

mul-function-Semigroup :
(f g : type-function-Semigroup) → type-function-Semigroup
mul-function-Semigroup = mul-Π-Semigroup X (λ _ → G)

associative-mul-function-Semigroup :
(f g h : type-function-Semigroup) →
mul-function-Semigroup (mul-function-Semigroup f g) h ＝
mul-function-Semigroup f (mul-function-Semigroup g h)
associative-mul-function-Semigroup =
associative-mul-Π-Semigroup X (λ _ → G)

has-associative-mul-function-Semigroup :
has-associative-mul-Set set-function-Semigroup
has-associative-mul-function-Semigroup =
has-associative-mul-Π-Semigroup X (λ _ → G)