Agda.tex

\chapter{Agda}
Agda is a dependently typed programming language based on Martin-Löf type theory
\cite{AgdaDoc}. Agda allows programmers to define types that depend on values,
to write functions that utilize these types, and to prove the correctness of the
program in the same language \cite{AgdaTB}. Agda is also a proof assistant
system. Agda is designed to help programmers write and verify correct
programs by allowing them to express their intentions in a precise and formal
way. Agda has been used in various applications such as formal verification,
program synthesis, theorem proving, and automated reasoning
\cite{2019arXiv191203028S}. It is also used by researchers and academicians to
teach and explore the concepts of functional programming, type theory, and
formal methods. 

In this chapter, we'll discuss several concepts in Agda. Section \ref{types},
explores types and functions, understanding how they work in Agda. Section
\ref{level} and \ref{equality} discuss the type levels and equality in Agda
respectively. Characterization of algebraic structures with respect to the Agda
standard library is discussed in section \ref{structure}. The chapter also
covers essential constructs such as homomorphism, isomorphism, and direct
product in Agda in section \ref{morphism} and section \ref{directproduct}. We do
not discuss other constructs like quotient algebra \cite{wechler2012universal}
to keep uniformity with what is in the Agda standard library. Finally, section
\ref{proof} discusses equational proofs in Agda.

\section{Types And Functions In Agda}
\label{types}
\subsection{Types In Agda}
Agda is based on a core language that provides a minimal set of primitives and
types and is extended with libraries and modules that define more complex data
structures, algorithms, and abstractions. Agda's type system allows for the
definition of new types and operations that are tailored to the specific needs
of a particular application or domain. Agda supports inductive types, simple
types, and parameterized types \cite{10.1007/978-3-642-03359-9_6}. A data type
in Agda can be declared using the keyword \inline{data} or \inline{record}. 

\begin{minted}[breaklines,samepage]{Agda}
data Bool : Set where
  false : Bool 
  true : Bool
\end{minted}

In the above example code, there are four things to notice.
\begin{enumerate}
  \item \inline{data} is the keyword used to define a new data type. 
  \item \inline{Bool} is the name of the data type.
  \item \inline{Bool} is a type of kind \inline{Set}. (More about \inline{Set} is explained later in the chapter)
  \item There are two constructor values of type \inline{Bool}. They are
  \inline{false} and \inline{true}.
\end{enumerate} 

Let us consider another example of inductive datatype\footnote{An inductive
datatype is a datatype that is defined in terms of itself.} to define natural
numbers \inline{Nat}. 

\begin{minted}[breaklines,samepage]{Agda}
data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat
\end{minted}
\label{code:Nat}

We can see that for defining natural numbers, it is impractical to list all the
constructors like how we did for \inline{Bool}. Instead, we give two ways to
construct a natural number: \inline{zero} is a natural number and \inline{suc}
is the successor of a natural number. In the above definition, \inline{Nat} is
an inductive type defined with base constant \inline{zero} and an inductive data
constructor \inline{suc}. \inline{zero} and \inline{suc} are constructors, where
\inline{suc} has a parameter of type \inline{Nat} and \inline{zero} has no
parameters. 

A record type in Agda is defined by using the keyword \inline{record}. For
example:

\begin{minted}[breaklines,samepage]{Agda}
record Person : Set where
  field
    name : String
    age : Nat
\end{minted}

In the example code, there are four things to notice.
\begin{itemize}
  \item \inline{Person} is the name of the data type.
  \item In record type, parameters may be defined after the record's name
  declaration or may be declared with \inline{field} keyword.
  \item \inline{field} keyword indicates the start of field declaration.
  \item \inline{name : String} and \inline{age : Nat} denotes that \inline{name}
  and \inline{age} are fields of type \inline{String} and \inline{Nat}
  respectively.
\end{itemize}

You can then create instances of this record type by providing values for the
fields:

\begin{minted}{Agda}
alice : Person
alice = record { name = "Alice" ; age = 25 }
\end{minted}

We can access the fields of a record using dot notation:
\begin{minted}{Agda}
nameOfAlice : String
nameOfAlice = alice.name

ageOfAlice : Nat
ageOfAlice = alice.age
\end{minted}

We can use \inline{constructor} keyword in \inline{record} type declaration to
define a constructor function for creating instances of the record type. For
example:

\begin{minted}[breaklines,samepage]{Agda}
record Person₁ : Set where
  constructor makePerson
  field
    name : String
    age : Nat
\end{minted}

We can use the constructor \inline{makePerson} to create instances of the \inline{Person₁}
record:

\begin{minted}[breaklines,samepage]{Agda}
alice : Person₁
alice = makePerson "Alice" 25
\end{minted}

In Agda, the types of fields within a \inline{record} can depend on the values
of other fields within the same record. This way we can express the relationship
or constraints between the components of a record. An example of this is the
Agda's built-in $\Sigma$-type of dependent pairs.

\begin{minted}[samepage,breaklines]{Agda}
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst
\end{minted}

The $\Sigma$ type represents a pair of values where the type of the second value
depends on the value of the first. The underscore in the constructor denotes
where the argument goes. We see more examples of this kind when we talk about
functions later in the chapter. To instantiate this Σ record type, we need to
provide an element of type \inline{A} and a value of type \inline{B fst}:

\begin{minted}[samepage,breaklines]{Agda}
alice : Σ String (λ _ → Nat)
alice = "Alice" , 25
\end{minted}

\inline{Σ} is a dependent pair type constructor that takes two arguments of type
\inline{String} and \inline{(λ _ → Nat)}. The underscore in \inline{λ _ → Nat}
serves as a placeholder indicating that the type of the second component depends
on the value of the first component. The underscore \inline{(_)} placeholder is
often used in Agda to indicate that you don't need to provide a name for a
variable when its value isn't explicitly used in the expression. We see more
examples of record type when we define algebraic structure later in the chapter. 

\subsection{Functions In Agda}
Those familiar with Haskell will find Agda to be somewhat familiar. For example,
functions have a very similar syntax to those in Haskell. A function in Agda is
defined by declaring the type followed by the clauses.

\begin{minted}[breaklines,samepage]{Agda}
f : (x₁ : A₁) → ... → (xₙ : Aₙ) → B
f p₁ ... pₙ = d
...
f q₁ ... qₙ = e
\end{minted} 

Where \inline{f} is the function name, \inline{p} and \inline{q} are the
patterns of type \inline{A}. \inline{d} and \inline{e} are expressions. There
are other ways to define a function such as using dot patterns, absurd patterns,
as patterns and case trees \cite{10.1007/978-3-642-03359-9_6}.

With the above definition of type \inline{Bool}, let us define \inline{not}
function using pattern matching as:

\begin{minted}[breaklines,samepage]{Agda}
not : Bool → Bool
not false = true
not true = false
\end{minted} 

\inline{not} function takes an argument of type \inline{Bool}. The equal sign
(\inline{=}) is used to say that when a clause on the left-hand side of the
equal sign is seen, and the right-hand side is what's computed.

Similar to Haskell, Agda doesn't have the concept of multi-argument functions.
For example, to define addition (\inline{add}) function on natural numbers
(\inline{Nat}), we take an argument \inline{Nat} and return a function that
takes \inline{Nat} and returns \inline{Nat}.

\begin{minted}[breaklines,samepage]{Agda}
add : Nat → Nat → Nat
add zero m = m
add (suc n) m = suc (add n m)
\end{minted}

Operators in Agda are typically defined using symbolic notation or special
operator symbols. Addition as an infix operation can be defined in Agda as:

\label{code:Add}
\begin{minted}[breaklines,samepage]{Agda}
_+_ : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)
\end{minted}

In the above example, the function \inline{_+_} takes two arguments of type
\inline{Nat} and returns a value that is the sum of the two arguments of type
\inline{Nat}. The underscore symbol in the name specifies where the argument
goes. A recursive call must be made on a structurally smaller argument. For the
function \inline{_+_} above, the first argument \inline{n} is smaller in the
recursive call \inline{suc n}. Operators can have different associativity and
precedence rules. You can specify the fixity of operators to control how they
are parsed. For example,
\inline{infixl 5 _+_}

\section{Type Levels In Agda}
\label{level}
In the above section, we said \inline{Bool} is a type of kind \inline{Set}. What
we normally call \inline{Type} in programming, Agda calls it \inline{Set}. If
\inline{Set} is a type of type, is it possible that \inline{Set} is its own
type? If we make \inline{Set} a type of itself, then the language becomes
non-terminating \cite{AgdaTB}. 

Bertrand Russell introduced a paradox when defining the collection of all sets
and is called Russell's paradox. The naive set theory defines a set as
a well-defined collection of objects. The paradox \cite{russell2020principles}
defines the set of all sets that are not members of themselves. This develops
into two kinds of contradictions.
\begin{itemize}
  \item If the set contains itself, then it should not be a member of itself by
  definition
  \item If the set does not contain itself then it is not a member of itself.
\end{itemize}

In Martin-Löf's type theory, when we make a \inline{Set} its own type, it causes
inconsistency, by Girard's paradox \cite{coquand1986analysis}. To overcome this
paradox, Agda introduces a series of universes to create the type hierarchy, and
each universe represents a level of types \cite{sortSystem}. A universe is a
type whose elements are type \cite{universeagda}. This primitive type is useful
to define and prove theorems about functions that operate on large sets. In
Agda, not every type belongs to \inline{Set}. Since we cannot have a type
\inline{Set : Set}, Agda provides a hierarchy of universes \inline{Set},
\inline{Set₁}, \inline{Set₂} and so on. \inline{Set} stands for \inline{Set₀}
and it is the base universe. From the definition of \inline{Bool} discussed in
section \ref{types}, \inline{false} and \inline{true} is of type \inline{Bool},
the type of \inline{Bool} is \inline{Set}, \inline{Set} is of type
\inline{Set₁}, and so on. Agda doesn't allow types at a given level to depend on
types from higher universes.

We saw that in Agda, not every type belongs to \inline{Set}. Every type belongs
somewhere in the hierarchy \inline{Set₀}, \inline{Set₁}, \inline{Set₂}, and so
on. This definition works if we are comparing two values of some type in
\inline{Set}. But, we cannot compare two values that belong to \inline{Set ℓ}
for some arbitrary \inline{ℓ}. To solve this problem, Agda provides type
\inline{Level}. The type \inline{Set ℓ} represents the type of all types at
level \inline{ℓ}. For example, \inline{Set 0} represents \inline{Set₀},
\inline{Set 1} represents \inline{Set₁}, and so on. This type helps us to define
equality generalized to an arbitrary level.

\section{Equality}
\label{equality}
In Chapter 2, when defining theory, we said that an equation is of the form $t_1
= t_2$ where $t_1$ and $t_2$ are term expressions and $=$ represents equality
relation. In dependent type theory, equality is a complex concept. Equality says
that two things are "equal". But asking "when two things are equal" is
nontrivial. In this section, we discuss a hierarchy of "sameness" from
\cite{bocquet2020coherence} and \cite{eremondi2022propositional}.

\subsection{Syntactic Equality}
For some symbol $t_1 \text{and} t_2$, $t_1 = t_2$ if $t_1 and t_2$ are literally
the same symbols. This is called syntactic equality.

\subsection{Definitional Equality}
Definitional equality says that $t_1 = t_2$ when solving one symbol by applying
some definitions leads to syntactic equality. Two programs are equal if they
compute to the same value. For example, $(\lambda x \rightarrow x + y) 5$ and $5
+ y$ are the same. $5 + y$ is obtained when we compute the value of the
expression $ (\lambda x \rightarrow x + y) 5$.

When we write a function in Agda, we add defining equations to Agda's
definitional equality. For example, let us write a logical AND function
(\inline{_^_}) in Agda:

\begin{minted}[samepage,breaklines]{Agda}
_^_ : Bool → Bool → Bool
true ^ true = true
x ^ y = false
\end{minted}

In Agda, not every equation we write holds literally. In the above example,
only the equation \inline{true ^ true = true} holds. The equation \inline{x ^ y
= false} overlaps with the first equation when both $x$ and $y$ are
\inline{true}. This equation does not hold definitionally. In Agda, when pattern
matching, cases are tried in order from top to bottom. Agda will split the above
clause to three equations which holds definitionally \cite{abel2012agda}:
\begin{description}
  \item[] \inline{false ^ true = false}
  \item[] \inline{true ^ false = false}
  \item[] \inline{false ^ false = false}
\end{description}

Some fundamental rules that Agda follows for definitional equality are: 
\begin{itemize}
  \item \emph{Beta reduction} - We apply a lambda abstraction to an argument by
  substituting the argument into the body of the function. In Agda, we can
  replace the formal parameter of a lambda abstraction with an actual argument.
  This leads to the simplification of the expression.
  \item \emph{Congruence Rules} - If two expressions are equal, and you perform
  an operation on both expressions, the results should also be equal. In
  Agda, if two expressions are definitionally equal, we can replace the
  sub-expressions with equal expressions that will result in equal expressions.
  \item \emph{eta-expansion} - For the record definition \inline{Person} given
  in section \ref{types}, every \inline{ x : Person} is definitionally equal to
  \inline{record {name = Person.name x ; age = Person.age x}}. It is based on
  the principle that two functions are equal if they produce equal results for
  all possible arguments. 
\end{itemize}

We limit the scope of definitional equality here. Some references to find more
information about definitional equality are \cite{norell2007towards} and
\cite{martin1984intuitionistic}. 

\subsection{Propositional Equality}
When we write proof to say that two programs are equal, this proof may not be
a definitional equality. Instead, this proof itself can be a program that
expresses that two things are equal. In a universe polymorphic type system like
Agda, types are classified into various levels denoted as \inline{Set₀}, \inline{Set₁},
\inline{Set₂}, and so on. The definition of propositional equality in the Agda standard
library is universe polymorphic. That is a generic definition of propositional
equality is given using universes that can be used in different levels.

\begin{minted}[samepage,breaklines]{Agda}
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
\end{minted}

In the above definition, \inline{{a}} is an implicit parameter representing the
universe level of the set. In Agda, propositional equality \inline{_≡_} is
defined for any type $A$ and any element \inline{x} of type \inline{A}, the
identifier \inline{refl} provides evidence that \inline{ x ≡ x}. Therefore every
value is equal to itself and there is no alternative way to show values are
equal. From this definition of equality, we can prove that it is an equivalence
relation.

\begin{minted}[breaklines,samepage]{Agda}
sym : Symmetric {A = A} _≡_
sym refl = refl
\end{minted}

\begin{minted}[samepage,breaklines]{Agda}
trans : Transitive {A = A} _≡_
trans refl eq = eq
\end{minted}

We see how \inline{Symmetric} and \inline{Transitive} are defined in subsection
discussing equivalence.

\subsection{Equivalence}
In Agda's standard library, equivalence (\inline{_≈_}) is often preferred over
propositional equality (\inline{_≡_}) when defining algebraic structures
\cite{musa}. In Agda, equivalence is defined as a record type with three fields
to say that the relation is reflexive, symmetric and transitive:

\begin{minted}[breaklines,samepage]{Agda}
record IsEquivalence : Set (a ⊔ ℓ) where
  field
    refl  : Reflexive _≈_
    sym   : Symmetric _≈_
    trans : Transitive _≈_
\end{minted}

In the above code, \inline{IsEquivalence} is defined over for carrier \inline{A
: Set a} and binary relation \inline{_≈_ : REL A ℓ} that are parameters to the
module \inline{Relation.Binary.Core}. We see why modules are parameterized with carrier
set and equality relation later in the chapter when defining algebraic
structures. The field \inline{refl} is of type \inline{Reflexive  _≈_} and is
defined as:

\begin{minted}[breaklines,samepage]{Agda}
Reflexive : Rel A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x
\end{minted}

Where \inline{_∼_} is a relation of type {Rel A ℓ} that says for all element
\inline{x}, the elements are related to itself \inline{x ∼ x}. Type-level
functions refer to functions that operate on types rather than on values. They
are functions that take types as input and return types as output.

Symmetric relation is defined over a generalized symmetry that flips the order of arguments.

\begin{minted}[samepage,breaklines]{Agda}
Sym : REL A B ℓ₁ → REL B A ℓ₂ → Set _
Sym P Q = P ⇒ flip Q
\end{minted}
The first line declares \inline{Sym} that takes two arguments: \inline{P} of
type \inline{REL A B ℓ₁} and \inline{Q} of type \inline{REL B A ℓ₂}. Where
\inline{A} and \inline{B} are carrier sets over arbitrary universe level. The
module result type \inline{Set _}, where the underscore represents a universe
level that will be inferred. \inline{flip} is a function to flip the order of
the arguments. 

\begin{minted}[samepage,breaklines]{Agda}
Symmetric : Rel A ℓ → Set _
Symmetric _∼_ = Sym _∼_ _∼_
\end{minted}

\inline{Symmetric} uses the previously defined \inline{Sym} that states that a
relation \inline{_∼_} is symmetric if it satisfies the conditions of symmetry as
defined in the \inline{Sym}. \inline{Symmetric} will evaluate to type that
\inline{∀ x y : A}, \inline{x ∼ y → y ∼ x} for relation \inline{∼} of type
\inline{REL A ℓ}.

Similar to symmetric relation, transitivity is defined using generalized
transitive relation and \inline{Transitive} will evaluate to type that \inline{∀
i j k : A}, \inline{i ∼ j → j ∼ k → i ∼ k} for relation \inline{∼} of type
\inline{REL A ℓ}.

\begin{minted}[samepage,breaklines]{Agda}
Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

Transitive : Rel A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_
\end{minted}

\section{Structure Definition}
\label{structure}
A design decision was made in the Agda standard library to define algebraic
structures as a record type. The category theory library
\cite{hu2021formalizing} also follows the same design pattern to use record
types. There are several advantages to using record type:
\begin{itemize}
  \item Record types provide a convenient and flexible way to bundle
  together data and operations that satisfy certain algebraic properties. 
  \item Algebraic structures may have dependent relationships between their
  components. For example, the type of an identity element depends on the type
  of elements in the set. Record types support dependent types,
  allowing you to express these relationships accurately.
  \item Records behave as modules. This allows us to export symbols in record
  type and bring them to scope. We may also need to make sure doing so does not
  create ambiguity.
  \item Record types have good IDE support(via Emacs)
\end{itemize}

Let us now try to define \inline{IsMonoid}, an algebraic structure in Agda.
A monoid is an algebraic structure with a binary operation that satisfies
associativity and has an identity element. In Agda, we can define a structure as
a record type using the keyword \inline{record}. The record type allows to have
parameters immediately after the record's name declaration or may be declared
with \inline{field} keyword.

\begin{minted}[samepage,breaklines]{Agda}
record IsMonoid (A : Set) : Set where
  field
    e : A           
    op : A → A → A  

    assoc : ∀ {x y z} → op x (op y z) ≡ op (op x y) z
    leftId : ∀ {x} → op e x ≡ x
    rightId : ∀ {x} → op x e ≡ x
\end{minted}

In the above example, we see that \inline{IsMonoid} structure has a parameter
\inline{A : Set} with fields \inline{e} - the identity element and \inline{op} -
the binary operation. We give the laws of monoid structure as its field. Another
way to define a monoid structure is to parameterize the binary operation and the
identity element.

\begin{minted}[samepage,breaklines]{Agda}
record IsMonoid₀ {A : Set} (_∙_ : A → A → A) (ε : A) : Set where
  field
    assoc : ∀ {x y z} → op x (op y z) ≡ op (op x y) z
    leftId : ∀ {x} → op e x ≡ x
    rightId : ∀ {x} → op x e ≡ x 
\end{minted}

In the above definition, the carrier set \inline{A} becomes implicit and we
parameterize the operations of the structure. In theory, both the definitions
are the same. Using fields inside the record may provide a more encapsulated and
self-contained representation of the algebraic structure while having them after
the record name allows more flexibility in choosing the carrier set and
operation when creating instances of the record. 

From the above definition of \inline{IsMonoid₀}, when we try to define
\inline{IsGroup}\footnote{Group is an algebraic structure that is a monoid with
inverse operation.}, we see that both monoid and group have things in common.
They both have a carrier set (\inline{A}), a binary operation (\inline{op}), and
an identity element (\inline{e}). Given two structures that share some
components, expressing that sharing component becomes difficult \cite{musa}. To
overcome these difficulties, we may parameterize the sharing components like the
operations and the carrier set.

We may observe that all the algebraic structures have a carrier set. When
defining algebraic structures in a module, we can make the carrier set as the
argument to the module, so it is accessible by all the structures defined under
that module. The module declaration is treated as a top-level function that
takes the parameters of the module as arguments. The parameters can be values
and types but not other modules.

In section \ref{equality}, we introduced different ways to say when two things
are equal. When defining \inline{IsMonoid}, we used Agda's propositional
equality (\inline{_≡_}) to compare the terms. However, in practice, this
definition of propositional equality is too strong and one prefers to use a
finer equivalence relation \cite{musa}. Equivalence is useful when we want to
capture "sameness" in a more flexible way. Agda standard library gives a binary
relation as an argument to the module and equivalence relation
(\inline{isEquivalence}) as a field to the \inline{IsMagma} (defined later in
the chapter) structure from which other structures are extended.
 
\begin{minted}[breaklines,samepage]{Agda}
  module Algebra.Structures
    {a ℓ} {A : Set a} 
    (_≈_ : Rel A ℓ)
    where
  \end{minted} 

In the above code, we see that the Agda standard library allows us to define things at
some arbitrary level. \inline{A} is a \inline{Set} in some level \inline{a} and
\inline{_≈_} is a homogeneous binary relation \inline{Rel} on universe \inline{A
ℓ}.

Now we can define a magma structure in Agda with equivalence as:

\begin{minted}[samepage,breaklines]{Agda}
record IsMagma₀ {A : Set} (_∙_ : A → A → A) : Set where
  field
    isEquivalence : IsEquivalence _≈_
\end{minted}

Although the equivalence allows us to compare the terms, it becomes restrictive
to play with equal terms. In this case, we can use congruence which says that if
two elements are equivalent, then applying certain operations to them should
yield equivalent results. For example, let \inline{≈} be an equivalence relation
on a set $S$ and operation $f: S × S → S$. The operation $f$ is said to be
congruent with respect to the equivalence if, for all $a, b, c, d \in S$, $a ≈
b$ and $c ≈ d$, then $f(a, c) ≈ f(b, d)$. Therefore when defining a structure we
give congruence with the operation.

Let us understand how algebraic structure is defined in the Agda standard
library. An algebraic structure is defined in the Agda standard library as a
record type using the \inline{record} keyword. The structures are obtained by
wrapping the predicates that are expressed as "is-a" relation
\cite{hu2021formalizing}. The types of algebraic structures are defined in
module \inline{Algebra.Structures} that have an underlying set \inline{A} and a
homogeneous binary relation \inline{_≈_}. The following example shows how to
characterize magma structures in Agda:

\begin{minted}[breaklines,samepage]{Agda}
record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∙-cong        : Congruent₂ ∙

  open IsEquivalence isEquivalence public
\end{minted}

In the above example, structure \inline{IsMagma} is defined as a record type
with a parameter \inline{Op₂ A}. The properties of the structure
\inline{IsMagma} are declared as the fields of the record, which include
equivalence (\inline{isEquivalence}) and congruence (\inline{∙-cong}).
\inline{∙} is a binary operation on the set \inline{A}. \inline{a ⊔ ℓ} gives the
largest of two levels. \inline{_≈_} is the binary operation argument for
\inline{IsEquivalence}. \inline{IsEquivalence} and \inline{Congruent₂} are
predicates defined in standard library. We open the module
\inline{isEquivalence} to bring its definition into scope. The open statement is
made public using the keyword \inline{public} to be able to re-export the names
from another module.

In the above definition, we see \inline{(∙ : Op₂ A)}, the binary operation.
Instead of writing \inline{A → A → A}, the Agda standard library defines a
type-level function \inline{Op₂}.

\begin{minted}[breaklines,samepage]{Agda}
  Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
  Op₂ A = A → A → A
\end{minted}

The subscript 2 represents that it is a binary operation. Similarly, the
standard library defines \inline{Op₁}:

\begin{minted}[breaklines,samepage]{Agda}
  Op₁ : ∀ {ℓ} → Set ℓ → Set ℓ
  Op₁ A = A → A
\end{minted}

Although parameterized structures are same as the unparameterized (unbundled)
versions, in practice there may be certain presentations that are useful. Paper
\cite{al2019language} discusses ways to unbundle a structure at will. When
building a library, it is not practical to provide all ways of parameterized
structures. Agda standard library provides a bundled version of the structures.
The bundled version of the structures contains the operations of the structures,
sets and axioms. Agda standard library defines the raw representation of a
theory that is the definition of its signature. \inline{RawMagma} in Agda
standard library is defined as:

\begin{minted}[samepage,breaklines]{Agda}
record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier

  infix 4 _≉_
  _≉_ : Rel Carrier _
  x ≉ y = ¬ (x ≈ y)
\end{minted}

\inline{_≉_} is the inequality relation that states that two elements are not
equal \inline{ x ≉ y} if they are not equal under the equivalence relation.
Bundled version structures are defined by importing structures from
\inline{Algebra.Structures} so we can parameterize the definitions with equality that
is used to compare the terms of the structure.

\begin{minted}[breaklines,samepage]{Agda}
record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isMagma : IsMagma _≈_ _∙_

  open IsMagma isMagma public

  rawMagma : RawMagma _ _
  rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }

  open RawMagma rawMagma public
    using (_≉_)
\end{minted}

Above is the bundled version of \inline{IsMagma} structure. \inline{RawMagma} is
the raw version of the magma with only the operators and set. infix<l,r> denotes
the fixity and precedence of the operator. The operator with higher fixity binds
more strongly than an operator with a lower numeric value. \inline{_≈_} defines
equality used to compare terms of \inline{Magma}. \inline{using} keyword is used
to limit the imported components. 

Before we finish discussing the structure definition, there is one important
concept to discuss that is \emph{renaming}. Although the choice of name is
theoretically irrelevant, renaming is often used to provide more generic and
consistent naming conventions, making the library easier to use and more
accessible to users. The Agda standard library uses certain conventions for
renaming. Keyword \inline{renaming} is used to rename the fields. Consider the
below example:

\label{code:rename}
\begin{minted}[breaklines,samepage]{Agda}
  record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isMonoid    : IsMonoid + 0#
    *-cong        : Congruent₂ *
    *-assoc       : Associative *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

  open IsMonoid +-isMonoid public
    renaming
    ( assoc         to +-assoc
    ; ∙-cong        to +-cong
    ; ∙-congˡ       to +-congˡ
    ; ∙-congʳ       to +-congʳ
    ; identity      to +-identity
    ; identityˡ     to +-identityˡ
    ; identityʳ     to +-identityʳ
    ; isMagma       to +-isMagma
    ; isUnitalMagma to +-isUnitalMagma
    ; isSemigroup   to +-isSemigroup
    )

  *-isMagma : IsMagma *
  *-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = *-cong
    }

  *-isSemigroup : IsSemigroup *
  *-isSemigroup = record
    { isMagma = *-isMagma
    ; assoc   = *-assoc
    }

  open IsMagma *-isMagma public
    using ()
    renaming
    ( ∙-congˡ  to *-congˡ
    ; ∙-congʳ  to *-congʳ
    )
\end{minted} 
We use \inline{using}, \inline{hiding}, and \inline{renaming} to control which
names are brought into scope. From the above example, we see that for addition
operation (\inline{+}), the fields of the form $\mathscr{X}$ are renamed to
$+-\mathscr{X}$. \cite{musa} proposes packaging the renaming to helper modules.
However, as new algebraic structures are added to the library, it becomes
more difficult to maintain the conventions and requires carefully defining the
structures.  

\section{Homomorphism In Agda}
\label{morphism}
A homomorphism is a structure-preserving map between two structures. For two
magma structures $(A,∙)$ and $(B,◦)$, a homomorphism  \(f\) : \(A \ \rightarrow
\ B\) is defined as:
\[f(x\  ∙ \  y) \ = \ f(x) \ ◦ \  f(y)\] 

In Agda, homomorphism for two magma structures is defined as a record type:

\begin{minted}[breaklines,samepage]{Agda}
module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) where

  open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
  open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)

  record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
    homo              : Homomorphic₂ ⟦_⟧ _∙_ _◦_

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

The \inline{raw structures}, in the above example, \inline{RawMagma} is the
definition of the signature of the structure. \inline{IsMagmaHomomorphism} is a
record type with fields \inline{isRelHomomorphism} and \inline{homo}. Since the
formalization of the types of algebraic structures in Agda is based on setoid,
\inline{IsRelHomomorphism} is defined for homomorphism between the homogeneous
equivalence relations \inline{_≈₁_} and \inline{_≈₂_}. \inline{Homomorphic₂} is
defined for two binary operations as:

\begin{minted}[samepage,breaklines]{Agda}
Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Set _
Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)
\end{minted}

From this definition of homomorphism, monomorphism of the structure is given as:

\begin{minted}[breaklines,samepage]{Agda}
  record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
    injective           : Injective ⟦_⟧

  open IsMagmaHomomorphism isMagmaHomomorphism public
\end{minted}

\inline{IsMagmaMonomorphism} is defined as a record type with field
\inline{isMagmaHomomorphism} and \inline{injective}. The \inline{Injective}
function is a one-to-one map defined as:

\begin{minted}[samepage,breaklines]{Agda}
Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
\end{minted}

where \inline{_≈₁_} is the equality over the domain \inline{A} and \inline{_≈₂_}
is the equality over codomain \inline{B}.

Isomorphism of a structure can be derived from monomorphism with surjectivity.

\begin{minted}[samepage,breaklines]{Agda}
record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
    surjective          : Surjective ⟦_⟧

  open IsMagmaMonomorphism isMagmaMonomorphism public
\end{minted} 

\inline{IsMagmaIsomorphism} is defined as a record type with field
\inline{isMagmaMonomorphism} and \inline{surjective}. A surjective relation
requires equality (\inline{_≈₂_}) on the codomain \inline{B} and is defined as:

\begin{minted}[samepage,breaklines]{Agda}
Surjective : (A → B) → Set (a ⊔ b ⊔ ℓ₂)
Surjective f = ∀ y → ∃ λ x → f x ≈₂ y
\end{minted}

\section{Product Algebra}
\label{directproduct}
Recall the definition of product, direct product, and direct sum discussed in
Chapter 2. A co-product of an algebra is the dual of the product algebra
\cite{sannella2012foundations}. A bi-product of algebra is an algebra that is
both a product and a co-product. The standard library defines objects that are
products of appropriate algebras and calls them direct products. In many cases,
the bi-product coincides with the direct product when certain conditions are met
\cite{szabo2000linear}. For the scope of the thesis, we do not consider this
distinction. There is currently an
\MYhref{https://github.com/agda/agda-stdlib/issues/1907}{issue} in the standard
library to address this problem. 

The difference between a direct product and a cartesian product is mainly
related to the type of mathematical structures you are dealing with. Cartesian
product refers to sets with no additional structure. The Cartesian product of
two sets $A$ and $B$, denoted as $A × B$, is a new set that contains ordered
pairs $(a, b)$ where $a$ is an element from set $A$, and $b$ is an element from
set $B$. A direct product typically deals with algebraic structures, such as
groups, rings, or vector spaces.

The products of various structures are defined under the module
\mintinline[breaklines,breakafter=.]{Agda}{Algebra.Construct.DirectProducts} in
the Agda standard library. The product of magma structure is defined as:

\begin{minted}[breaklines,samepage]{Agda}
magma : Magma a ℓ₁ → Magma b ℓ₂ → Magma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
magma M N = record
  { Carrier = M.Carrier × N.Carrier
  ; _≈_     = Pointwise M._≈_ N._≈_
  ; _∙_     = zip M._∙_ N._∙_
  ; isMagma = record
    { isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence
    ; ∙-cong = zip M.∙-cong N.∙-cong
    }
  } where module M = Magma M; module N = Magma N
\end{minted}

where \inline{Magma} is the bundled version of the magma structure. The carrier
set for the direct product of \inline{M} and \inline{N} is the product $M \times N$.
\inline{Pointwise} gives the product of relations (\inline{_≈_}) in \inline{M}
and \inline{N}. \inline{zip} gives a $\Sigma$-type of dependent pairs.
\inline{×-isEquivalence} is the product of equivalence relations in \inline{M}
and \inline{N}.

\section{Equational Proofs In Agda}
\label{proof}
A proof is a sequence of steps that transform one expression into another using
a set of rules. Agda allows us to declare properties of functions and data types
that need to be verified by the compiler \cite{kidney2020finiteness}. A
constructive equational proof in Agda refers to the process of proving a logical
proposition using equational reasoning within Agda's type system
\cite{murray2022constructive}. 

In section \ref{types}, we have seen how to define natural numbers and addition
function on it. Now, we will write an inductive proof using pattern matching
that states that the addition of two natural numbers is commutative.

\begin{minted}[breaklines,samepage]{Agda}
comm : ∀ (m n : Nat) → m + n ≡ n + m
comm zero zero = refl
comm zero (suc n) = cong suc (comm zero n)
comm (suc m) n = cong suc (comm m n)
\end{minted}

In the above example, we see three cases:
\begin{itemize}
  \item Case 1: When \inline{comm zero zero}, that is $m = n = 0$. Then
  \inline{zero + zero = zero} holds by reflexivity. The proof \inline{comm zero
  zero} represents commutative property where both \inline{m} and \inline{n} are
  \inline{zero}. The \inline{refl} function is used to prove that two expressions
  are equal using the reflexivity of equality.
  \item Case 2: \inline{comm zero (suc n)}, in this case, \inline{m} is \inline{zero}
  and \inline{n} is a successor of some natural number. The proof proceeds
  recursively using induction on \inline{n}. The recursive assumption is that
  \inline{comm zero n} is already proved. That is \inline{zero + n = n + zero}.
  Using this assumption, we can conclude that \inline{zero + suc n} is equal to
  \inline{suc n + zero}, by incrementing both sides of the equation with
  \inline{suc}.
  \item Case 3: \inline{comm (suc m) n}, In this case, \inline{m} is a successor
  of some natural number, and \inline{n} can be any natural number. The proof
  uses induction on \inline{m}. The inductive step relies on the assumption that
  \inline{comm m n} is true. The proof applies the successor function
  \inline{suc} to both sides of the equation, to show that \inline{suc m + n} is
  equal to \inline{n + suc m}.
\end{itemize}
In algebraic structure, consider the example of the proposition that $x ∙ (y ∙
z) = y ∙ (x ∙ z)$ for a commutative semigroup i.e., a Magma with associativity
$(x ∙ (y ∙ z) = (x ∙ y) ∙ z)$ and commutativity $(x ∙ y) = (y ∙ x)$. The proof
can be written in Agda as:

\begin{minted}[breaklines,samepage]{Agda}
x∙yz≈y∙xz :  ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (x ∙ z)
x∙yz≈y∙xz x y z = begin
  x ∙ (y ∙ z)    ≈⟨ sym (assoc x y z) ⟩
  (x ∙ y) ∙ z    ≈⟨ ∙-congʳ (comm x y) ⟩
  (y ∙ x) ∙ z    ≈⟨ assoc y x z ⟩
  y ∙ (x ∙ z)    ∎
\end{minted}

To make proofs more readable, people have tried to emulate textual proofs, for
example, by creating "begin" and "end" syntax. \inline{begin} indicates the
start of the proof. \inline{begin_} is a function that takes two type arguments
\inline{x} and \inline{y}, and an argument of type x IsRelatedTo y. It returns a
proof that \inline{x} is equivalent \inline{(∼)} to \inline{y}. The function
simply uses pattern matching to extract the proof \inline{x∼y} and returns it.

\begin{minted}{Agda}
begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
begin relTo x∼y = x∼y
\end{minted}

\inline{IsRelatedTo} is a type defined to infer arguments even if the underlying
equality evaluates. Standard step to relation is defined as \inline{step-∼}.

\begin{minted}[breaklines,samepage]{Agda}
step-∼ : ∀ x {y z} → y IsRelatedTo z → x ∼ y → x IsRelatedTo z
step-∼ _ (relTo y∼z) x∼y = relTo (trans x∼y y∼z)
\end{minted}

The \inline{step-∼} function provides a way to extend an equational proof using
the relation \inline{IsRelatedTo} while maintaining the equality \inline{(∼)}.
It takes an initial proof that \inline{x ∼ y}, a proof \inline{relTo y∼z} of
\inline{y IsRelatedTo z}, and produces a proof of \inline{x IsRelatedTo z}. The
\inline{trans} is the transitivity used to combine two proofs of relatedness.

The \inline{step-≈} gives convenient syntax for invoking the \inline{step-∼}.
step using equality is given as:

\begin{minted}[breaklines,samepage]{Agda}
step-≈ = Base.step-∼
syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z
\end{minted}

It provides a syntax shortcut for using the \inline{≈⟨ ⟩} notation, which allows
you to chain relatedness proofs using equational reasoning.

The termination (i.e., QED) of the proof is given using \inline{_∎} that relates
object to itself.

\begin{minted}[breaklines,samepage]{Agda}
_∎ : ∀ x → x IsRelatedTo x
x ∎ = relTo refl
\end{minted}