Squares and Diagonals

⇦ previous · index · next ⇨

Tesla (Yinsen) Ice Zhang, [CC BY-NC-ND 4.0]

(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 Squares&Diagonals 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:

We can redraw the above picture in a flattened way:

this look exactly like a square!

Squares

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:

• Whether p i0 i0 is convertible to reflEx a i0 (here reflEx a is the left hand side of the type reflEx a ≡ reflEx a)

• Whether p i1 i0 is convertible to reflEx a i0 (here reflEx a is the right hand side of the type reflEx a ≡ reflEx a)

• Whether p i0 i1 is convertible to reflEx a i1 (here reflEx a is the left hand side of the type reflEx a ≡ reflEx a)

• Whether p i1 i1 is convertible to reflEx a i1 (here reflEx a is the right hand side of the type reflEx a ≡ reflEx a)

• Whether p i0 j is convertible to reflEx a j (here reflEx a is the left hand side of the type reflEx a ≡ reflEx a)

• Whether p i1 j is convertible to reflEx a j (here reflEx a is the right hand side of the type reflEx a ≡ reflEx a)

If we want a path between two unknown path, things will become a little more complicated:

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, 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: and we can finally have the square:

module UseOfSquares

  (a b c d : A)

  (p : a ≡ b)

  (q : a ≡ b)

  (s : p ≡ q)

  where

and the picture of it:

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:

Diagonal

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:

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)

  where

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:

we have two endpoints unknown yet.

It is easy to think of ways to make squares such that:

• a on top left, b on bottom right (simply a path to a constant path)

• b on top left, a on bottom right(simply a constant path)

However, we can also let them both a, and both b! The key is to use the ∧ (min) and ∨ (max) operators.

When they're both a, the square expression will be λ i j → p (i ∧ j) (this square is referred hereafter as minSq). Unfortunately we can't have the type of this square right now, but we can draw pictures for it (and we will use this structure in the next chapter)!

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:

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:

Exercise

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

License

This and the original version of this blog are licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.