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  _⊝_
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 the a-side of 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!