Cold Introduction (1) -- Squares and Diagonals


This blog is now co-hosted on nextjournal, and you can modify & run the code online in this link. (notice: this chapter is intended to be short) Recall from the previous post, we have max, min, neg and we can construct paths of symmetry.

{-# OPTIONS --cubical --allow-unsolved-metas #-}
module 2019-8-20-Cutt1 where
open import Cubical.Core.Everything
variable A : Set

Paths’ paths

Now let’s do something interesting with paths. We start with a constant path:

reflEx : (a : A)  a  a
reflEx a = λ i  a

We can construct a path between two reflEx as:

reflReflEx : (a : A)  reflEx a  reflEx a
reflReflEx a = λ j i  a

We can intuitively graph reflReflEx a as a path, whose points are paths as well:

λi. a λi. a λi. a λj i. a

We can redraw the above picture in a flattened way:

λj i. a λi. a λi. a

this look exactly like a square!


To understand squares more thoroughly, we need to study what we’ve just did deeper. Paths are lambda expressions taking an interval as parameter. Squares, on the other hand, are just lambda expressions taking two intervals as parameters. Our square reflReflEx a = λ j i → a type-checks, is because the square is literally a constant square. The type-checker can apply arbitrary interval parameters to reflReflEx a, and all of them returns a, which is what we have written in the expected type. We can list some checks the compiler can do, assuming p = reflReflEx a:

pathPath : (a : A)  (p q : a  a)  p  q
pathPath a p q = λ j i  {!a!}

Here we can’t fill the goal with a, because even it is clear that both p i0 and p i1 are convertible to a (and a is what we want to return in our path lambda), we can’t say for all i : I, p i is convertible to a – we don’t know what is between the two known endpoints of p and q. We can’t easily return a for all interval parameters as it does not respect the internals of p and q. In this case we can also say p ≡ q is not a constant square. We can do λ j i → a for constant squares is because the internals of reflEx a is known to be λ i → a.

Properties of squares

Let’s first assume a square, whose four endpoints are a b c d : A:

module UseOfSquares
  (a b c d : A)

then we need two paths p and q, one from a to b and another from c to d:

  (p : a ≡ b)
  (q : c ≡ d)

in this case, if we want a path from p to q, we can’t easily write something : p ≡ q, as the definition of requires the two endpoints to have the same type, while p and q are of different types. Therefore this square is in other words a Heterogeneous Equality. Fortunately, the design of path types is considerate of this case – there’s a type PathP, which first take a path between two types A and B (so you’re like proving A is equal to B), and then take instances of A and B one each. So, to bypass this typing issue, we make p and q two different paths between a and b:

  (p : a  b)
  (q : a  b)

and we can finally have the square:

  (s : p  q)

and the picture of it:

s : p≡q q:a≡b p:a≡b b b a a

Now let’s have some fun. First, the left and right edges of the square are just endpoints of the square, as squares are essentially paths’ paths:

 left : a  b
 left = s i0
 right : a  b
 right = s i1

But how about the top and bottom? Well, this time I want to spoil you haha:

 top : a  a
 top = λ i  s i i0
 bottom : b  b
 bottom = λ i  s i i1

because uncurrying left and right makes top and bottom crystal clear:

 left′ : a  b
 left′ = λ i  s i0 i
 right′ : a  b
 right′ = λ i  s i1 i

(please imagine the four functions above graphically, you should be able to imagine simple pictures like this) we can also rotate s 180 degrees, aka flip it vertically and horizontally (sym is symmetry – you can lookup its definition by clicking it):

 open import Cubical.Foundations.Prelude
 rotate : (sym q)  (sym p)
 rotate = λ i j  s (~ i) (~ j)

its picture is like:

λ i j. s (~ i) (~ j) sym q:b≡a sym p:b≡a b b a a


We can also find the diagonals of s. Consider the one from bottom left to top right, the diagonal is gonna be a path, whose i0 endpoint is the left bottom of s and i1 endpoint is the right top of s:

 diagonal : a  b
 diagonal = λ i  s i i

its picture:

s : p≡q b b a a λ i. s i i

I assume this is easy enough to understand.

Construction of squares

After using existing squares for a while, let’s make some squares! This time we still assume p : a ≡ b:

module ConstructionOfSquares
  (a b : A)
  (p : a  b)

The easiest square is the constant path for p:

 easiest : p  p
 easiest = reflEx _

But of course we can do more. We can see our p as the diagonal of an unknown square:

s : ??? b a ? p : a≡b ?

we have two endpoints unknown yet. It is easy to think of ways to make squares such that:

s : ??? b a a p : a≡b a x y

I picked two points x and y inside the square to explain why this picture represents p (i ∧ j). Every point inside the square can be seen as the value of the square applied with two intervals, one for the horizontal axis and one for the vertical one. For instance, we can think of minSq i j as the point (you know which one) in the following picture:

minSq : ??? minSq i j i j

From this perspective, as x is above the diagonal, we can say that for the coordinates of x, the vertical axis is larger than the horizontal one. y is below the diagonal, thus it’s the inverse case. If we say x is minSq i j (which evaluates to p (i ∧ j)), and as we already know that j > i, we can simplify i ∧ j to i, thus x becomes p i. For y it becomes p j. Then, for the top left corner, it’s just minSq i0 i1 which reduces to p (i0 ∧ i1) which reduces to p i0, and then reduces to a. The bottom right corner is minSq i1 i0 which also reduces to a. We can graph this mapping like this:

a b a a


Explain λ i j → p (i ∨ j) as I did and draw the picture of it. I believe you can do this in your mind!

Tweet this Top


This work (Cold Introduction (1) -- Squares and Diagonals) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.