# 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.

I had the same thought to treat equality types as indexed by their associated equivalence. It immediately reminded me of heterogeneous equality, but one which plays nicely in the presence of univalence. The explicit-path equality helps avoid the the unforgivable “adp” function in chapter 2 of the HoTT book. At the same time, it brings a pleasant symmetry to otherwise lopsided equations.

One thing that always bothered me is that path elimination rule was that it doesn’t seem to eliminate paths at all. We might call the elements of Sigma (SxS) \(s,t) -> s = t “free paths”. Given a fixed t : S in the context, we might call the elements of Sigma S \s -> s = t “one-side-free paths”. The induction laws for paths really say something about eliminating free and one-side-free paths, but neither can tell us about a path with both sides fixed.

The idea that your “path” function needs to be unique for each input sounds like it is a contractible type. Contractibility (along with propositionality) is an awfully pleasant property for any type to have. You can’t possibly get it wrong, and you can potentially lift it up to the judgmental world. It would be nice to see a compiler which was aware of this notion.

Also, I think you may have a small typo in the following line. I think perhaps you means Q : S {=} T.

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

Thanks for spotting the typo. My fingers instinctively deliver a thing which is mistaken for something which isn’t quite an html tag but near enough to be damned.

Contractibility of paths is indeed the essence of J-ness (where uniqueness of paths is K-ness). Univalence amounts to adding whatever paths you like as long as they’re contractible. We should expect to work with heterogeneous equality in a “European” type theory: homogeneity makes comparability a hostage to the disappointing accident that is the definitional/judgmental equality. Where in “John Major” equality and OTT we were able to presume that there was at most one sensible meaning for a heterogeneous equation, now we must bookkeep the basis for proposing such a thing.

I’m nervous about lifting contractibility to the judgment level, at least for paths, because we do project out the witness to the existential when we transport a value along a path. In general, you cannot get away with making something irrelevant judgmentally unless they really are irrelevant to computational processes: that there is only one thing it could possibly be isn’t irrelevant enough if you need to get your hands on that thing.

Needn’t there a caret be swinging in front of Pis nose to lure type theory’s old workhorse into the freshly digged the equality mine? f’ =[ Pi? S^ T^ ]= f` = …

Makes me want to write programs again

Hi Sebastian! Good to hear from you! And, yes.

Hi Conor,

Having recently digested a few of your papers on OTT, levitation, outrageous coincidences, and the general monad (among others), I decided to brush up on categorical as a “meditation” of sorts. I am currently reading “The Development of Categorical Logic” by John L. Bell, and I found the following excerpt from the opening chapter page 6, along with the bit about a locally small complete topos `E` giving rise to a *well-founded* model `E*` of IZF set theory, to be extremely interesting and dense — tying together many loose ends in the old noggin. Now, I am not a type theorist (IANATT?) — merely a computer scientist — by any stretch of the imagination, so this may all be common knowledge and I do realize that most papers on type theory are written for type theorists, but I find it ironic that the internal “syntax” used by many theories obscures many of the finer distinctions the categorical “semantics” helps to elucidate.

“R. Diaconescu (1975) established the important fact, conjectured by Lawvere, that, in a topos, the axiom of choice implies that the topos is Boolean. This means that, in IZF, the axiom of choice implies the law of excluded middle. This latter formulation of Diaconescu’s result was refined by Goodman and Myhill (1978) to show that, in IZF, the law of excluded middle follows from the axiom of choice for unordered pairs. (It was later realized that the law or excluded middle in fact follows from the mere existence of a choice function on the power set of a set with two elements.) In Fourman and Scedrov (1982), it was shown, using a topos of presheaves, that in intuitionistic set theory even what they termed the “world’s simplest axiom of choice”—the assertion that every family, all of whose elements are doubletons and which itself has at most a single member—may fail. (By contrast, in Grayson 1975 it is shown that Zorn’s lemma, while classically equivalent to the axiom of choice, is consistent with IZF; see also Bell 1997.) In Bell (1993), a version of Diaconescu’s theorem was used to show that the law of excluded middle is derivable within the intuitionistic version of Hilbert’s ε-calculus.

Of major significance in the development of topos theory was the emergence of the concept of classifying topos for a first-order theory, that is, a topos obtained by freely adjoining a model of the theory to the topos of constant sets. The roots of this idea lie in the work of the Grothendieck school and in Lawvere’s functorial semantics, but it was Joyal and Reyes (see Reyes 1974) who, in 1972, identified a general type of first-order theory, later called a coherent or geometric theory, which could be shown always to possess a classifying topos. This work was later extended by Reyes and Makkai to infinitary geometric theories: they showed that any topos is the classifying topos of such a theory (see Makkai and Reyes 1977). In 1973 Lawvere (see Lawvere 1975a) pointed out that, in virtue of Joyal and Reyes’s work, a previous theorem of Deligne (see Artin et al. 1964, VI 9.0) on coherent toposes—the classifying toposes of (finitary) geometric theories—was equivalent to the Gödel-Henkin completeness theorem for geometric theories. He also observed that, analogously, the theorem of Barr (1974) on the existence of “enough” Boolean toposes was equivalent to a “Boolean-valued” completeness theorem for infinitary geometric theories.

The practice of topos theory quickly spawned an associated philosophy—jocularly known as “toposophy”— whose chief tenet is the idea that, like a model of set theory, any topos may be taken as a taken as an autonomous universe of discourse or “world” in which mathematical concepts can be interpreted and constructions performed. Accordingly topos theorists sought to “relativize”—i.e., suitably interpret and prove—within an arbitrary topos results which had originally been proved for the topos of sets. One of the most important of these results was the basic theorem of J. Giraud, originally presented in Grothendieck’s Paris seminars of the early 1960s, which characterized categories of sheaves over a site in terms of exactness and size conditions. Giraud himself (1972) had proved a relative version of his theorem for Grothendieck toposes, but it was W. Mitchell who first formulated the correct form of the theorem for elementary toposes. However, Mitchell was able to prove only a special case of the theorem; it was Diaconescu (1975) who succeeded in proving the “relative Giraud

theorem” in full generality. (Later Zangwill 1980 and Chapman and Rowbottom 1991 gave purely logical proofs of the theorem within the internal language.) The principal tool introduced by Diaconescu—his theorem characterizing geometric morphisms (the natural maps between toposes) to categories of internal presheaves in a topos—turned out also to be the key to proving the relative versions of the Joyal-Reyes results on classifying toposes. The major step in this direction was taken in by G. C. Wraith, who, in 1973, constructed the classifying topos for the theory of equality—the object classifier—over an arbitrary topos with a natural number object. The general existence theorem for classifying toposes for “internal” geometric theories soon followed: this was proved independently by Joyal, Bénabou (1975) and Tierney (1976). Classifying toposes for internal algebraic theories were constructed in Johnstone and Wraith (1978), and Blass (1989) showed that the existence of an object classifier over a given topos implies that the topos has a natural number object.”

Best regards.

Ashley

Conor, do you pretend you investigate some “reality”? Or you are a “strongly advanced programmer”

No.

The idea of indexing equalities by what equivalence they’re relative to reminds me a lot of equality in CTT, where equality is indexed by the particular type it happens to be in (e.g. tt = ff in Top, but not in Bool).