Adventures in CubicalTT (Part 4)

Last time we discussed how to work with Higher Inductive Types. This time, I planed on talking about quotient types. Before getting into the topic at hand, however, I want to discuss sigma types. CubicalTT supports them via the ((a : A) * B a) notation, and the ordinary product type can be defined as ((_:A) * B). The first element of a product, z, is denoted z.1, and the second is z.2.

Like with the function types, CubicalTT understands eta equivalence.

prodEta (A : U) (B : A -> U) (p : (a:A) * B a) : Id ((a:A) * B a) p ( p.1, p.2 ) = <i> p

And we can combine the two conversions.

EtaConvFP (A Y : U) (B : A -> U) (u : Y -> (a:A) * B a) : Id (Y -> (a:A) * B a) u (\(y : Y) -> ( (u y).1, (u y).2 )) = <i> u

One thing I wondered is how one would prove that this is a categorical product. First, I’ll define the projection functions and the non-dependant product to emphasize my argument.

prod (A B : U) : U = (_:A) * B

proj1 (A B : U) (z : prod A B) : A = z.1
proj2 (A B : U) (z : prod A B) : B = z.2

I also need composition;

compose (A B C : U) (f : B -> C) (g : A -> B) : (A -> C) = \(a : A) -> f (g a) 

A categorical product has to satisfy the following commutative diagram;

   f / | \ g
   /   |   \      
|/     V     \|
A <- A x B -> B
proj1     proj2

That is to say, for any type Y with functions f and/or g going to A and B, there should be a unique function U, such that proj1 o U = f and proj2 o U = g. It’s fairly easy to find the correct U;

pU (A B Y : U) (f : Y -> A) (g : Y -> B) : Y -> prod A B = \(y : Y) -> (f y, g y)

And it’s easy to prove that it satisfies the diagram;

pUt1 (A B Y : U) (f : Y -> A) (g : Y -> B) : Id (Y -> A) f (compose Y (prod A B) A (proj1 A B) (pU A B Y f g)) = <i> f

pUt2 (A B Y : U) (f : Y -> A) (g : Y -> B) : Id (Y -> B) g (compose Y (prod A B) B (proj2 A B) (pU A B Y f g)) = <i> g

Lastly, we need to prove that pU is unique. We need to show that, for any u satisfying the diagram, u = pU. This ends up not being that hard.

product (A B Y : U) (f : Y -> A) (g : Y -> B) (u : Y -> prod A B)
        (p1 : Id (Y -> A) f (compose Y (prod A B) A (proj1 A B) u) )
        (p2 : Id (Y -> B) g (compose Y (prod A B) B (proj2 A B) u) ) :
        Id (Y -> prod A B) (pU A B Y f g) u =
        <i> \(y : Y) -> ( (p1 @ i) y , (p2 @ i) y )

To elaborate on this proof, we can ask what happens at the beginning and end of this path. At first we have

\(y : Y) -> ( (p1 @ 0) y , (p2 @ 0) y ) = \(y : Y) -> ( f y , g y ) = pU

And at last we have

\(y : Y) -> ( (p1 @ 1) y , (p2 @ 1) y ) = \(y : Y) -> ( proj1 (u y) , proj2 (u y) ) = u

Justifying our conclusion. This doesn’t directly relate to the central topic of this post, but I wanted to talk about this.

I said that this post would be about quotient types, but I didn’t actually do much related to quotient types since my last post. Instead, I focused on other things, and most of the stuff in this post will be miscellaneous stuff I feel is worth commenting on.

To give an understanding of the utility of quotient types, I recommend reading section 7 “General Covariance” of Homotopy Type Theory: A synthetic approach to higher equalities by Michael Shulman. While I recommend reading the whole thing, that section has the main take away point for why quotient types are useful. We can strip away undesired structure by adding identity paths between things which we want to be impossible to differentiate.

A simple example is the naturals equated by parity. That is to say, we start with the naturals, and we assert that any two even numbers are equal, and any two odd numbers are equal;

data pnats = zeroP
           | sucP (n : pnats)
           | parityPath (n : pnats) <i> [ (i=0) -> n, (i=1) -> sucP (sucP n) ]

From here we can, for instance, prove that 3 equals 1.

oneP : pnats = sucP zeroP
twoP : pnats = sucP oneP
threeP : pnats = sucP twoP

pnatsTest : Id pnats oneP threeP =
  <i> parityPath{pnats} oneP @ i

We might think that this is isomorphic to the booleans, but in fact it is not. The reason is that pnats has non-trivial paths from 0 and 1 back onto themselves. I’ve only done a little work on this, so I have nothing to really show.

A lot of what I wanted to do required GADTs. As an example, I wanted to use HITs to model proper binary naturals. One can do this by just asserting that 00 = 0 and 10 = 1, like so;

data bnat2 = Z2
           | O2
           | ZS2 (n : bnat2)
           | OS2 (n : bnat2)
           | p00 <i> [ (i=0) -> Z2, (i=1) -> ZS2 Z2]
           | p10 <i> [ (i=0) -> O2, (i=1) -> OS2 Z2]

And this will work, but there’s a better way. With GADTs, we could have the binary number carry its natural value along with it. If two binary nats have the same nat value, then they are the same. We could do something like so;

data bnatG : nat -> U where
  ZG : bnatG zero
  OG : bnatG (suc zero)
  ZSG : (n : nat) -> bnatG n -> bnatG (mult 2 n)
  OSG : (n : nat) -> bnatG n -> bnatG (plus (suc zero) (mult 2 n))
  bnatNorm : (n : nat) -> (b1 b2 : bnatG n) -> <i> [ (i=0) -> b1, (i=1) -> b2 ]

Unfortunately, this is something for the future. When it does come, this bnatG should be provably equivalent to bnat2, generating the same paths.

Speaking of the future, I spent much of my time getting side tracked, thinking of directed homotopy types. These are types where the paths have a direction to them, which is to say, they wouldn’t be invertible. Instead of each type being an infinity-groupoid, each type would be an infinity-category. You can think of them as paths in a directed space, where you could go down hill, but never up it.

Based on some of the material I’ve been reading recently, I began wondering about the category of natural numbers. There are two main categories of natural numbers. One exists where matrices are the morphisms, with every n x m matrix being a morphism from n to m. Another has a morphism from n to m so long as n ≤ m. I began wondering how these categories would be defined as types in a dependently typed language, assuming it has directed homotopy types. The later might be easy, defined like so;

data lenats = ZLE
            | SLE (n : lenats)
            | sleLE (n : lenats) <i> [ (i=0) -> n, (i=1) -> SLE n ]

We could compose paths from (m to n) and (n to o) together to form new paths from m to o;

lenatsT (m n o : lenats) (p1 : path lenats m n) (p2 : path lenats n o) : path lenats m n =
  <i> comp lenats p1 [ (i=1) -> <k> p2 @ k ]

I then started wondering about matrices, and how they could be used to create the appropriate type. In CubicalTT, to do something along these lines, you start with some type, A, and some relation on A, R : A -> A -> U. You then assert that this relation generates paths in the new type.

data Quotiented (A : U) (R : A -> A -> R)
    = quot (a : A)
    | path1 (a b : A) (r : R a b) <i> [ (i = 0) -> quot a, (i = 1) -> quot b ]
    | path2 ...

There aren’t too many examples of this in the library, but here is one example usage to create a quotient set out of some relation;

data Quot (A : U) (R : A -> A -> U) =
    quot (a : A)
  | identification (a b : A) (r : R a b) <i> [ (i = 0) -> quot a, (i = 1) -> quot b ]
  | setTruncation (a b : Quot A R) (p q : Id (Quot A R) a b) <i j> 
       [ (i = 0) -> p @ j
       , (i = 1) -> q @ j
       , (j = 0) -> a
       , (j = 1) -> b ]

Generally I’d assume that R should at least be an equivalence relation, but that’s not actually necessary. I wanted to use this to recreate my parity naturals, but I couldn’t think of a way to define the appropriate relation without GADTs.

data SameParity : (n m : nat) -> U where
  ZP  : SameParity zero zero
  PLE : (n m : nat) -> SameParity n m -> SameParity (suc n) (suc m)
  SSP : (n m : nat) -> SameParity n m -> SameParity n (suc (suc m))
  INV : (n m : nat) -> SameParity n m -> SameParity m n

If I did define them with Quot, they might actually be equal to the booleans, though I’m not sure.

You could use this, almost unaltered, to generate the necessary morphisms in the category with matrices. Just define R n m to exist whenever an n x m matrix does. One could go further and define a generic category of relations.

One should question, then, how one would create morphisms in the type universe. The way this is done in CubicalTT is through the glue operation, which asserts a morphism whenever an equivalence exists, essentially implementing univalence. I’m not actually sure about this, but my immediate intuition is that any functor should induce a morphism in U. We could start off with a keyword, funct, and construct the appropriate proof;

-- Category with three objects
data Cat3 = o1
          | o2
          | o3
          | m12 <i> [(i=0) -> o1, (i=1) -> o2]
          | m23 <i> [(i=0) -> o2, (i=1) -> o3]

-- Category with two objects
data Cat2 = o1
          | o2
          | m12 <i> [(i=0) -> o1, (i=1) -> o2]

Cat32Funct : Cat3 -> Cat2 = split
  o1 -> o1
  o2 -> o2
  o3 -> o2
  m12 @ i -> <k> m12{Cat2} @ i
  m23 @ i -> idpath Cat2 o2 @ i

Now that I think about it, I’m pretty sure the properties of functors hold automatically/definitionally for all functions, and there’s nothing to prove. That would mean that all functions are functors, and therefore all should induce morphisms in U.

PathCat32 : path U Cat3 Cat2 =
  <i> funct Cat3 [(i=0) -> (Cat2, Cat32Funct)]

I suppose that makes sense. An equivalence should be, more or less, an invertible function, and induce an invertible morphism. A non-invertible equivalence would not be an equivalence at all, just a function, and induce an ordinary morphism.

Of course, directed homotopy types are a long ways off, so I’ll get onto more relevant things.

As a follow up to my square manipulation functions, I decided to try creating functions which would collapse a square into a triangle. This ended up needing the /\ and \/ operators. As an example, this will collapse the top right corner.

SquareCollapseTR (A : U) (a00 a10 a01 a11 : A) (a0010 : Id A a00 a10) (a0001 : Id A a00 a01) (a1011 : Id A a10 a11) (a0111 : Id A a01 a11)
            (Sq : Square A a00 a10 a0010
                           a01 a11 a0111 a0001 a1011) :
            Square A a00 a11 (<i> comp A (a0010 @ i) [ (i=1) -> <j> a1011 @ j ]) 
                     a01 a11 a0111 a0001 (refl A a11) =
           <i j> comp A (Sq @ i @ j) [ (i=1) -> <k> a1011 @ (k \/ j) ]

Note the path on the bottom. We start with Sq, which will begin at a00 = a01, and end at a10 = a11. We then compose it with a1011 @ (k \/ j), which will begin at a1011 @ (k \/ 0) = a1011 @ k : a10 = 11, the same as the ending to our square, and will end at a1011 @ (k \/ 1) = a1011 @ 1 = a11.

Also note the composition path that we used in our return square type. It runs from a00, through a10 (which we’re getting rid of), to a11. If we instead chose to run through a01, we’d generate a type error. Here are the other variations on this I made;

SquareCollapseBR (A : U) (a00 a10 a01 a11 : A) (a0010 : Id A a00 a10) (a0001 : Id A a00 a01) (a1011 : Id A a10 a11) (a0111 : Id A a01 a11)
            (Sq : Square A a00 a10 a0010
                           a01 a11 a0111 a0001 a1011) :
            Square A a00 a10 a0010
                     a01 a10 (<i> comp A (a0111 @ i) [ (i = 1) -> <j> a1011 @ -j ]) a0001 (refl A a10) =
           <i j> comp A (Sq @ i @ j) [ (i=1) -> <k> a1011 @ (-k /\ j) ]

SquareCollapseTL (A : U) (a00 a10 a01 a11 : A) (a0010 : Id A a00 a10) (a0001 : Id A a00 a01) (a1011 : Id A a10 a11) (a0111 : Id A a01 a11)
            (Sq : Square A a00 a10 a0010
                           a01 a11 a0111 a0001 a1011) :
            Square A a01 a10 (<i> comp A (a0010 @ i) [ (i = 0) -> <j> a0001 @ j ]) 
                     a01 a11 a0111 (refl A a01) a1011 =
           <i j> comp A (Sq @ i @ j) [ (i=0) -> <k> a0001 @ (k \/ j) ]

SquareCollapseBL (A : U) (a00 a10 a01 a11 : A) (a0010 : Id A a00 a10) (a0001 : Id A a00 a01) (a1011 : Id A a10 a11) (a0111 : Id A a01 a11)
            (Sq : Square A a00 a10 a0010
                           a01 a11 a0111 a0001 a1011) :
            Square A a00 a10 a0010 
                     a00 a11 (<i> comp A (a0111 @ i) [ (i = 0) -> <j> a0001 @ -j ]) (refl A a00) a1011 =
           <i j> comp A (Sq @ i @ j) [ (i=0) -> <k> a0001 @ (-k /\ j) ]

Here are also two more type equivalences I wrote. I encourage you to think about what they’re doing in detail.

UnitFUId (A : U) : Id U Unit (A -> Unit) =
  <i> glue Unit [(i=1) -> (A -> Unit
                          ,\(_:A -> Unit) -> tt
                          ,\(u:Unit)(_:A) -> u
                          ,\(u:Unit) -> <j> being u @ -j
                          ,\(f:A -> Unit) -> <j> \(a:A) -> (being (f a) @ -j)

UFAId (A : U) : Id U A (Unit -> A) =
  <i> glue A [(i=1) -> (Unit -> A
                       ,\(f:Unit -> A) -> f tt
                       ,\(a:A)(_:Unit) -> a
                       ,\(a:A) -> <_> a
                       ,\(f:Unit -> A) -> <j> \(u:Unit) -> f (being u @ -j)

That’s about it. I’ll probably write more about CubicalTT in the future, but this is the last post in this sequence. I want to write more about HITs as I understand them better.