This blog is now co-hosted on nextjournal, and you can modify & run the code online in this link.

Motivation

I’m planning to write a series of introduction to the Cubical Type Theory, using the Agda proof assistant. My motivation was that existing Cubical Type Theory (and Cubical Agda) tutorials are all impossible to read unless you know Homotopy Type Theory. However, I still believe it’s possible to learn Cubical Type Theory without HoTT background – the only thing we need is someone who knows Cubical to write an introduction. I have participated the summer school of [HoTT 2019], and have solved most of my confusions in the Cubical methods lectures by Anders Mortberg. I feel like it’s time for me to be the Cubical person, to write a really readable introduction to the Cubical Type Theory. As this introduction is “not HoTT”, it should be “cold”. Thus “cold introduction”. [HoTT 2019]: https://hott.github.io/HoTT-2019/summer-school/

Prerequisite

• Non-cubical Agda (Vanilla Agda) experience
• Lambda calculus basic concepts, such as currying
• Primary school geometry (lines, squares, cubes)

{-# OPTIONS --cubical --omega-in-omega #-}
module 2019-8-1-Cutt0 where
open import Cubical.Core.Everything

Let’s jam

We start with a question: how should we represent proofs in a programming language? In Martin-Lof Type Theory which Agda is (kind of) based on, the equality relation is represented using a type named _≡_. It’s parameterized and indexed by elements of a type, with only one inhabitant refl defined as the proof of reflexivity. The Cubical Type Theory introduces another equality type that fits HoTT better (instead of MLTT), but as this introduction is cold, I won’t be able to explain “Why Cubical” here.

Intervals

There is a type, called “interval” in papers, and I in Agda. Look at it – you can jump to its definition by clicking the I below.

--         ↓
interval = I
--         ↑

The I type is best explained as the type of a point on a path. Imagine i : I, we can draw a picture to show i:

We have a (geometrically speaking) path from 0 to 1, and every point on this path is an instance of I. And of course, 0 and 1 are also valid instances of I. Intervals have the following properties:

• It’s possible to quantify over an interval – say, ∀ (i : I), blabla.
• They are always larger than or equal to 0, less than or equal to 1. We write i0 for 0, and i1 for 1 in Agda:

_ : I
_ = i0
_ : I
_ = i1

There isn’t much primitive operations on intervals – at least it’s impossible to have predicates on them (we can have predicates on intervals in some other structures though), like λ i → if i == 0 then bla else rua is impossible. We do have several other operations:

• min, which takes two intervals and return the one closer to 0
• max, which returns the one closer to 1
• neg, which returns the point of symmetry They are named with some scary mathematical notations in Agda:

min : I → I → I
min = _∧_
max : I → I → I
max = _∨_
neg : I → I
neg = ~_

They follow the De Morgan’s theorem, say ~ (i ∧ j) will be equivalent to ~ i ∨ ~ j, etc. Endpoints behaves as-is, like i ∧ 0 will be equal to 0, i ∨ 0 will be equal to i, etc. However, interval is not Boolean, as they are points on a path – there’s infinite number of points on a path, but for Boolean there are only two. We can construct something interesting:

andNot : I → I → I
andNot i j = ~ (i ∧ j)

which is equivalent to:

andNot' : I → I → I
andNot' i j = ~ i ∨ ~ j

Now we’ve got some intuitions on intervals. Good!

Path type

The reason why we have this strange I type is because we need to introduce the Path type. Every (geometrically speaking) path is defined with two values – its two endpoints. Imagine a type A and two inhabitants a and b of which,

myImagination
  : (A : Set)
  → (a b : A)

we can have a Path type for type A between a and b (I’m currying the parameters):

  → Set
myImagination = Path

The type of paths between a and b is written as Path A a b where A is the type of a and b. Inhabitants of Paths are lambda expressions taking intervals as parameters. We call them Path lambdas. We can also have normal functions that takes an interval as argument, but Path lambdas are special constructions regarding ordinary lambdas.

Reflexivity

For instance, we can have a constant path lambda:

-- I wish your device displays this nicely
constantPathLam : (A : Set) → (a : A) → Path A a a
constantPathLam    A           a        i = a
--                 ↑           ↑        ↑
--             the type        |    the interval
--                    two endpoints are both `a`

When Agda checks your path lambda p against the type Path A a b (say, the typing judgement Gamma |- p : Path A a b), it checks whether the return value of p i0 (as p is a lambda taking an interval as parameter, we can apply an argument to it!) is definitionally equal to a, and whether p i1 is definitionally equal to b. Thus λ i → a is a valid instance of Path A a a, as (λ i → a) i0 is essentially just a (and so does (λ i → a) i1). We can draw the picture for the constantPathLam path as:

We write a ≡ b as shorthand form of Path _ a b, because Path type is the Cubical version of the equality type. Rewriting the above definition using ≡ will be:

constantPathLam′ : (A : Set) → (a : A) → a ≡ a
constantPathLam′ A a i = a

This constantPathLam′, is the proof of reflexivity in the Cubical Type Theory. We already have this in the Cubical Agda library:

import Cubical.Foundations.Prelude as Prelude
_ : {A : Set} {a : A} → a ≡ a
_ = Prelude.refl

We can think of paths as an infinite-sized read-only array of values, its indices are intervals, and it’s defined by the array element getter.

Symmetry

As we can find the point of symmetry for intervals, we can invert a path (parameters are aligned in the code so they are more consistent with the type signature):

invert : (A : Set) (a b : A) (p : a ≡ b) → b ≡ a
invert    A         a b       p = λ i → p (~ i)

To explain this function, imagine a path p of type a ≡ b,

We construct a new path lambda, mapping every interval of which to “the interval of symmetry on p”, so its type becomes the “path of symmetry of a ≡ b”, in other words, b ≡ a. Here’s a graphical example – and one mapping from i to ~ i is explicitly drawn (but you should imagine that for all interval on the above path, like i, we map it to the corresponding point on the below path, like ~ i):

(for pictures, arrows starting from an interval i on the path p to something a means “the value (or point, in other words) corresponds to i is a” or “p i evaluates to a”) What we’ve just done? We created a new path lambda, returned some compound expression consisting of a given path and the interval it takes. Using similar techniques and a little functional programming, we can do two more magics.

Congruence

First of all, we can prove congruence in MLTT. We create a function,

congruence
  : {A B : Set}

that takes a function from A to B,

  → (f : A → B)

and a path between two inhabitants of A,

  → {x y : A}
  → (p : x ≡ y)

and return a proof of f x ≡ f y.

  → f x ≡ f y

How do we prove this? Well, by creating a path and do some magic with the interval it takes and some other variables provided, as we did just now:

congruence f p = λ i → f (p i)

What did this code do? It:

1. Created a path lambda, so we have an interval i
2. Applied the i to p, so we have a value of type A on the path p which is between a and b
3. Applied the value extracted from p to the function f, which takes an instance of A and returns an instance of B Thats it! We can visualize this process. First we send the interval to p:

Then we apply the value to f and get back:

Now we’re all good!

Function Extensionality

Function extensionality is the proposition that if two functions are point-wise equivalent, the functions are equivalent. We can’t prove this constructively before, but it’s now possible under Cubical. We can express function extensionality as a function,

functionExtensionality
  : {A B : Set}

taking two function from A to B,

  → {f g : A → B}

and a proof p of their point-wise equality,

  → (p : ∀ a → f a ≡ g a)

and returns a proof that these two functions are equivalent:

  → f ≡ g

We can prove this by constructing a path that returns a function, where the function is implemented using p:

functionExtensionality p i = λ a → p a i

This time we:

1. Created a path lambda, so there’s an interval i
2. Returned another lambda, taking a parameter a which is of type A, just like f and g did
3. Applied a to p, so we get a path of type f a ≡ g a (notice that f a and g a are of type B
4. Applied i to that path, so we get an instance of B To demonstrate this proof in picture, let’s first graph p, the point-wise proof, which is a function that returns a path:

(for pictures, arrows not starting from an interval on a path are functions) With p, which is a function from a to a path, We can specialize it to a function from a to any speicific point on the path it originally returns, if we have the interval representing the point. Thus we create a new path, mapping each interval i to the function obtained by specializing p with i. Here’s a graphical demonstration:

Conclusion (for now)

Now we’re fairly familiar with simple paths (I hope so). For exercise, define “higher order” paths, whose endpoints are paths as well. This means our path lambdas will return path lambdas, like λ i j → a, where a contains free variable i and j. Think of some paths like that, and I’ll talk about them in the next post.