Cold Introduction (3) -- Open Squares can be Capped

by

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!):

a⊝b ssa⊝ssb sa⊝sb j (from cancel) i sa⊝sb cancel sa sb i cancel a b i

(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:

a d c i j b r j q j p i

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:

ax w i k b d y zj c

(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:

a⊝ba⊝b i k sa⊝sb j sa⊝sbsa⊝sb sa⊝sbssa⊝ssb sa⊝sb

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:

 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:

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:

a c a i j b q j p i

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!


Tweet this Top

License

This work (Cold Introduction (3) -- Open Squares can be Capped) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

License