hcomp is a primitive operation in cubical type theory that completes the lid of an incomplete cube, given the bottom face and some number of side faces.
NOTE
All the code samples in this document are written in and checked for correctness by Agda, a dependently typed programming language that implements cubical type theory. Many of the names and symbols in the names are clickable links that take you to where that symbol is defined. Below are all of the imports required for this page to work.
Imports for Agda
{-# OPTIONS --cubical #-} module 2024-09-18-hcomp.index where open import Cubical.Foundations.Prelude hiding (isProp→isSet) open import Cubical.Foundations.Equiv.Base open import Cubical.Foundations.Isomorphism open import Cubical.Core.Primitives open import Cubical.HITs.Susp.Base open import Cubical.HITs.S1.Base open import Data.Bool.Base hiding (_∧_; _∨_)
Two-dimensional case
In two dimensions, can be understood as the double-composition operation. Given three paths , and , it will return a path representing the composed path .
”Single” composition (between two paths rather than three) is typically implemented as a double composition with the left leg as . Without the double composition, this looks like:
path-comp : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z path-comp {x = x} p q i = let u = λ j → λ where (i = i0) → x (i = i1) → q j in hcomp u (p i)
The (i = i0)
case in this case is which is definitionally equal to .
Example:
Suppose we want to prove that all mere propositions (h-level 1) are sets (h-level 2). This result exists in the cubical library, but let’s go over it here.
isProp→isSet : {A : Type} → isProp A → isSet A isProp→isSet {A} f = goal where goal : (x y : A) → (p q : x ≡ y) → p ≡ q goal x y p q j i = -- ...
We’re given a type , some proof that it’s a mere proposition, let’s call it .
Now let’s construct an hcomp. In a set, we’d want paths and between the same points and to be identified. Suppose and operate over the same dimension, . If we want to find a path between and , we’ll want another dimension. Let’s call this . So essentially, the final goal is a square with these boundaries:
Our goal is to fill this square in. Well, what is a square but a missing face in a 3-dimensional cube? Let’s draw out what this cube looks like, and then have give us the top face. Before getting started, let’s familiarize ourselves with the dimensions we’re working with:
- is the left-right dimension, the one that and work over
- is the dimension of our final path between . Note that this is the first argument, because our top-level ask was .
- Let’s introduce a dimension for doing our
We can map both and down to a square that has on all corners and on all sides.
Let’s start with the left and right faces. The left is represented by the face lattice . This is a sub-polyhedra of the main cube since it only represents one face. The only description of this face is that it contains all the points such that the dimension is equal to . Similarly, the right face can be represented by .
To fill this face, we must find some value in that satisfies all the boundary conditions. Fortunately, we’re given something that can produce values in : the proof that we are given!
tells us that and are the same, so and . This means we can define the left face as and the right face as . (Remember, is the direction going from bottom to top)
We can write this down as a mapping:
The same logic applies to the front face and back face . We can use to generate us some faces, except using and , or and as the two endpoints.
Writing this down as code, we get:
This time, the dimension has the edges.
Since all the edges on the bottom face as , we can just use the constant as the bottom face.
In cubical, this is the constant expression x
.
Putting this all together, we can using to complete the top face for us:
let u = λ k → λ where (i = i0) → f x x k (i = i1) → f x y k (j = i0) → f x (p i) k (j = i1) → f x (q i) k in hcomp u x
Hooray! Agda is happy with this.
Let’s move on to a more complicated example.
Example:
Suspensions are an example of a higher inductive type. It can be shown that spheres can be iteratively defined in terms of suspensions.
Since the -sphere is just two points (solutions to in 1 dimension), we represent this as . We can show that a suspension over this, , is equivalent to the classic -sphere, the circle .
Let’s state the lemma:
Σ2≃S¹ : Susp Bool ≃ S¹
Equivalences can be generated from isomorphisms:
Σ2≃S¹ = isoToEquiv (iso f g fg gf) where
In this model, we’re going to define and by having both the north and south poles be squished into one side. The choice of side is arbitrary, so I’ll choose . This way, is suspended into the path, and is suspended into the .
Here’s a picture of our function :
The left setup is presented in the traditional suspension layout, with meridians going through and while the right side “squishes” the north and south poles using , while having the other path represent the .
On the other side, , we want to map back from into . We can map the back into , but the types mismatch, since but . But since is , we can just concatenate with its inverse to get the full path:
In Agda, we can write it like this:
f : Susp Bool → S¹ f north = base f south = base f (merid true i) = base f (merid false i) = loop i
g : S¹ → Susp Bool g base = north g (loop i) = (merid false ∙ sym (merid true)) i
Now, the fun part is to show the extra requirements that are needed to show that these two functions indeed form an isomorphism:
Let’s show by induction on , which is of type . The case is easily handled by , since definitionally by the reduction rules we gave above.
fg : (s : S¹) → f (g s) ≡ s fg base = refl
The loop case is trickier. If we were using book HoTT, here’s how we would solve this (this result is given in Lemma 6.5.1 of the HoTT book):
Between the second and third steps, I used functoriality of the operation (equation (i) of Lemma 2.2.2 in the HoTT book).
How can we construct a cube to solve this? Like in the first example, let’s start out by writing down the face we want to end up with:
We’re looking for the path in the bottom-to-top dimension. We would like to have give us this face. This time, let’s see the whole cube first and then pick apart how it was constructed.
First of all, note that unrolling would give us , which is the same as . Since this is a composition, it deserves its own face of the cube, with our goal being the lid.
We can express this as an operation, which is similar to in that it takes the same face arguments, but produces the contents of the face rather than just the upper lid.
For the rest of the faces, we can just fill in opposite sides until the cube is complete. The Agda translation looks like this:
fg (loop i) j = let u = λ k → λ where (i = i0) → base (i = i1) → f (merid true (~ k)) (j = i0) → let u = λ k' → λ where (i = i0) → base (i = i1) → f (merid true (~ k')) in hfill u (inS (f (merid false i))) k (j = i1) → loop i in hcomp u (f (merid false i))
Nothing should be too surprising here, other than the use of a nested which is needed to describe the face that contains the composition.
Now, to prove , where . We can do induction on . Again, the point constructor cases are relatively simple.
gf : (b : Susp Bool) → g (f b) ≡ b gf north = refl gf south = merid true
For the meridian case , we can do -induction on . First, for the case, let’s see the diagram of what we’re trying to prove.
After simplifying all the expressions, we find that . So really, we’re trying to prove that .
But wait, that’s odd… there’s a in the top right corner. What can we do?
Well, we could actually use the same path on the right as on the top. We won’t even need an for this, just a clever interval expression:
gf (merid true i) j = merid true (i ∧ j)
One last cube for the case. This cube actually looks very similar to the cube, although the points are in the suspension type rather than in . Once again we have a composition, so we will need an extra to get us the front face of this cube.
This cube cleanly extracts into the following Agda code.
gf (merid false i) j = let u = λ k → λ where (i = i0) → north (i = i1) → merid true (j ∨ ~ k) (j = i0) → let u = λ k' → λ where (i = i0) → north (i = i1) → merid true (~ k') in hfill u (inS (merid false i)) k (j = i1) → merid false i in hcomp u (merid false i)
These are some of my takeaways from studying cubical type theory and these past few weeks. One thing I’d have to note is that drawing all these cubes really does make me wish there was some kind of 3D visualizer for these cubes…
Anyway, that’s all! See you next post :)
References
- https://arxiv.org/abs/1611.02108
- https://agda.readthedocs.io/en/v2.7.0/language/cubical.html
- https://1lab.dev/1Lab.Path.html#box-filling
- https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/Agda/Cubical/Lecture8-notes.lagda.md#homogeneous-composition-hcomp