Warming up to Homotopy Type Theory

“Why do you hate homotopy type theory?” is question I am sometimes asked, but I never answer it, because the question has an inaccurate presupposition. I am not happy when people forget that function extensionality, a key benefit of HoTT, was already available in Observational Type Theory. I am not happy when people disregard the convenience of having a clearly delimited fragment of one’s propositions where proofs can be identified definitionally. I am not happy when people act as if homotopy type theory already works when, without an internal notion of computation which gives canonical forms (like OTT has), it doesn’t…yet. But I’m pretty sure it will acquire such a notion. So, for the avoidance of doubt, I do not hate homotopy type theory: I hate homotopy type theorists almost as much as I hate myself, which is why I have decided to become a homotopy type theorist as a kind of therapy. I’ve been thinking quite a lot, of late, about how to make homotopy type theory go, being as I am, an incorrigible tinkerer with computational mechanisms, and I think I’m onto something. By way of taking Ariadne’s advice, I thought I’d bruce out some ravings about where I think I’ve got to. I suspect I’m not going to be very helpful to people who aren’t already HoTT-headed, and probably not all that helpful to those who are, so let me manage expectations downwards: I’m not attempting pedagogy, I’m just thinking aloud.

As some of you may know, I’m from Northern Ireland, a place which naturally promotes homotopic (not that they would call it that, in case someone thought they were gay, given that malapropism is the fourth most popular national pastime after (in reverse order) homophobia, sectarianism and emigration) considerations as a consequence of the inconveniently large lake in the middle of it. “Who lives in the big blue bit?”(*), asked former Secretary of State, Sir Humphrey Atkins, when presented with a map of the place, shaded in accordance with sectarian affiliation. But I digress. Lough Neagh (which is pronounced something roughly like “Loch Nay”, giving us Northern Irish one more “ough” than the rest of yous) is the hole where the Isle of Man used to be until Fionn mac Cumhaill threw it at someone and missed.

But the point is that if you’re going from Antrim to Enniskillen, you’ve got to go round Lough Neagh one way or the other, and no matter how much you stretch or divert your route, if you stay dry, you won’t deform one way into the other. And indeed, if you happen to be in Antrim and you ask for directions to Enniskillen, they’ll most likely tell you “If I was going to Enniskillen, I wouldn’t start from here.”. Much in the same way (upto deformation, I hope), if I was going to Homotopy Type Theory, I wouldn’t start from the Calculus of Inductive Constructions.

Why not? Because we start from the strange idea that equality is some sort of inductive definition

  Id (X : *)(x : X)(y : X) : *
  refl (X : *)(x : X) : Id X x x

which already places too much faith in the disappointing accident that is the definitional equality of an intensional type theory, and then we add an eliminator with a computation rule which nails our moving parts to said accident…

  J (X : *)(x : X)(P (y : X)(q : Id X x y) : *)(m : P x (refl X x))
    (y : X)(q : Id X x y) : P y q
  J _ _ _ m _ (refl _ _) = m

…right? What does that do? It says that whenever the proof of the equation is by reflexivity, the value m to be transported is already of the right type, so we don’t even need to think about what we have to do to it. If we are willing to consider only do-no-work transportation, we will never be able to escape from the definitional equality. (Note that the purpose of pattern matching q against refl is just to have a sound but not complete check that x is definitionally equal to y. If you like proof irrelevance (much more fun than K, for example), then you can just ignore q and decide definitional equality of x and y. I mean, if you’ve gone to the trouble of engineering a decidable definitional equality, you might as well get paid for it.)

But we don’t stick with definitional equality, and thank goodness for that. Observational Type Theory gives you structural equality on types and thus do-no-work-after-program-extraction transportation, but for open terms (and to be conservative over intensional type theory), we needed to refocus our efforts around the machinery of transportation, so that nontrivial explanations of equality result in nontrivial computations between types. That’s enough to get extensionality working. But univalence (the type of Antrim stuff is equal to the type of Enniskillen stuff if you have a way to transport it either way, such that a “there and back trip” makes no change to the stuff and orbits Lough Neagh a net total of zero times) is a whole other business, because now we can’t get away with just looking at the types to figure out what’s going on: we have to look at the particular route by which the types are connected.

(Local simile switch. Thorsten Altenkirch, Wouter Swierstra and I built an extensionality boat. We might imagine that one day there will be a fabulous univalence ship: the extensionality boat is just one of its lifeboats. But nobody’s built the ship yet, so don’t be too dismissive of our wee boat. You might learn something about building ships by thinking about that boat. I come from Belfast: we built the Titanic and then some prick sailed it into an iceberg because they made a valid deduction from a false hypothesis.)

So, what’s the plan? Firstly, decompose equality into two separate aspects: type equivalence and its refinement, value equality. The former is canonical.

  (X : *) {=} (Y : *)  :  *

I’m using braces rather than angle brackets only because I have to fight HTML.

The latter is computed by recursion over the former.

  (x : X) =[ (Q : X {=} Y) ]= (y : Y)  :  *

That is, the somewhat annotated mixfix operator =[…]= interprets a type isomorphism between types as the value equality relation thus induced on those types. I shall HoTT in Rel for this.

Value equality is thus heterogeneous in a way which necessarily depends on the type isomorphism which documents how to go about considering the values comparable. Let’s be quite concrete about that dependency. We get to look at Q to figure out how to relate x and y.

Reflexivity is not a constructor of {=}. Rather, every canonical type former induces a canonical constructor of {=}. In particular

  *^            :  * {=} *
  X =[ *^ ]= Y  =  X {=} Y

We may add

  sym (Q : X {=} Y)  :  Y {=} X
  y =[ sym Q ]= x    =  x =[ Q ]= y

  trans (Y : *)(XY : X {=} Y)(YZ : Y {=} Z) : X {=} Z
  x =[ trans Y XY YZ ]= z  =  Sigma Y \ y -> x =[ XY ]= y * y =[ YZ ]= z

Function extensionality becomes the value equality induced by the structural isomorphism for Pi-types. Types on which we depend turn into triples of two-things-and-a-path-between-them.

  Pi^ (S^ : S' {=} S`)
      (T^ : (s : Sigma (S' * S`) \ ss -> (s^ : ss car =[ S^ ]= ss cdr))
            -> T' (s car car) {=} T` (s car cdr))
    : Pi S' T' {=} Pi S` T`
  f' =[ Pi^ S^ T^ ]= f`  =  (s : Sigma (S' * S`) \ ss -> (s^ : ss car =[ S^ ]= ss cdr)) ->
    f' (s car car) =[ T^ s ]= f` (s car cdr)

Every elimination form must give rise to an elimination form for the corresponding equality proofs: if you eliminate equal things in equal ways, you get equal results, and these things have to compute when you get canonical proofs of equations between canonical things being eliminated. Consequently, reflexivity shows up as the translation from types to type isomorphisms, then from values to the equality induced by those type isomorphisms. In Observational Type Theory as we implemented it, reflexivity was an axiom, because by proof irrelevance (by which I mean by making sure never to look at the proof) it didn’t matter what it was: the half-built Death Star was fully operational. Here, we can’t get away with that dodge. Fortunately, I have at least some clue how to proceed. My less famous LICS rejectum, joint work with Thorsten, gives a vague sketch of the construction. The upshot is that every

X : *

has some

X^ : X {=} X

, and by way of a refinement, every

x : X

has some

x^ : x =[ X^ ]= x

.

Now, a type isomorphism is no use unless you can actually get from one side of it to the other. We shall need that type isomorphisms induce paths between values. That is, we shall need an eliminator

  path (S : *)(T : *)(Q : S {=} T)(s : S) : Sigma T \ t -> s =[ Q ]= t

and moreover, we shall need that paths are unique, in the sense that, for given inputs, every pair in the return type of

path

is equal to the thing that

path

returns. That is, we have a kind of propositional η-rule for paths. I’m not yet sure of the most ergonomic way to formulate that uniqueness. But consider, in particular, q : x =[ X^ ]= y. We will have that (x , x^) =[…]= (y , q) in the type of paths from x via X^. We thus recover more or less the J rule, seen as transportation between two path-dependent types.

  J (X : *)(x : X)
    (P : ((Sigma X \ y -> x =[ X^ ]= y) -> *)
    (m : P (x , x^))
    (y : X)(q : x =[ X^ ]= y)
    : P (y , q)
  J X x P m y q =
    path (P (x , x^)) (P (y , q)) (P^ (((x , x^) , (y , q)) , ... path uniqueness ...))
      m car

To achieve the definitional equational theory we’re used to from the J rule, we will need to make sure that the reflexivity construction, x^, generates proofs which are recognizably of that provenance, and we shall have to ensure that being recognizably reflexive is preserved by elimination forms, e.g., that we can take

  f^ ((s , s) , s^) = (f s)^

so that we can make

  path X X X^ x = (x , x^)

If we can obtain that path uniqueness from x along X^ when applied to (x , x^) gives (x , x^)^, then we shall have

  J X x P m x x^
    = path (P (x , x^)) (P (x , x^)) (P^ (((x , x^) , (x , x^)) , (x , x^)^)) m car
    = path (P (x , x^)) (P (x , x^)) (P (x , x^))^ m car
    = (m , m^) car
    = m

That is, the computationally obscure J rule has been decomposed into in-your-face transportation and path uniqueness. Somehow, I’m not surprised. It would not be the first time that a dependent eliminator has been recast as a non-dependent eliminator fixed up by an η-law. That’s exactly how I obtained a dependent case analysis principle for coinductive data without losing subject reduction.

Of course, we shall need to define

path

by recursion over type isomorphisms. We shall thus need to say how to compute

path Y X (sym XY) y

, which amounts to delivering the path in the other direction (the htap?), and its uniqueness. Transitivity goes (I hope) by composition.

So what of univalence? It’s not an axiom. It’s a constructor for

X {=} Y

where you just give the implementations of both path directions and show their uniqueness, thus explaining how to implement the elimination behaviour. We then need something like

  x =[ Univalence X Y xy yx ... ]= y  =  xy x =[ Y^ ]= y

but that’s annoyingly lopsided. We also need to know when isomorphisms are equal. Something like

  Q =[ X {=} Y ]= Q'  =  (\ x -> path X Y Q car) =[ (X -> Y)^ ]= (\ x -> path X Y Q' car)

might be enough, but again annoyingly lopsided.

It’s late and I’m tired, so I suppose I should try to sum up what I’m getting at. I’m hoping we can get to a computational treatment of univalence by isolating the notion of type isomorphism in quite an intensional way. On the one hand, the structure of a type isomorphism tells us how to formulate the equality for values in the related types. On the other hand, the structure of a particular type isomorphism tells us how to compute the transportations of values across it, giving rise to unique paths. Univalence allows us to propose arbitrary isomorphisms, and somehow, univalence gives an η-long normal form for type isomorphism: every type isomorphism is provably equal to the packaging-by-univalence of its elimination behaviour.

However, hilariously, we have to make sure that the relations =[…]= induces between equivalent type isomorphisms are equivalent (i.e. pointwise isomorphic), in order to show that =[…]=, like all the other elimination forms, respects equality. As County Antrim folk say, “There’s nothing for nothing in Islandmagee.”. Islandmagee, by the way, is the peninsula on the east coast, across the narrow sea from Westeros (which is a rehabilitated landfill site between Whitehead and Larne), apparently containing nothing.

(*) Eels, mostly.