# Squares and Diagonals

## ⇦ previous · index · next ⇨

(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`
2.7s
Agda

## 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`
0.7s
Agda

We can construct a path between two `reflEx a`s:

`reflReflEx : (a : A) → reflEx a ≡ reflEx a`
`reflReflEx a = λ j i → a`
0.7s
Agda

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 !}`
0.6s
Agda

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)`
Agda

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`
0.7s
Agda

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`
0.7s
Agda

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`
0.7s
Agda

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`
0.8s
Agda

(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)`
2.8s
Agda

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`
0.7s
Agda

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`
0.7s
Agda

The easiest square is the constant path for `p`:

` easiest : p ≡ p`
` easiest = reflEx _`
0.6s
Agda

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!