QuasigroupLoop.tex

\chapter{Theory Of Quasigroup And Loop In Agda}
Quasigroups and loops find applications in various fields of mathematics,
computer science, and physics. For example, Einstein's formula of addition of
velocities gives a loop structure \cite{ungar2007einstein}. In computer science,
they are used in error-correcting codes and cryptography, where properties like
uniqueness of solution and error detection play a crucial role
\cite{phillips2010automated}. The properties of loops help in the development of
efficient computational algorithms, in the areas of optimization, scheduling,
and permutation-based problems \cite{khan2015mining}. In this chapter, we
formalize two important non-associative algebras - quasigroup, and loop
structure.
 
\section{Definitions}
A quasigroup is a set equipped with binary operations that satisfies the
quasigroup property. Formally, a quasigroup $(Q,∙/\backslash)$ is an algebra
consisting of a set ($Q$) and three binary operations $∙$ (multiplication),
$\backslash$ (left division), and $/$ (right division). These operations satisfy
the following identities $\forall x y \in Q$:

\begin{equation} \label{eq_L-leftdivides}
y\ =\ x\ ∙\ (x\ \backslash\ y)
\end{equation}
\begin{equation} \label{eq_L-rightdivides}
y\ =\ x\ \backslash\ (x\ ∙\ y)
\end{equation}
\begin{equation} \label{eq_R-leftdivides}
y\ =\ (y\ /\ x)\ ∙\ x
\end{equation}
\begin{equation} \label{eq_Rirightdivides}
y\ =\ (y\ ∙\ x)\ /\ x
\end{equation}

In Chapter 3, we may observe that Agda supports many unicode characters (UTF-8)
that can be used in identifiers. However, there are some limitations in the use
of certain characters due to their reserved status that can cause conflict with
Agda's syntax. Backslash ($\backslash$) is used in Agda's syntax for various
purposes, such as defining Unicode characters and escape sequences, which would
result in potential conflicts if it were allowed as an identifier. To overcome
this issue, we use // and \textbackslash\textbackslash instead of / and
\textbackslash \ respectively.

We can write the above predicates in Agda as:

\begin{minted}[samepage,breaklines]{Agda}
LeftDividesˡ : Op₂ A → Op₂ A → Set _
LeftDividesˡ _∙_  _\\_ = ∀ x y → (x ∙ (x \\ y)) ≈ y
\end{minted}
\begin{minted}[samepage,breaklines]{Agda}
LeftDividesʳ : Op₂ A → Op₂ A → Set _
LeftDividesʳ _∙_ _\\_ = ∀ x y → (x \\ (x ∙ y)) ≈ y
\end{minted}
\begin{minted}[samepage,breaklines]{Agda}
RightDividesˡ : Op₂ A → Op₂ A → Set _
RightDividesˡ _∙_ _//_ = ∀ x y → ((y // x) ∙ x) ≈ y
\end{minted}
\begin{minted}[samepage,breaklines]{Agda}
RightDividesʳ : Op₂ A → Op₂ A → Set _
RightDividesʳ _∙_ _//_ = ∀ x y → ((y ∙ x) // x) ≈ y
\end{minted}

We can combine two predicates using the product (\inline{×}) as:

\begin{minted}[samepage,breaklines]{Agda}
LeftDivides : Op₂ A → Op₂ A → Set _
LeftDivides ∙ \\ = (LeftDividesˡ ∙ \\) × (LeftDividesʳ ∙ \\)

RightDivides : Op₂ A → Op₂ A → Set _
RightDivides ∙ // = (RightDividesˡ ∙ //) × (RightDividesʳ ∙ //)
\end{minted} 

A quasigroup in Agda is defined as a record type:

\begin{minted}[samepage,breaklines]{Agda}
record IsQuasigroup (∙ \\ // : Op₂ A) : Set (a ⊔ ℓ) where
field
  isMagma       : IsMagma ∙
  \\-cong       : Congruent₂ \\
  //-cong       : Congruent₂ //
  leftDivides   : LeftDivides ∙ \\
  rightDivides  : RightDivides ∙ //

open IsMagma isMagma public
\end{minted}
In the above definition, \inline{IsQuasigroup} is a record type with three
binary operations $∙,\ \backslash\backslash \ //$ on setoid $A$. The structure
has five fields. We restrict discussing the syntax of the definition as it is
covered in Chapter 3.

A loop is a quasigroup that has an identity element. The identity axiom is given
as:
\begin{equation}\label{eq_lineslope}
x\ ∙\ e\ =\ e\ ∙\ x\ =\ x
\end{equation}

Like left/right division, the identity predicate in Agda is given as:

\begin{minted}[samepage,breaklines]{Agda}
LeftIdentity : A → Op₂ A → Set _
LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x

RightIdentity : A → Op₂ A → Set _
RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x

Identity : A → Op₂ A → Set _
Identity e ∙ = (LeftIdentity e ∙) × (RightIdentity e ∙)
\end{minted}

A loop structure can be characterized in Agda as:

\begin{minted}[samepage,breaklines]{Agda}
record IsLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
field
  isQuasigroup : IsQuasigroup ∙ \\ //
  identity     : Identity ε ∙

open IsQuasigroup isQuasigroup public
\end{minted}

Bol loops are non-associative algebraic systems that satisfy a weakened form of
the associative property. A loop is called a \textit{right bol loop} if it
satisfies the right-bol identity
\[ ((z\ ∙\ x)\ ∙\ y)\ ∙\ x\ =\ z\ ∙\ ((\ x\ ∙\ y)\ ∙\ x)\]
A loop is called a \textit{left bol loop} if it satisfies the left-bol identity
\[ x\ ∙\ (y\ ∙\ (x\ ∙\ z))\ =\ (x\ ∙\ (y\ ∙\ x))\ ∙\ z\]
A loop is called \textit{middle bol loop} if it satisfies the middle-bol identity
\[(z\ ∙\ x)\ ∙\ (y\ ∙\ z)\ =\ z\ ∙\ ((x\ ∙\ y)\ ∙\ z)\] 

A left-right bol loop is called a \textit{moufang loop} if it satisfies the
moufang identity. Moufang loops have applications in the fields of geometry, and
theoretical physics \cite{kunen1996moufang}.
\[(z\ ∙\ x)\ ∙\ (y\ ∙\ z)\ =\ z\ ∙\ ((x\ ∙\ y)\ ∙\ z)\]

The definition of these structures is similar to \inline{IsLoop} and can be
found in the Agda standard library in module \inline{Algebra.Structures}.

\section{Homomorphism}
A structure-preserving map $f$ between two structures of same type is called a
homomorphism. For quasigroups $(Q_1,∙,\backslash \backslash ,//)$ and
$(Q_2,\circ,\backslash ,/)$, homomorphism is defined as a function \(
f:(Q_1,∙,\backslash \backslash,//) \rightarrow (Q_2,\circ,\backslash,/) \) such
that:
\begin{itemize}
  \item $f$ preserves the binary operation: $f(x∙y) = f(x) \circ f(y)$
  \item $f$ preserves the left division operation : $f(x\backslash \backslash y)
  = f(x)\backslash f(y)$
  \item $f$ preserves the right division operation: $f(x//y) = f(x)/f(y)$
\end{itemize}

In Agda, quasigroup homomorphism can be defined as:

\begin{minted}[samepage,breaklines]{Agda}
record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
    ∙-homo            : Homomorphic₂ ⟦_⟧ _∙₁_ _∙₂_
    \\-homo           : Homomorphic₂ ⟦_⟧ _\\₁_ _\\₂_
    //-homo           : Homomorphic₂ ⟦_⟧ _//₁_ _//₂_

  open IsRelHomomorphism isRelHomomorphism public
    renaming (cong to ⟦⟧-cong)
\end{minted}

The loop homomorphism preserves left and right divisions along with the identity
element. The homomorphism $f$ preserves all the binary operations as quasigroup
along with the identity element. For two loop structure $(L_1,∙,\backslash
\backslash,//,e_1) \text{and} (L_2,\circ,\backslash,/,e_2) $, the function \(
f:(L_1,∙,\backslash \backslash,//,e_1) \rightarrow (L_2,\circ,\backslash,/,e_2)
\) is a loop homomorphism if it is a quasigroup homomorphism and: 
\[f(e_1) = e_2\] where $e_1$ is the identity element of loop $L_1$ and $e_2$ is
the identity element of loop $L_2$. In Agda, loop homomorphism can be defined
using quasigroup homomorphism as:

\begin{minted}[breaklines,samepage]{Agda}
record IsLoopHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
    ε-homo                   : Homomorphic₀ ⟦_⟧ ε₁ ε₂

  open IsQuasigroupHomomorphism isQuasigroupHomomorphism public
\end{minted}

The definitions of quasigroup loop monomorphism and isomorphism can be defined
similarly to magma homomorphism as discussed in Chapter 3. These definitions can
be found in the Agda standard library under module
\MYhref{https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Morphism/Structures.agda}{Algebra.Morphism.Structures}.

\section{Composition of Homomrphism}
If $f$ is a homomorphism such that $f\ :\ a \ \rightarrow \ b$ and $g$ is a
homomorphism such that $g\ :\ b\ \rightarrow \ c$, then the composition of
homomorphism can be defined as $g \ ∘\ f\ :\ a \ \rightarrow \ c$. In Agda we
can prove that the composition of quasigroup homomorphism is homomorphic as:

\begin{minted}[breaklines,samepage]{Agda}
isQuasigroupHomomorphism
  : IsQuasigroupHomomorphism Q₁ Q₂ f
  → IsQuasigroupHomomorphism Q₂ Q₃ g
  → IsQuasigroupHomomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupHomomorphism f-homo g-homo = record
  { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
  ; ∙-homo              = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.∙-homo x y )) ( G.∙-homo (f x) (f y) )
  ; \\-homo              = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.\\-homo x y )) ( G.\\-homo (f x) (f y) )
  ; //-homo              = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.//-homo x y )) ( G.//-homo (f x) (f y) )
  } where module F = IsQuasigroupHomomorphism f-homo; 
          module G = IsQuasigroupHomomorphism g-homo
\end{minted}

In the above quasigroup homomorphism composition, \inline{f} is a homomorphism
from quasigroup $Q₁$ to $Q₂$, \inline{g} is a homomorphism from quasigroup $Q₂$ to $Q₃$.
\inline{isRelHomomorphism} field gives the composition of homomorphism for a
homogeneous binary relation (≈). We can prove that the composition of binary
operations homomorphism (∙) for quasigroup is homomorphic using transitive
relation \inline{≈₃-trans} such that \[g (f ((Q₁ ∙ x) y)) ≈ (g ((Q₂ ∙ f x) (f
y)) \text{ and } g ((Q₂ ∙ f x) (f y))) ≈ ((Q₃ ∙ g (f x)) (g (f y)))\]
\[\Rightarrow g (f ((Q₁ ∙ x) y)) ≈ ((Q₃ ∙ g (f x)) (g (f y)))\]

Monomorphism and isomorphism composition constructs for quasigroup and loop are
defined similar to homomorphism and can be found in the Agda standard library.

\section{Product Algebra}
The product algebra $M \ \times \ N$ of two quasigroups $M$ and $N$ is defined
in Agda as:

\begin{minted}[breaklines,samepage]{Agda}
quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
quasigroup M N = record
  { _\\_    = zip M._\\_ N._\\_
  ; _//_    = zip M._//_ N._//_
  ; isQuasigroup = record
    { isMagma = Magma.isMagma (magma M.magma N.magma)
    ; \\-cong = zip M.\\-cong N.\\-cong
    ; //-cong = zip M.//-cong N.//-cong
    ; leftDivides = (λ x y → M.leftDividesˡ , N.leftDividesˡ <*> x <*> y) , (λ x y → M.leftDividesʳ , N.leftDividesʳ <*> x <*> y)
    ; rightDivides = (λ x y → M.rightDividesˡ , N.rightDividesˡ <*> x <*> y) , (λ x y → M.rightDividesʳ , N.rightDividesʳ <*> x <*> y)
    }
  } where module M = Quasigroup M; module N = Quasigroup N
\end{minted}

In the above code, \inline{zip} gives a $\Sigma$-type of dependent pairs.
\inline{<*>} is used to convert the curried functions to a function on a pair.
Currying a function is to break down a function that takes multiple arguments
into a series of functions that take exactly one argument. The product of loop
structure can be defined similarly to quasigroup. 

\section{Properties}
In this section, we prove some properties of quasigroup, loop, middle bol loop,
and moufang loop using Agda. The proofs for quasigroup and loop are adapted from
\cite{Stener2016MoufangL} and \cite{bruck1944some}.
\subsection{Properties Of Quasigroup}
Cancellative quasigroups are used in cryptographic protocols. Properties such as
left and right cancellation can be used to ensure the confidentiality of data
during encryption and decryption processes \cite{shcherbacov2003elements}. Let
$(Q, ∙, /, \backslash)$ be a quasigroup then:
\begin{enumerate}
\item $Q$ is cancellative. A quasigroup is left cancellative if $x\ ∙\ y\ =\ x\ ∙\ z$ then
$y\ =\ z$ and a quasigroup is right cancellative if $y\ ∙\ x\ =\ z\ ∙\ x$ then $y\ =\ z$. A
quasigroup is cancellative if it is both left and right cancellative.
\item \(\text{If} \ x\ ∙\ y\ =\ z\ \text{then}\ y\ =\ x\ \backslash \ z\)
\item \(\text{If} \ x\ ∙\ y\ =\ z\ \text{then}\ x\ = z\ /\ y\)
\end{enumerate}
Proof:
\begin{enumerate}
\item 
\begin{minted}[breaklines,samepage]{Agda}
cancelˡ : LeftCancellative _∙_
cancelˡ x y z eq = begin
  y             ≈⟨ sym( leftDividesʳ x y) ⟩
  x \\ (x ∙ y)  ≈⟨ \\-congˡ eq ⟩
  x \\ (x ∙ z)  ≈⟨ leftDividesʳ x z ⟩
  z             ∎

cancelʳ : RightCancellative _∙_
cancelʳ x y z eq = begin
  y             ≈⟨ sym( rightDividesʳ x y) ⟩
  (y ∙ x) // x  ≈⟨ //-congʳ eq ⟩
  (z ∙ x) // x  ≈⟨ rightDividesʳ x z ⟩
  z             ∎

cancel : Cancellative _∙_
cancel = cancelˡ , cancelʳ
\end{minted}

\item 
\begin{minted}[breaklines,samepage]{Agda}
y≈x\\z : ∀ x y z → x ∙ y ≈ z → y ≈ x \\ z
y≈x\\z x y z eq = begin
  y            ≈⟨ sym (leftDividesʳ x y) ⟩
  x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩
  x \\ z       ∎
\end{minted}

\item 
\begin{minted}[breaklines,samepage]{Agda}
x≈z//y : ∀ x y z → x ∙ y ≈ z → x ≈ z // y
x≈z//y x y z eq = begin
  x            ≈⟨ sym (rightDividesʳ y x) ⟩
  (x ∙ y) // y ≈⟨ //-congʳ eq ⟩
  z // y       ∎
\end{minted}
\end{enumerate}

\subsection{Properties Of Loop}
Properties of division operation hold for a loop.\\
Let $(L, ∙, /, \backslash, e)$ be a Loop with identity $x\ ∙\ e\ =\ x\ =\ e\ ∙\ x$
then the following properties holds 
\begin{enumerate}
\item \(x \ /\  x\ =\ e\) 
\item \( x\ \backslash \ x\ =\ e\)
\item \(e\ \backslash \ x\ =\ x\) 
\item \(x\ /\ e\ =\ x\) 
\end{enumerate}
Proof:
\begin{enumerate}
\item 
\begin{minted}[breaklines,samepage]{Agda}
x//x≈ε : ∀ x → x // x ≈ ε
x//x≈ε x = begin
  x // x       ≈⟨ //-congʳ (sym (identityˡ x)) ⟩
  (ε ∙ x) // x ≈⟨ rightDividesʳ x ε ⟩
  ε            ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x\\x≈ε : ∀ x → x \\ x ≈ ε
x\\x≈ε x = begin
  x \\ x       ≈⟨ \\-congˡ (sym (identityʳ x )) ⟩
  x \\ (x ∙ ε) ≈⟨ leftDividesʳ x ε ⟩
  ε            ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
ε\\x≈x : ∀ x → ε \\ x ≈ x
ε\\x≈x x = begin
  ε \\ x       ≈⟨ sym (identityˡ (ε \\ x)) ⟩
  ε ∙ (ε \\ x) ≈⟨ leftDividesˡ ε x ⟩
  x            ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x//ε≈x : ∀ x → x // ε ≈ x
x//ε≈x x = begin
  x // ε       ≈⟨ sym (identityʳ (x // ε)) ⟩
  (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩
  x            ∎
\end{minted}
\end{enumerate}
\subsection{Properties Of Middle Bol Loop}
Middle Bol loops are used in combinatorial design theory to construct specific
types of combinatorial designs. The proofs for properties of the middle bol loop are
adapted from \cite{jaiyeola2021new}. Let $(M, ∙, /, \backslash, e)$ be a middle bol loop then the
following identities hold.
\begin{enumerate}
\item \(x\ ∙\ ((y\ ∙\ x)\ \backslash \ x)\ =\ y\ \backslash\ x\) 
\item \(x\ ∙\ ((x\ ∙\ z)\ \backslash \ x)\ =\ x\ /\ z\)
\item \(x\ ∙ (z\ \backslash\ x)\ =\ (x\ /\ z)\ ∙\ x\)
\item \((x\ /\ (y\ ∙\ z))\ ∙\ x\ =\ (x\ /\ z)\ ∙\ (y\ \backslash\ x)\)
\item \((x\ /\ (y\ ∙\ x))\ ∙\ x\ =\ y\ \backslash \ x\)
\item \((x\ /\ (x\ ∙\ z))\ ∙\ x\ = \ x\ /\  z\)
\end{enumerate}
Proof:
\begin{enumerate}
\item
\begin{minted}[breaklines,samepage]{Agda}
xyx\\x≈y\\x : ∀ x y → x ∙ ((y ∙ x) \\ x) ≈ y \\ x
xyx\\x≈y\\x x y = begin
  x ∙ ((y ∙ x) \\ x)  ≈⟨ middleBol x y x ⟩
  (x // x) ∙ (y \\ x) ≈⟨ ∙-congʳ (x//x≈ε x) ⟩
  ε ∙ (y \\ x)        ≈⟨ identityˡ ((y \\ x)) ⟩
  y \\ x              ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
xxz\\x≈x//z : ∀ x z → x ∙ ((x ∙ z) \\ x) ≈ x // z
xxz\\x≈x//z x z = begin
  x ∙ ((x ∙ z) \\ x)  ≈⟨ middleBol x x z ⟩
  (x // z) ∙ (x \\ x) ≈⟨ ∙-congˡ (x\\x≈ε x) ⟩
  (x // z) ∙ ε        ≈⟨ identityʳ ((x // z)) ⟩
  x // z              ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
xz\\x≈x//zx : ∀ x z → x ∙ (z \\ x) ≈ (x // z) ∙ x
xz\\x≈x//zx x z = begin
  x ∙ (z \\ x)       ≈⟨ ∙-congˡ (\\-congʳ( sym (identityˡ z))) ⟩
  x ∙ ((ε ∙ z) \\ x) ≈⟨ middleBol x ε z ⟩
  x // z ∙ (ε \\ x)  ≈⟨ ∙-congˡ (ε\\x≈x x) ⟩
  x // z ∙ x         ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x//yzx≈x//zy\\x : ∀ x y z → (x // (y ∙ z)) ∙ x ≈ (x // z) ∙ (y \\ x)
x//yzx≈x//zy\\x x y z = begin
  (x // (y ∙ z)) ∙ x  ≈⟨ sym (xz\\x≈x//zx x ((y ∙ z))) ⟩
  x ∙ ((y ∙ z) \\ x)  ≈⟨ middleBol x y z ⟩
  (x // z) ∙ (y \\ x) ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x//yxx≈y\\x : ∀ x y → (x // (y ∙ x)) ∙ x ≈ y \\ x
x//yxx≈y\\x x y = begin
  (x // (y ∙ x)) ∙ x  ≈⟨ x//yzx≈x//zy\\x  x y x ⟩
  (x // x) ∙ (y \\ x) ≈⟨ ∙-congʳ (x//x≈ε x) ⟩
  ε ∙ (y \\ x)        ≈⟨ identityˡ ((y \\ x)) ⟩
  y \\ x              ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x//xzx≈x//z : ∀ x z → (x // (x ∙ z)) ∙ x ≈ x // z
x//xzx≈x//z x z = begin
  (x // (x ∙ z)) ∙ x  ≈⟨ x//yzx≈x//zy\\x x x z ⟩
  (x // z) ∙ (x \\ x) ≈⟨ ∙-congˡ (x\\x≈ε x) ⟩
  (x // z) ∙ ε        ≈⟨ identityʳ (x // z) ⟩
  x // z              ∎    
\end{minted}
\end{enumerate}
\subsection{Properties Of Moufang Loop}
The properties of Moufang loops have applications in computational mathematics
and algorithm design. They provide insights into the efficient implementation of
mathematical algorithms and data structures \cite{kunen1996moufang}. The proofs
in this sub-section are adapted from \cite{Stener2016MoufangL}. Let $(M, ∙, /,
\backslash, e)$ be a moufang loop then the following identities hold.
\begin{enumerate}
\item Moufang loop is alternative. A moufang loop is left alternative if it
satisfies \((x\ ∙\ x)\ ∙\ y\ =\ x\ ∙\ (x\ ∙\ y)\), a moufang loop is right
alternative if it satisfies \(x\ ∙\ (y\ ∙\ y)\ =\ (x\ ∙ y)\ ∙\ y\) and if a
moufang loop alternative if it is both left and right alternative. 
\item Moufang loop is flexible. A Moufang loop is flexible if it satisfies
flexible identity $(x\ ∙\ y)\ ∙\ x\ =\ x\ ∙\ (y\ ∙\ x)$
\item $z\ ∙\ (x\ ∙\ (z\ ∙\ y))\ =\ ((z\ ∙\ x)\ ∙\ z)\ ∙\ y$
\item $x\ ∙\ (z\ ∙\ (y\ ∙\ z))\ =\ ((x\ ∙\ z)\ ∙\ y)\ ∙\ z$ 
\item $z\ ∙\ ((x\ ∙\ y)\ ∙\ z)\ =\ (z\ ∙ \ (x\ ∙\ y))\ ∙\ z$ 
\end{enumerate}
Proof:
\begin{enumerate}
\item
\begin{minted}[breaklines,samepage]{Agda}
alternativeˡ : LeftAlternative _∙_
alternativeˡ x y = begin
  (x ∙ x) ∙ y       ≈⟨ ∙-congʳ (∙-congˡ (sym (identityˡ x))) ⟩
  (x ∙ (ε ∙ x)) ∙ y ≈⟨ sym (leftBol x ε y) ⟩
  x ∙ (ε ∙ (x ∙ y)) ≈⟨ ∙-congˡ (identityˡ ((x ∙ y))) ⟩
  x ∙ (x ∙ y)       ∎

alternativeʳ : RightAlternative _∙_
alternativeʳ x y = begin
  x ∙ (y ∙ y)         ≈⟨ ∙-congˡ(∙-congʳ(sym (identityʳ y))) ⟩
  x ∙ ((y ∙ ε) ∙ y)   ≈⟨ sym (rightBol y ε x) ⟩
  ((x ∙ y) ∙ ε ) ∙ y  ≈⟨ ∙-congʳ (identityʳ ((x ∙ y))) ⟩
  (x ∙ y) ∙ y         ∎

alternative : Alternative _∙_
alternative = alternativeˡ , alternativeʳ
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
flex : Flexible _∙_
flex x y = begin
  (x ∙ y) ∙ x       ≈⟨ ∙-congˡ (sym (identityˡ x)) ⟩
  (x ∙ y) ∙ (ε ∙ x) ≈⟨ identical y ε x ⟩
  x ∙ ((y ∙ ε) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (identityʳ y)) ⟩
  x ∙ (y ∙ x)       ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
z∙xzy≈zxz∙y : ∀ x y z → (z ∙ (x ∙ (z ∙ y))) ≈ (((z ∙ x) ∙ z) ∙ y)
z∙xzy≈zxz∙y x y z = sym (begin
  ((z ∙ x) ∙ z) ∙ y ≈⟨ (∙-congʳ (flex z x )) ⟩
  (z ∙ (x ∙ z)) ∙ y ≈⟨ sym (leftBol z x y) ⟩
  z ∙ (x ∙ (z ∙ y)) ∎)
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x∙zyz≈xzy∙z : ∀ x y z → (x ∙ (z ∙ (y ∙ z))) ≈ (((x ∙ z) ∙ y) ∙ z)
x∙zyz≈xzy∙z x y z = begin
  x ∙ (z ∙ (y ∙ z))  ≈⟨ (∙-congˡ (sym (flex z y ))) ⟩
  x ∙ ((z ∙ y) ∙  z) ≈⟨ sym (rightBol z y x) ⟩
  ((x ∙ z) ∙ y) ∙ z  ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
z∙xyz≈zxy∙z : ∀ x y z → (z ∙ ((x ∙ y) ∙ z)) ≈ ((z ∙ (x ∙ y)) ∙ z)
z∙xyz≈zxy∙z x y z = sym (flex z (x ∙ y))
\end{minted}
\end{enumerate}