# The opposite of a semigroup

Content created by Fredrik Bakke.

Created on 2023-11-04.

module group-theory.opposite-semigroups where

Imports
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


## Idea

The opposite of a semigroup G with multiplication μ is a semigroup with the same underlying set as G and multiplication given by x y ↦ μ y x.

## Definition

module _
{l : Level} (G : Semigroup l)
where

set-op-Semigroup : Set l
set-op-Semigroup = set-Semigroup G

type-op-Semigroup : UU l
type-op-Semigroup = type-Set set-op-Semigroup

mul-op-Semigroup : type-op-Semigroup → type-op-Semigroup → type-op-Semigroup
mul-op-Semigroup x y = mul-Semigroup G y x

associative-mul-op-Semigroup :
(x y z : type-op-Semigroup) →
mul-Semigroup G z (mul-Semigroup G y x) ＝
mul-Semigroup G (mul-Semigroup G z y) x
associative-mul-op-Semigroup x y z = inv (associative-mul-Semigroup G z y x)

op-Semigroup : Semigroup l
pr1 op-Semigroup = set-op-Semigroup
pr1 (pr2 op-Semigroup) = mul-op-Semigroup
pr2 (pr2 op-Semigroup) = associative-mul-op-Semigroup