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
andr
:
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 ofnewPath
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 isp i
- The
a ≡ c
path isq j
- The
p i
path reduces toa
wheni = i0
, we calli = i0
thea
-side ofp i
- The
q j
path starts from (or “connected to”, in other words) thea
side of thep i
path - We use the syntax
(i = i0) -> q j
for this Similarly we have(i = i1) -> r j
, and that’s all ofnewPath
. Fun fact: you canhcomp
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!