Agda is an interactive theorem prover/functional programming language which boasts a Haskell-like syntax and very strict reasoning. What this means is that reasoning in Agda is very much similar to the reasoning in formal Type Theory without the sugar-coating of tactics. While this is a very raw-bones approach, it does have several advantages, first of which is close control over what is exactly happening when one defines functions and how one invokes case analysis. Certainly, philosophically it is much more rigorous writing down the recursion and induction principles for types oneself instead of having them be generated automatically as is done in Coq.
Moreover, a person interested in contemporary developments of HoTT will be happy to hear that Agda also has support for cubical type theory!
With that said, let us delve into what one needs to start up using Agda. Now, as we have mentioned, Agda is very bare-bones as it very much resembles the formal argumentation in type theory. The upside of that is that there are very few things one needs in order to successfully use to close to full capacity.
Depending on how you installed Agda, once you launch your .agda file in the editor, you will need to start up the Agda mode, which is called "loading." Loading happens at all at once, i.e. is not incremental, by pressing Ctrl+C Ctrl+L. There are no steps like in Coq, so be careful not to write out too much in between the checks, as you may get lost in the error messages. Hence we should try to load Agda as much as possible whilst defining new stuff. You can be successfully working with Agda with a belief that there are only two ways of doing stuff: defining inductive types and defining functions, which are represented by two different procedures. Let us start with inductive types.
Agda knows that you are about to present it with an inductive definition for a type by typing "data" at the beginning of the line. Afterward, we provide a name for our type, where it belongs type-wise and its constructors. Here is our canonical example of natural numbers (note that the double lines on the side specify comments in Agda, i.e. make everything on the line a comment):
data ℕ : Set where -- "where" is a stand-in for the start of the definition
zero : ℕ -- note the space at the beginning of the line here
succ : ℕ → ℕ -- and here
(alternatively, one can also enclose comments in {- -} brackets )
Note that Agda seems to be, unlike Coq, very smart in understanding which elements ought to be constructors. This is a visual lie that is present only when looking at isolated cases. Earnestly, it hinges on the "hidden" syntax of spaces and indents. What this means is that making spaces between certain elements is a big deal for Agda so once should use spaces sparingly, it is a resource, rather than a cosmetic appliance as in Coq. For example, above we can see that before zero and succ generators there is a space. This means that we are signaling to Agda, after the declaration of the name for an inductive type, that these are specifically its constructors. As long as we are doing indents in the next line, we are letting Agda know that we, apparently want that next line to be yet another constructor. This may cause a lot of errors, so be careful. The burdensome extra notation of Coq is here supplanted by making the user extra-careful. A good hint is thinking of the indentations as markers that indicate that the specified element ought to be structurally "in" the defined object. Admittedly, it is a bit of a faulty intuition and one will see why when we come to defining terms.
Now, let us unfold some extra notation and architecture simply looking at the above definition. As usual, specifying zero and succ (and then stopping, i.e. not adding any more generators) is equivalent to a semantic statement that there are precisely two ways of making sure we have an element of ℕ , namely, it is either zero, or, given some natural number, we can apply succ to it to produce its element. This is standard, generators are just straightforward formalization of the construction rules of types. Similarly, defining the coproduct, we will specify its constructors as left and right injections belonging to function types from the respective types to the coproduct.
Similarly, we will define our bool 𝔹 as generated by true and false, and unit 𝕌 as generated by one element tt. The empty type 𝟘 is generated by nothing. Here is the Agda code pertaining to our definitions:
data 𝔹 : Set where
true : 𝔹
false : 𝔹
data 𝕌 : Set where
tt : 𝕌
data 𝟘 : Set where
Once again: note the spaces. Being pedantic, we should also say that the definition for the empty type is not correct above as the user may screw up the definition if they write anything after it in Agda with a space. So, the best part about writing tutorials for Agda is that - formally - all the code you posted is not prima facie correct.
Even if the inductive definitions are given, however, nothing else is, once we have defined our type. That means no recursors or inductive principles available for direct use. Those will have to be defined separately, with analysis by cases Agda has. That is, what it does have is an automatic possibility of defining functions by constructor cases on terms of inductive types, which gives us enough expressive power to define recursion and inductive principles.
The "where" command is the central one in Agda for inductive definitions, specifying the start of constructors specifications.
Note that we gave the naturals the name ℕ here for a reason: Agda has an inbuilt support for Unicode, making the environment extremely friendly for us mathematicians, even if the code is sometimes not that straightforward (for example ℕ is given by \bN and ≡ by \==). However, there are numerous cheatsheets for symbols available online for those in need.
The usage of Unicode also means that some Unicode characters are prebuilt into our type theory, specifically when encountering Pi-types and function types, the former is specified by ∀ (written \forall) and the latter by → (written \to). With function types the notation is evident, i.e. between two types A and B we have a function type A → B. For the Pi-type we have some additional notation to specify. Once we have declared our ranges, for example (A : Type) and (a : A) and some family P : A → Type, we have our Pi-type ∀ (A : Type) (a : A) → P a. So the forall symbol, firstly, gets used on several variables of different types in a row, following the usual convention, and, secondly, announces the codomain via specifying it as a function to a type family applied to a chosen element in its domain via the → symbol. Note that the argument information is usually parsed via parentheses.
Also notice that "Set" is a stand-in for a universe. Quite an unfortunate naming, specifically for those interested in HoTT, yet sometimes life is just unfair. Note that Agda here differs from Coq. It cannot infer universe levels and instead, if a level is left unspecified, thinks that the type is located at level zero. So saying that "A : Set" means that A is a type at the o-th universe level. The levels for universes can be provided explicitly as well, by specifying an explicit variable - seemingly typeless - for then to be mentioned near Set once you declare your types. However, for that, it is usually best to load some additional data from Agda, in order to have a proper understanding of what is going on with the universes. Even if the whole philosophy of these tutorials is to work "library-free," if you want to specify universe levels explicitly, type in
open import Agda.Primitive public using (Level; lzero; lsuc; _⊔_; Setω)
at the beginning of the page. We will see an example of level-specification right away, in our examples of infix notations, which will finish up our discussion of inductive types.
A very useful feature of Agda is the ability to specify notations as infix right at the very definition. That is, we have a way to define - for example - inductive types of two arguments in Agda in a way that will treat its name both as a prefix name for a function and as an infix name with arguments on both sides. To see how this plays out, let us define an already mentioned coproduct type:
data _+_ {l1 l2 } (A : Set l1) (B : Set l2) : Set (l1 ⊔ l2) where
inl : A → A + B
inr : B → A + B
This seems to be a much more complex definition that we gave before, and mainly due to specifying the levels for our universes. However, we will return to these points soon, let us first talk about the infix notation.
Here, we have specified that we have a function of two arguments (where these two arguments are types from two universes) that we named +. Moreover, we have specified that it is a function that can be put between the two types and still work the needed way, by putting underscored on its sides, making _+_. In this way, we are able to make any sort of a two-placed function infix by underscoring it on its sides. However, that does not stop the function from being able to be used prefix as well. So if A and B are types we have that "A + B" and "_+_ A B" designate the same type: the coproduct of A and B.
Generally, defining the infix notation by underscoring is enough, yet if Agda asks for - or if you simply want to - impose the binding on the notation, i.e. how rightly does the infix bind, simply type in
infixl n _foo_
where n is the level of binding (the higher, the tighter), and "_foo_" is the name of the function. One can put several functions in the same line after a space to designate that it belongs to the same binding level.
Now, one should be ready to point out that in truth our function has 4 arguments instead of two if we count the universe levels we needed to declare, in which case the infix notation will not be of much use. However, we have a way of making Agda forgive us for not telling it an additional structure which it can guess itself. For example, Agda will surely guess the levels of A and B if we give it A and B, as they already belong to some universe of some level. So what we can do is instead put the information about the levels in curly - rather than round - brackets. This makes the arguments closed inside such brackets implicit and treat functions of many arguments as functions of few, given that Agda can infer them from the explicit variables. If it does not do it successfully, one can always provide implicit arguments explicitly by writing it out in the needed place in curly brackets. So, if A is in Set l1 and B is in Set l2 we can say that "_+_ {l1} {l2} A B" is well-typed. Moreover, maybe we want to avoid mentioning the level of B not to overburden our notation. So, for some reason we only want to specify the level of A. We can do this by writing "_+_ {l1} {_} A B". Generally, the underscore allows the user to leave unessential arguments and variable declarations implicit. As long as they are indeed unimportant, Agda should be able to figure out their importance itself and allow you to skip it (or, again, just infer the implicit argument when there is enough information). So, remember, if you feel lazy and think that something is evident or can be skipped (in terms of arguments), just put underscores.
Generally, the infixes are not the only way one can conveniently define functions. There are also ways of naturally defining truncation notation (that is, if P is a type, then ∥P∥ is its truncation) by naming our inductive type ∥_∥ and making explicit only the type that we will want to truncate. Note that this does not mean that one can define truncation in Agda easily. Both Coq and Agda do not have native support for higher inductive types, which makes their implementation rather... tasteless. One is encouraged to consult outside sources on the formalization of HITs in Agda.
Let us talk about universe levels for a bit as well. Generally, when we have two types and generate a third one (product, coproduct, function, etc) we have a type whose level is one that is the largest of the two universes that we were given in the beginning. The way that Agda goes about it is to say that its level is "l1 ⊔ l2" if the levels of the first two are l1 and l2. The symbol is written as \lub and is, of course, a stand-in for the least upper bound. If you want to talk about the properties of a next-level universe you can also - given some level l - talk about "Set (lsuc l) ". We should also mention that levels do have an explicit type, which one can put them in during specification, namely, they live in the type Level, so one can write "l1 l2 : Level," so we have our universe polymorphism inside of Coq.
One will also be happy to hear that Agda has support for cumulative universes (although not natively, so be wary of using cumulative arguments from the get-go)! In order to explain how to launch the environment for supporting cumulativity, we need to mention pragmas, which are commands in brackets which interact with the Agda libraries. So, declaring
{-# OPTIONS --cumulativity #-}
automatically makes our universes cumulative.
This finishes up our preliminaries and discussions of inductive types. We move on to function definitions and the usage of the functional apparatus of Agda. Functions are declared right away without the need to write any additional markups. If you want to declare a function: just start with its name. Here, the same goes for both recursive and usual functions. No separation a-la Coq is needed. Structurally, they will appear the same.
The discussion of functions with examples may be a bit complicated with Agda compared to Coq, since Agda is interactive inasmuch as the user is in the middle of the proof. As soon as the proof is finished, it simply checks that all the information is in place and the function is defined. In short, once the function is declared, there is no explanation of how one got there, just the pure result and the fact that it is correct. Nevertheless, it offers very straightforward and intuitive interaction in the process of the proof which we will try to textually show using the definition of addition for natural numbers.
Here is how it looks finalized (note that we will use _plus_ since we have already declared _+_ to be a function of two type arguments, which we will certainly encounter more than the natural numbers):
_plus_ : ℕ → ℕ → ℕ
zero plus m = m
(succ n) plus m = succ (n plus m) -- note the lack of spacing
This is nothing interesting, really (although note the lack of indenting). To give a recursive definition, we need to give a definition on cases with a possible use of a lower-value of our variables. This is exactly the way that Agda wants its recursive definitions to be given as well. Yet the above is the end-product. The real interest is in how can we get there. Sure, we can just paste that definition, but as a beginner (and once you encounter some complicated functions) you will need pointers as to how to get their values, i.e. you will want to interact with the theorem prover.
So, suppose we want to start defining _plus_. The way you do it is by providing an explicit function depending on which type does _plus_ lie in. In our case, it lies in ℕ → ℕ → ℕ, so we specify our input using infix notation: n plus m, so that we declare our first variable to be n and our second to be m, both taken from our natural numbers. Then, to declare how we want to define it, we insert the proper equality "=" symbol, which functions in Agda solely as a definitional equality symbol used in defining functions (that is, we will need to define equality later, which this tutorial will do explicitly). So, what we have present is
_plus_ : ℕ → ℕ → ℕ
n plus m =
At this point, we want some help from Agda. The way we do it is by literally putting in the question mark "?" after the equality and loading Agda. Hence we start with
_plus_ : ℕ → ℕ → ℕ
zero plus n = ?
and after loading - pressing Ctrl+C Ctrl+L - we get something akin to this (results may vary depending on the editor, we are using the VSCode Agda Mode extension):
_add_ : ℕ → ℕ → ℕ
n add m = {! 0!}
Alongside that, the goal line changes to indicate what exactly should the intestines of the brackets include. In our case, we need to produce a natural number, hence the goal is "?0 : ℕ". What we need in our definition here, as we have mentioned, is the case analysis on constructors. The way to make Agda consider this is by first clicking into the brackets, to let Agda know that you are considering this specific gap, then pressing Ctrl+C Ctrl+C, which will prompt a line at the bottom of your IDE saying something about considering cases. Enter the needed variable there, press enter, and Agda will do case analysis on that variable. So, in our case, we put in "n" in the box, and then press enter, getting
_add_ : ℕ → ℕ → ℕ
zero add m = {! 0!}
succ n add m = {! 1!}
Now, we are ready to wholeheartedly define our function. In the first placeholder, we type in "m" and then press Ctrl+C Ctrl+Space in order for Agda to accept out value. Of course, for the second definition, we need to use the lower-level value of the function, which we can do straightforwardly: Agda does not need additional commands to accept recursive arguments. So we simply type in "succ (n add m)", press Ctrl+C Ctrl+Space once more and we are done.
Since this is the last instance in which we will mention the natural numbers in a computational context, let us mention a pragma concerning the natural numbers, namely
{-# BUILTIN NATURAL ℕ #-}
which makes your file understand "0" as "zero," "1" as "succ zero", etc. Of course, this also works for any name of your naturals, simply replace ℕ in the pragma there and this will work. Other pragmas import specific definitions from the main library, so you may be interested in looking at the possibility of using those if you are a bit hesitant in defining all the supplementary material you may not need other than in specific circumstances.
We are, of course, also capable of producing more complex inductive definitions, even if a bit less intuitively than we usually do in mathematics. For example, let us consider a function evaluating whether a number is even and define it by a two-level induction:
evenb : ℕ → 𝔹
evenb zero = true
evenb (succ zero) = false
evenb (succ (succ n)) = evenb n
The definition looks standard, yet the way that Agda will aid you to present it is very matter-of-factural, that is - as we mentioned - by double induction. You will fist ask Agda to aid with "evenb n" with n our stand in for a natural number, then you will proceed by cases on n. Next, you fill in "true" for the base case and wonder what to do with "succ n." Since n is a term of an inductive type, Agda will understand you asking do do cases on n once again, this time producing
evenb : ℕ → 𝔹
evenb zero = true
evenb (succ zero) = {! 0!}
evenb (succ (succ n)) = {! 1!}
which allows us to finish the definition. Remember, as long as Agda sees any variable of an inductive type, it allows case analysis of it.
Let us also consider recursion on several variables by thinking about conjunction operation on booleans:
conj : 𝔹 → 𝔹 → 𝔹
conj b1 b2 = {! 0!}
Now, we proceed by case analysis on, firstly, b1, which gives us
conj : 𝔹 → 𝔹 → 𝔹
conj true b2 = {! 0!}
conj false b2 = {! 1!}
with the latter hole that needs to be closed up with "false". Now, to close up the first one, we need to also conduct case analysis on b2, which is naturally done for Agda in the usual manner of pressing Ctrl+C twice. Hence we end up with the complete definition of
conj : 𝔹 → 𝔹 → 𝔹
conj true true = true
conj true false = false
conj false b2 = false
This provides basically all the needed introduction to the practical functionality fo Agda and its bare bones. As mentioned, the system is indeed very rigorous and lacking in sugar, so everything else is basically up to the user. For the sake of being complete, let us stop to talk about our recursions/inductions and the important facts for practicing HoTT.
So, we have mentioned that the case analysis Agda provides is enough to specify our recursors and inductions. Let us back that up with two examples. First, let us recall our coproduct and define its recursors and induction principles.
rec+ : ∀ {l1 l2 l3} {A : Set l1} {B : Set l2} {C : Set l3} →
(A → C) → (B → C) → (A + B → C)
rec+ f g (inl x) = f x
rec+ f g (inr x) = g x
ind+ : ∀ {l1 l2 l3} {A : Set l1} {B : Set l2} {C : A + B → Set l3} →
( ∀ (a : A) → C (inl a)) → ( ∀ (b : B) → (C (inr b)) ) → ( ∀ (x : A + B) → C x)
ind+ f g (inl x) = f x
ind+ f g (inr x) = g x
In terms of syntax, note that when one wants to spread the type of the function over different lines, never simply go by "Enter," since that will make Agda think that you already started defining some poorly typed function. Use the space key - or double-space or tab - to indent your definition in a way that signals to Agda that you have not finished defining the type of the term. Secondly, be wary of using underscores in the names of your terms. Underscores are quite powerful in Agda, meaning that their use usually wreaks havoc on the interpretation by the checker. So try to never use underscores other than in specifying where the arguments go while defining functions.
These definitions work perfectly fine, since when we start defining, our functions - take, for example, the recursor - we start with needing to specify the value of "rec+ f g x". Asking Agda for help can allow us to do case analysis. Choosing "x" as the needed variable to split up produced two subgoals
rec+ : ∀ {l1 l2 l3} {A : Set l1} {B : Set l2} {C : Set l3} → (A → C) → (B → C) → (A + B → C)
rec+ f g (inl x) = {! 0!}
rec+ f g (inr x) = {! 1!}
due to the fact that the "x" is the term of the coproduct, which has two generators, namely, inl and inr. One can note that recursors are pretty much embedded into Agda through case analysis, so we basically lied at the beginning, yet for the greater good at being able to show the formulation of recursors and inductions directly inside our system.
Similarly, we have our definition of the equality as the inductive type generated by the constant path:
data _≡_ {l} {A : Set l} : A → A → Set l where
refl : ∀ {a} → a ≡ a
In which case we can define our induction principle by
ind== : ∀ {l1 l2} {A : Set l1} →
(C : (x y : A) → x ≡ y → Set l2)
(t : (a : A) → C a a refl) →
(x y : A) → (p : x ≡ y) → C x y p
ind== C t a a refl = t a
Which works by case analysis on "p" when considering the value of "ind== C T x y p."
Of course one is also capable of defining functions explicitly via mapping notation. There are multiple ways of making Agda look at your definition of a function as a mapping, yet the most readable and canonical one is always λ (written as \lambda, of course). So, we can, for example, define function composition by
_∘_ : ∀ {l1 l2 l3} {A : Set l1} {B : Set l2} {C : Set l3} (f : B → C) (g : A → B) → (A → C)
f ∘ g = λ x → f (g x)
or, equivalently by
_∘_ : ∀ {l1 l2 l3} {A : Set l1} {B : Set l2} {C : Set l3} (f : B → C) (g : A → B) → (A → C)
(f ∘ g) x = f (g x)
We, however, did not yet show how to use inductions in action other than in trivial cases. For this purpose, let us return to the natural numbers once more in order to provide the most intuitive demonstration. First, let us define an induction term for the natural numbers:
indℕ : ∀ {l1} (C : ℕ → Set l1) → (C zero) →
(forall (n : ℕ) → (C n → C (succ n) )) →
∀ (n : ℕ) → C n
indℕ C p q zero = p
indℕ C p q (succ n) = q n (indℕ C p q n)
And function application for equalities:
ap : ∀ {l1 l2} {A : Set l1} {B : Set l2} {x y : A} (f : A → B) →
(x ≡ y) → ( f x ≡ f y)
ap f refl = refl
Now, let us prove something using induction, like the associativity of naturals. This will also showcase how alternate and more complicated way of reasoning works in Agda.
So, we first define our proof as belonging to an appropriate type:
assocℕ : ∀ (n m k : ℕ) → (n plus (m plus k)) ≡ ((n plus m) plus k)
Agda will check that it is well-typed by printing that the above is in need of definition, even the name for the term is declared. Hence it is well-typed and we need to provide our proof. However, the way we use before does not exactly work. We can try to do cases on n, m, and k, yet that will not do us much good without the inductive hypothesis. However, we do not get an inductive hypothesis by case analysis, so it will not work to just put a "?" after the definitional equality and ask Agda for an input. Instead, we work on our own here, in a backwards direction. We first find a function which can get us the needed proof provided the necessary constraints. In our case, it is indℕ. So, we write
assocℕ : ∀ (n m k : ℕ) → (n plus (m plus k)) ≡ ((n plus m) plus k)
assocℕ n m k = indℕ
However, we can still ask Agda for help, even here. We can put a question mark in place of every argument of indℕ for it to let us know which types they ought to occupy. Hence, we write
assocℕ : ∀ (n m k : ℕ) → (n plus (m plus k)) ≡ ((n plus m) plus k)
assocℕ n m k = indℕ ? ? ? ?
and after loading we get
assocℕ : ∀ (n m k : ℕ) → (n plus (m plus k)) ≡ ((n plus m) plus k)
assocℕ n m k = indℕ {! 0!} {! 1!} {! 2!} {! 3!}
with Agda's notes on which hole ought to be filled with a term of which type below. Hence, our finished proof will look like
assocℕ : ∀ (n m k : ℕ) → (n plus (m plus k)) ≡ ((n plus m) plus k)
assocℕ n m k = indℕ (λ x → (x plus (m plus k))≡((x plus m) plus k)) refl (λ n → λ p → ap succ p) n
which works because of the definitional equality of "succ x plus y" and "succ (x plus y)". Agda will accept any proof up to definitional equality without any problem. However, for propositional equalities be ready to use transport, defined as usual by
transport : ∀ {l1 l2} {A : Set l1} {B : A → Set l2} {x y : A} →
(x ≡ y) → B x → B y
transport refl x' = x'
One would want the question signs to work inside holes as well, yet that, sadly, is not the case. One can understand why: Agda would need to do a lot of mental gymnastics to comprehend whether the given term will produce the needed type. That would also necessitate straightly backwards reasoning. All in all, if you think you will get away with just case analysis or a straightforward declaration of values, ask Agda a question right away after the definitional equality. If not, ask it to help with any term you have deemed to do enough of a role. Yet, once again, we remind you to get outside the holes if you consider to input a function. So, even if you are filling in the holes of some term, is you want to fill it with another term whose arguments you have not determined beforehand (and hence want to ask Agda about them), delete the holes and input your terms - with the question marks - in their place.
Finally, let us talk about the K-axiom. The K-axiom is evil, just pure evil. Well, it is for people who want to do HoTT stuff. The axiom grants the uniqueness of identity proofs, i.e. uniqueness of paths, which goes against HoTT's main feature. Thankfully, we have a very straightforward way of removing it from consideration, writing the pragma
{-# OPTIONS --without-K #-}
right at the top of our document. Just don't forget to do it!
Finally, when you are done, you will probably want to use the definitions you used in one document in another one. In order to do this, start the document with
module X where
Where X is the name of your file without the .agda extension. This will make your document a library of its own, capable of being opened. That is, once a module X has been declared, we can import it by typing
open import X
in the document. Note that other imported modules, as well as parmas used in the imported document, will not be imported by that command, you will need to type the other imports separately to make everything work.
Finally, we wanted to once again recall that Agda does not have native HITs, for which you need to delve deeper into other people's advice of sidestepping the definitional challenges, and also recall that Agda does have support for cubical types, which one is also encouraged to look into on Agda's Git.
With this, you should be more than well-equipped to use Agda with good aptitude. For any specific notes and documentation, one is encouraged to consult the Programming Language Foundations in Agda, providing a very thorough overview of all the needed topics in the core of Agda.
In case you have any suggestions for the guide, please feel free to contact me via the provided email on my webpage.