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 a`

s:

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`

:

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) 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). 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)!`minSq`

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!