First commit

.gitignore

@@ -0,0 +1 @@
+*.agdai

Basic.agda

@@ -0,0 +1,14 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive
+
+module Basic where
+
+data False : Set where
+
+record True : Set where
+
+data _||_ {a b : _} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+  inl : A → A || B
+  inr : B → A || B
+infix 1 _||_

File1.agda

@@ -0,0 +1,204 @@
+{-# OPTIONS --safe --warning=error --cubical --without-K #-}
+
+open import Agda.Primitive
+open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Naturals
+open import Basic
+
+module File1 where
+
+{-
+Let's define the integers.
+
+If you want to learn how to type something, remember the Emacs action is M-x describe-char with the cursor on a character.
+-}
+data ℤ : Set where
+  pos : ℕ → ℤ
+  neg : ℕ → ℤ
+  congZero : pos 0 ≡ neg 0
+
+{-
+A bit odd! We defined an integer to be "a natural tagged as positive", "a natural tagged as negative", or "a witness that pos 0 = neg 0".
+This is obvious nonsense (how can two things be equal if they were made from different constructors?! what even does it mean for "pos 0 ≡ neg 0" to be an integer?!) until you let go of your preconceptions about what it means for two things to be equal.
+-}
+
+-- Just to help you realise how odd this is, we'll use some new Cubical definitions to manifest a really weird element of ℤ which is neither a `pos` nor a `neg`. Don't worry too much about this for now.
+oddThing : ℤ
+oddThing = congZero i1
+
+-- Even odder, the integer we just made is equal to 0. Think how strange this is: it's not built using the only constructor that could build `pos 0`, but it's still equal to `pos 0`.
+oddThing2 : pos 0 ≡ oddThing
+oddThing2 = congZero
+
+{-
+Add 1 to an integer. The first cases are easy, but the last case is very odd and we will discuss it in detail.
+-}
+incr : ℤ → ℤ
+incr (pos x) = pos (succ x)
+incr (neg zero) = pos 1
+incr (neg (succ x)) = neg x
+
+-- First of all, we have in scope an "integer" `congZero` which is of type `pos 0 ≡ neg 0` - huh?!
+incr (congZero i) = pos 1 -- TODO: hole this
+{-
+This one looks different from the non-cubical world.
+
+Goal: ℤ
+———— Boundary ——————————————————————————————————————————————
+i = i0 ⊢ pos 1
+i = i1 ⊢ pos 1
+————————————————————————————————————————————————————————————
+i : I
+———— Constraints ———————————————————————————————————————————
+pos 1 = ?0 (i = i1) : ℤ
+pos 1 = ?0 (i = i0) : ℤ
+
+The constraints look pretty normal, telling you that goal 0 needs to be equal to `pos 1`.
+But there's stuff about this `i : I` here. What's that?
+
+Recall that Cubical alters the definition of ≡. Given any element of X, an element of X ≡ Y contains content for how that element corresponds to a Y, and vice versa.
+Homotopy type theory, and Cubical Agda, prefer to think of a more general structure on top of that data, though: not only can we go from an X to a Y, but we also store *how* we get there.
+More abstractly, we store how to traverse a path from X to Y. The `i` here is telling us where along that path we are; the template goes from the special symbol `i0` to the special symbol `i1`, and `i` is notionally somewhere between those two points.
+
+This gives some nice composability properties: if we know that X ≡ Y and that Y ≡ Z, we can compose the two paths to get a path X ≡ Z.
+Cubical Agda's great innovation is that all this has computational content: proofs about X can be transported along the path to obtain for free proofs about Z.
+
+Having told Agda that `incr (pos x) = pos (succ x)`, it can infer that `incr (pos 0) = pos 1`.
+So our goal of constructing a path `incr congZero : incr (pos 0) ≡ incr (neg 0)` is in fact the requirement to construct a path `pos 1 ≡ incr (neg 0)`.
+Similarly, we told it that `incr (neg 0) = pos 1`, so our path `incr congZero` is actually of type `pos 1 ≡ pos 1`
+The `I` from the goal is the template of the path `congZero n` which we are trying to construct from `pos 1` to `pos 1`.
+The `i0` and `i1` are the templates for the start and end points of the path, i.e. they both indicate `pos 1`.
+
+What we really wanted to write here was `incr congZero`. For reasons I don't understand, Agda doesn't accept this.
+We are forced to descend to the level of actually implementing the path from `pos 1` to `pos 1` by telling Agda where each `i` goes, even though there's an obvious way (`refl`) to specify the entire path at once.
+
+Agda can automatically infer the correct hole-fill, but you can try it with `pos 1`.
+-}
+
+{-
+Let's show that successors of naturals are nonzero.
+We do this using a new technique that only makes sense in Cubical-land.
+
+Given a path from `succ a` to `0`, we need to show False.
+The assumed member of `succ a ≡ 0` is a path that tells us how to get from `succ a` to `0` in a way that is preserved by function application.
+That is, it tells us how to show `f (succ a) ≡ f 0` for any `f`. (The function `subst` captures this ability to move functions from one end of a path to the other.)
+So if we pick `f` appropriately so that it outputs `False` at 0 but something else (anything else, as long as we can construct it!) at `succ a`, we will be done.
+-}
+succNonzero : {a : ℕ} → succ a ≡ 0 → False
+succNonzero {a} sa=0 = subst f sa=0 record {} -- TODO: hole the record
+  where
+    f : ℕ → Set
+    f zero = False
+    f (succ i) = True -- TODO: hole True
+
+{-
+Let's show that these equality things aren't *too* weird. We'll show that even though `pos 0` is equal to `congZero i1`, it's actually the *only* other `pos` which is equal to `congZero i1`. (You'd hope this would be the case; otherwise we'd have several `pos` being equal to each other.)
+
+Cubical Agda gives us a magical way to do this. Recall that we can move functions along paths (the `subst` from above, which lets us take an `x ≡ y` and an `f` to get `f x → f y`); we can actually also do the same thing viewed as transforming the *entire path* `x ≡ y` using `f` into `f x ≡ f y`.
+This is the function `cong`.
+
+If we can somehow create a function that "strips off `pos`", then that function can transform the path `pos a ≡ pos b` into a path `a ≡ b`.
+-}
+toNat : ℤ → ℕ
+toNat (pos x) = x
+toNat (neg x) = 0 -- this one doesn't matter as long as neg 0 goes to the same place as pos 0
+toNat (congZero i) = 0 -- this was forced to be 0 by the definition of `toNat (pos 0)`
+
+posInjective : {a b : ℕ} → pos a ≡ pos b → a ≡ b
+posInjective pr = cong toNat pr
+
+{-
+Finally, we can use the injectivity of `pos` in the obvious way to prove that only `pos 0` is `congZero i1`.
+-}
+notTooOdd : (n : ℕ) → (pos n ≡ congZero i1) → n ≡ 0
+notTooOdd zero pr = refl
+notTooOdd (succ n) pr = posInjective (pr ∙ sym congZero)
+
+{-
+Let's show that `pos` is injective in a different way, inspired by how you might do this kind of thing in a non-Cubical world. We'll go by induction, which means the interesting case will be `pos (succ a) ≡ pos (succ b) → pos a ≡ pos b`.
+
+This is a classic example of moving a path wholesale along a function; in this case, the function is "decrement".
+-}
+decr : ℤ → ℤ -- TODO hole this
+decr (pos zero) = neg 1
+decr (pos (succ x)) = pos x
+decr (neg x) = neg (succ x)
+decr (congZero i) = neg 1
+
+posDecr : {a b : ℕ} → pos (succ a) ≡ pos (succ b) → pos a ≡ pos b
+posDecr {a} {b} pr = cong decr pr
+
+posInjective' : {a b : ℕ} → pos a ≡ pos b → a ≡ b
+-- The two easy cases first
+posInjective' {zero} {zero} x = refl
+posInjective' {succ a} {succ b} x = cong succ (posInjective (posDecr x))
+{-
+We need to transform `pos zero ≡ pos (succ b)` into `zero ≡ succ b`.
+We could do this using the proof of `posInjective` - moving the path along `toNat` - but it is also interesting to construct the path `zero ≡ succ b` manually using `subst`.
+
+To use `subst`, we need to construct a function from ℤ which is "a type we can populate" at `pos zero` (i.e. at one end of the path), and `zero ≡ succ b` at `pos (succ b)` (i.e. at the other end of the path); then we will be able to move from the populated type to `zero ≡ succ b` using that function.
+-}
+posInjective' {zero} {succ b} x = subst t x record {}
+  where
+    t : ℤ → Set
+    t (pos zero) = True
+    t (pos (succ x)) = zero ≡ succ b
+    t (neg x) = True
+    t (congZero i) = True
+posInjective' {succ a} {zero} x = subst t x record {} -- TODO hole all this
+  where
+    t : ℤ → Set
+    t (pos zero) = succ a ≡ zero
+    t (pos (succ x)) = True
+    t (neg x) = succ a ≡ zero
+    t (congZero i) = succ a ≡ zero
+
+{-
+Is it true that `congZero i` is either `pos k` or `neg k` for some k?
+We've shown it for one endpoint, `i1` - but then we actually already knew that, because `congZero` takes `pos 0` to `neg 0`, so its endpoints are already known to be `pos` or `neg`.
+t : (a : ℤ) → Σ[ n ∈ ℕ ] (a ≡ pos n) || Σ[ n ∈ ℕ ] (a ≡ neg n)
+t (pos x) = inl (x , refl)
+t (neg x) = inr (x , refl)
+t (congZero i) = {!!}
+-}
+
+{-
+What does equality mean on the level of types, rather than values?
+Univalence, the axiom which Cubical provides computational meaning to, basically says "identity really means isomorphism".
+I will gloss over a lot of detail there, but here is a witness to `ℤ ≡ ℤ` that is not `refl`!
+-}
+incrDecrInverse1 : (a : ℤ) → incr (decr a) ≡ a
+incrDecrInverse1 (pos zero) = sym congZero
+incrDecrInverse1 (pos (succ x)) = refl
+incrDecrInverse1 (neg x) = refl
+{-
+The remaining case is worth talking about.
+We need a path from incr (decr (congZero j)) to congZero j.
+That is, we need a path from incr (neg 1) to congZero j; i.e. from neg 0 to congZero j.
+We already have a path from neg 0 to pos 0 - namely `sym congZero`.
+But `sym congZero` goes from `neg 0` to every point along `sym congZero` - and `congZero j` is also a point along `sym congZero`, because `sym` just means "reverse the path"!
+So we can get the path we need by truncating `sym congZero`, using the `∧` ("min") operation (a special builtin primitive in Cubical).
+The path, parameterised by `i` with `j` fixed, is "go backwards (`sym`) along `congZero` to the min of `i` and where `j` lies on this path (`~ j`), but then don't go any further".
+Here, `~` means essentially "negate"; if you got to position `i` travelling forward on path `p`, then you got to position `~ i` travelling backward on path `sym p`.
+
+This is probably best done if you draw a little picture.
+-}
+incrDecrInverse1 (congZero j) i = sym congZero (i ∧ (~ j))
+
+incrDecrInverse2 : (a : ℤ) → decr (incr a) ≡ a
+incrDecrInverse2 (pos x) = refl
+incrDecrInverse2 (neg zero) = congZero
+incrDecrInverse2 (neg (succ x)) = refl
+{-
+Similarly, here we need a path from pos 0 to congZero j; we can do that by following congZero up until the minimum of i and j, so that the path starts out by extending along `congZero` but then stops extending when it hits `j`.
+-}
+incrDecrInverse2 (congZero j) i = congZero (i ∧ j)
+
+incrIso : ℤ ≡ ℤ
+incrIso = isoToPath (iso incr decr incrDecrInverse1 incrDecrInverse2)
+
+{-
+Unexpected! Cubical has let us prove that ℤ ≡ ℤ in a very nonstandard way. What use is this? Who knows.
+-}

Naturals.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+module Naturals where
+
+data ℕ : Set where
+  zero : ℕ
+  succ : ℕ → ℕ
+
+{-# BUILTIN NATURAL ℕ #-}
+
+_+N_ : ℕ → ℕ → ℕ
+zero +N b = b
+succ a +N b = succ (a +N b)

README.md

@@ -0,0 +1,20 @@
+# Cubical Agda Tutorial
+
+This was written while I was getting up to speed with Cubical Agda.
+
+# Quick start
+
+## Installing Agda
+
+If you already have Agda installed, great.
+If not, follow the official instructions.
+I use `brew install agda`.
+
+## Installing cubical
+There are install instructions at https://agda.readthedocs.io/en/v2.6.1/language/cubical.html .
+Only the paragraph "For detailed install instructions..." is necessary; it amounts to cloning the Cubical repo, building it, and adding it to ~/.agda/libraries and ~/.agda/defaults.
+
+## Which file to start with
+
+The first file is `File1.agda`.
+Open it up in emacs (or your normal Agda editing environment) and follow it.