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

Recall the previous post,
we have higher inductive types, their operations and properties
and a glance to the `isoToPath`

function.

{-# OPTIONS --cubical --allow-unsolved-metas #-} module 2019-10-14-Cutt3 where open import Cubical.Core.Everything open import Cubical.Foundations.Prelude open import Agda.Builtin.Nat variable A : Set

At the end of the blog I have left another HIT integer definition,
that is the set of natural numbers’ substraction equipped with a
path such that `a - b`

equals `suc a - suc b`

:

infixl 5 _⊝_ data DeltaInt : Set where _⊝_ : Nat -> Nat -> DeltaInt cancel : ∀ a b -> a ⊝ b ≡ suc a ⊝ suc b

One question come along with this HIT:
*how do we prove the following proposition?*

question = ∀ a b i → cancel a b i ≡ cancel (suc a) (suc b) i

We can picture it (we call this square the **“question square”**.
We’ll use this term soon, memorize it!):

(note that we’re using `ssa`

for `suc (suc a)`

,
`sa`

for `suc a`

(and also same shorthands for `b`

)
to save the space on the picture)

The question square involves three different endpoint values,
therefore not constructable with the three operations we knew (`∧`

, `∨`

and `~`

),
as those three operators basically “expand” one path to a square,
while our new square is composing several paths.

Well, to do this we need another operation – `hcomp`

,
which is short for “homogeneous composition”.

# Homogeneous Composition

In the cubical type theory tutorials I have read before,
the `hcomp`

operator is described with scary terms like “Kan operation”,
“Kan-filling operation”, etc.
They also try to describe the operation as:

composition of a open square

or:

obtain the cap of a open square

or something similar.
I actually read these sentences,
but I never really understand what parameters I should pass to `hcomp`

.
The only semi-readable tutorial I’ve found is Anders’ tutorial based on cubicaltt,
a minimal dependently-typed language that implements the cubical type theory.
But cubicaltt is cubicaltt, it’s not Agda.

Here’s my version of introduction, I wish they make sense to you.

## Squares

First, imagine three paths `p`

, `q`

and `r`

:

module SquareHcomp (a b c d : A) (p : a ≡ b) (q : a ≡ c) (r : b ≡ d) where

Using the operation `hcomp`

we can obtain a path `c ≡ d`

from the given three paths
(the reason why `hcomp`

is designed this way is beyond the topic of this blog).

Here’s a concrete example of `hcomp`

,
I’ll write the code and draw the picture (so you can take a glance),
and tell you how to read them (but **don’t** dive into the syntax right now).
We start from the picture,
understand the intuition and then get back to the Agda concrete syntax.

Code:

newPath : c ≡ d newPath i = hcomp (λ j -> λ { (i = i0) -> q j ; (i = i1) -> r j }) (p i)

Explanation of the syntax
(read at your own risk – the rest of this blog do not depend on this paragraph):
We’re writing a function that pattern matches the `i`

parameter out,
returning an expression which is a call to `hcomp`

with two arguments,
the first one is a lambda taking a parameter `j`

and then returns another
lambda which is a special lambda that looks like a pattern matching lambda
but different (we’ll call it “system”),
the second one is `p i`

.

Don’t look at the type signature of `hcomp`

(I know you’re curious,
but just don’t click it) – it’s not helpful yet.

Picture:

The dash line in the above graph is our `newPath`

, whose internal is constructed via `hcomp`

.
Note that I have annotated the corresponding path of `q j`

, `r j`

and `p i`

for you.

Now, forget about the syntax we have seen just now – let’s look at the picture.
The `hcomp`

operation takes three paths and give you one path back.
We call the incomplete square formed by the three given paths an *open shape*,
and in case it’s two dimensional, we also call it an *open square*.
Note that the three paths are connected (by *connected* I mean sharing one endpoint in common),
this is the reason why the can form an open shape.
**What hcomp does is that it gives you the cap that the open shape is missing**,
and in case it’s a square, it gives you the top path that the open square is missing.

This sounds very easy, but it’s easy only because we’re dealing with squares. How’bout adding one more dimension?

Well, `hcomp`

actually works for any numbers of dimensions.
Remember that what `hcomp`

does is that it gives you the cap that the open shape is missing,
so in case it’s an open **cube** (with five given squares),
it can give you the top **square** that is missing!!
Therefore, if we want a square of some specific four endpoints,
we can find an open cube whose missing cap has that four endpoints,
and use `hcomp`

to get the square we wanted!

Recall the question square – its four endpoints of it are known to us, so we can imagine it as the cap square of a cube. The cube have 8 endpoints and 6 squares in total, where:

- The four endpoints at the top should form the question square
- The other four at the bottom are free for us to pick
- The top square is the square we want, say, the output of
`hcomp`

- The other five squares are input to
`hcomp`

**We want to pick the specific four bottom endpoints to make the five input squares
simple enough to construct.**
By “simple enought” I mean “constructable via the known paths, the `∧`

, `∨`

and `~`

operators”.

So, let’s first picture a cube in general:

(Sorry for the ridiculous SVG – I’m doing my best.
Also, the `i`

, `j`

and `k`

directions matters –
remember that paths are directional)

The dashed square is the square we want `hcomp`

to give us.
In case of `question`

we assign `a ⊝ b`

, `suc a ⊝ suc b`

, `suc (suc a) ⊝ suc (suc b)`

and `suc a ⊝ suc b`

to `w`

, `x`

, `y`

and `z`

, respectively.
Here’s a table for the variable assignment, if you need:

Point | Term |
---|---|

`w` |
`a ⊝ b` |

`x` |
`suc a ⊝ suc b` |

`y` |
`suc (suc a) ⊝ suc (suc b)` |

`z` |
`suc a ⊝ suc b` |

You may draw the substituted picture yourself, I’m not doing all the intermediate steps for you.

There are many possible choices of values for `a`

, `b`

, `c`

and `d`

,
but here’s the combination I picked (for better exercise,
pick a different combination):

Point | Term |
---|---|

`a` |
`a ⊝ b` |

`b` |
`suc a ⊝ suc b` |

`c` |
`suc a ⊝ suc b` |

`d` |
`suc a ⊝ suc b` |

(note the `a`

and `b`

at the left hand side of the table are points,
while the `a`

and `b`

at the right hand side are `Int`

instances)

Now we have the cube complete, the rest of the steps are filling out the five squares. Let’s observe the features of the five squares of this nice cube (I strongly recommend you to draw the cube out):

Square | Feature |
---|---|

`abcd` |
max square |

`abxw` |
refl |

`bcyx` |
min square |

`adzw` |
refl |

`cdzy` |
min square |

Note:

- By “max square” I mean the max square formed by the
`cancel`

path, similarly the “min squares”.- If you’ve forgotten the definition of “max squares”, review the second blog in this cold introduction series.

- By “refl” I mean
`λ i -> some-path`

(or possibly`λ i j -> cancel i`

), say, a constant path whose endpoints are also paths, or a rotated version of which.

Wow, so it turns out that our open cube (with the top square missing) has all of its five squares simply constructible!

Here’s the final cube:

# Describing an open shape

Now it’s time to introduce the concrete syntax of `hcomp`

in Agda.

Normally, when we call `hcomp`

to create an n-dimensional path,
the function will be like (in case it’s a 2-dimensional path):

```
test i j = hcomp blabla
```

Say, there’s already two interval variables in the context.
However, the open shape we’re describing has one more dimension
(remember that when you want a path, `hcomp`

a square;
when you want a square, `hcomp`

a cube; etc.).
The extra interval variable is not present in the top-missing
shape that `hcomp`

gives us, but it should be accessible in the
side-shapes.
The bottom of the open shape is parallel to the top-missing shape,
which is indenpend to the extra dimension.

In conclusion, the arguments to `hcomp`

should have:

- The bottom
- A function, from an interval (standing for the extra dimension), to all of the sides of a shape

In case of a cube, there should be four sides returned by the function, each of which are squares; in case of a square, there should be two sides returned, each are paths.

We start from an explanation to the `newPath`

above,
towards a the question square
(you may want to lookup the svg of `newPath`

above – I don’t want to
copy-paste the same svg twice, it’s very big).

newPath2 : c ≡ d newPath2 i = hcomp -- ^ the original dimension (\ j -> -- ^ the extra dimension \ { (i = i0) -> q j -- ^^^ the `a ≡ c` path, goes from `j = i0` to `j = i1` -- ^^^^^^ the starting point of the `a ≡ c` path ; (i = i1) -> r j -- ^^^ the `b ≡ d` path, goes from `j = i0` to `j = i1` -- ^^^^^^ the starting point of the `b ≡ d` path }) (p i) -- ^^^ the bottom side, `a ≡ b`

We use the pattern matching syntax to describe the open shapes’ sides.
Taking the `q j`

one as an example:

- The
`a ≡ b`

path is`p i`

- The
`a ≡ c`

path is`q j`

- The
`p i`

path reduces to`a`

when`i = i0`

, we call`i = i0`

theof`a`

-side`p i`

- The
`q j`

path starts from (or “connected to”, in other words) the`a`

side of the`p i`

path - We use the syntax
`(i = i0) -> q j`

for this

Similarly we have `(i = i1) -> r j`

, and that’s all of `newPath`

.

Fun fact: you can `hcomp`

zero-dimensionly, which is the identity function:

id : ∀ {ℓ} {A : Set ℓ} -> A -> A id a = hcomp {φ = i0} (λ i ()) a

# Back to the `question`

As a preparation, we write up the min/max squares of `cancel`

:

maxSq : (a b : Nat) -> (i j : I) -> DeltaInt maxSq a b i j = cancel a b (i ∨ j) minSq : (a b : Nat) -> (i j : I) -> DeltaInt minSq a b i j = cancel a b (i ∧ j)

Then, we implement `question`

:

questionImpl : question questionImpl a b i j = hcomp (λ k -> λ -- the extra dimension { (i = i0) -> cancel a b j -- ^ when `i = i0`, it's the left square adzw ; (i = i1) -> minSq (suc a) (suc b) j k -- ^ when `i = i1`, it's the right square bcyx ; (j = i0) -> cancel a b i -- ^ when `j = i0`, it's the front square abxw ; (j = i1) -> minSq (suc a) (suc b) i k -- ^ when `j = i1`, it's the back square cdzy }) (maxSq a b i j) -- abcd square

We’re done! Yay!

# Transitivity

The `compPath`

function, say, the proof that paths are transitive,
is also proved using `hcomp`

.
The type signature of `transitivity`

is:

transitivity : {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c

We start from introducing the variables and go with a square `hcomp`

:

transitivity {a = a} p q i = hcomp

We make a square like this:

Translating the picture into Agda will be:

(λ j -> λ { (i = i0) -> a ; (i = i1) -> q j }) (p i)

We have transitivity now!

#### Footnote

Thanks to Anders Mörtberg for teaching me `hcomp`

at the
HoTT 2019 Summer School at CMU.

I have received emails from David Leduc and Donnacha Oisín Kidney, showing their appreciation to this “Cold introduction” series. These words help a lot, I’d like to thank you (for reading my shitposts haha) too!

Btw, I’m also looking for Dependent Type relevant research opportunities. If you’re interested in hiring me (you may want to see my resume), email me!

Also, if you’re looking for something to read about and you expect me to know, also email me!