# Wild quasigroups

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-05-07.

module structured-types.wild-quasigroups where

Imports
open import foundation.automorphisms
open import foundation.binary-equivalences
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.universe-levels

open import structured-types.magmas


## Idea

A wild quasigroup is a type A equipped with a binary equivalence μ : A → A → A.

## Definition

Wild-Quasigroup : (l : Level) → UU (lsuc l)
Wild-Quasigroup l = Σ (Magma l) (λ M → is-binary-equiv (mul-Magma M))

module _
{l : Level} (A : Wild-Quasigroup l)
where

magma-Wild-Quasigroup : Magma l
magma-Wild-Quasigroup = pr1 A

type-Wild-Quasigroup : UU l
type-Wild-Quasigroup = type-Magma magma-Wild-Quasigroup

mul-Wild-Quasigroup : (x y : type-Wild-Quasigroup) → type-Wild-Quasigroup
mul-Wild-Quasigroup = mul-Magma magma-Wild-Quasigroup

mul-Wild-Quasigroup' : (x y : type-Wild-Quasigroup) → type-Wild-Quasigroup
mul-Wild-Quasigroup' x y = mul-Wild-Quasigroup y x

is-binary-equiv-mul-Wild-Quasigroup :
is-binary-equiv mul-Wild-Quasigroup
is-binary-equiv-mul-Wild-Quasigroup = pr2 A

is-equiv-mul-Wild-Quasigroup :
(x : type-Wild-Quasigroup) → is-equiv (mul-Wild-Quasigroup x)
is-equiv-mul-Wild-Quasigroup = pr2 is-binary-equiv-mul-Wild-Quasigroup

equiv-mul-Wild-Quasigroup : type-Wild-Quasigroup → Aut type-Wild-Quasigroup
pr1 (equiv-mul-Wild-Quasigroup x) = mul-Wild-Quasigroup x
pr2 (equiv-mul-Wild-Quasigroup x) = is-equiv-mul-Wild-Quasigroup x

is-equiv-mul-Wild-Quasigroup' :
(x : type-Wild-Quasigroup) → is-equiv (mul-Wild-Quasigroup' x)
is-equiv-mul-Wild-Quasigroup' = pr1 is-binary-equiv-mul-Wild-Quasigroup

equiv-mul-Wild-Quasigroup' : type-Wild-Quasigroup → Aut type-Wild-Quasigroup
pr1 (equiv-mul-Wild-Quasigroup' x) = mul-Wild-Quasigroup' x
pr2 (equiv-mul-Wild-Quasigroup' x) = is-equiv-mul-Wild-Quasigroup' x