What’s Special About Identity Types

From a homotopy theorist’s point of view, identity types and their connection to homotopy theory are perfectly natural: they are “path objects” in the category of types. However, from a type theorist’s point of view, they are somewhat more mysterious. In particular, identity types are just one particular inductive family; so what’s special about them that they give us homotopy theory and other inductive families don’t? And specifically, how can it be that we “get out” of identity types more than we inductively “put into them”; i.e. why can there be elements of Id(x,x) other than refl, whereas for some other inductive types like Fin, we can prove that there’s nothing in them other than what we put in?

Dan Licata’s recent post partly answered the second of these questions. He pointed out that instead of an inductive family indexed by $A\times A$ , we can regard $\mathrm{Id}_A$ as indexed by one copy of A and parametrized by the other. Then, for any fixed M:A, it is provable that any element of $\mathrm{Id}_A(M,N)$ must be of the form refl M.

However, he also mentioned that identity types are still different from some other inductive families in what we can prove about inhabitants of a specific instance. For instance, we can prove (using a large elimination) that there are no elements in Fin 0 and that there is exactly one element in Fin 1, which are specific instances of the inductive family Fin of finite sets. However, we cannot prove that there is exactly one element of Id M M, which is a specific instance of the family of identity types. When I asked why, the answer I got was that it has to do with what you know about the index type.

This is a good answer, but I don’t think it’s quite the whole story. For instance, there are inductive families with an arbitrary index type, but for which we can prove things about inhabitants of specific instances. An obvious example is the inductive family with no constructors. On the other hand, another obvious question is what we need to know about the index type in order to prove things about inhabitants of specific instances? Finally, what is special about identity types that they relate to homotopy theory, and can we say something similar about any other inductive families?

The answer I’m about to give is probably obvious to some people, but it wasn’t obvious to me at first, so I thought I would share it. (I wrote this post over the weekend with no Internet access. When I got back, I discovered that Peter Lumsdaine had already mentioned part of what I’m about to say over at the n-Cafe.)

Recall that in categorical semantics for type theory in a locally cartesian closed category, an ordinary W-type is a (weakly) initial algebra for a polynomial functor. This is a functor of the form $\Sigma_A \Pi_{p} B^*$ , where $p\colon B\to A$ is arbitrary map, representing a dependent type (sometimes called a “container” in this context).

For instance, the natural numbers are the initial algebra for the polynomial functor defined by $p\colon 1\to 2$ . This says that they have two constructors (zero and succ), one of which has arity 0 (the point of 2 not in the image of 1) and the other of which has one recursive input (the other point of 2, over which the fiber of p is 1).

More generally, an inductive family is a (weakly) initial algebra for a dependent polynomial functor on a slice category $\mathcal{C}/X$ , which is a functor of the form $\Sigma_s \Pi_{p} r^*$ for a given diagram

$\displaystyle X \overset{r}{\longleftarrow} B \overset{p}{\longrightarrow} A \overset{s}{\longrightarrow} X$

(I feel the need to point out, since it confused me once, that this diagram does not in general live entirely in $\mathcal{C}/X$ — which is to say that we do not have s p = r. However, the whole diagram may be taking place in some other slice category over an ambient context $\Gamma$ of “parameters,” as opposed to the “indices” X.)

For instance, the family Fin of finite sets, indexed over the natural numbers, is the initial algebra for the dependent polynomial functor determined by

$\displaystyle \mathbb{N} \overset{\mathrm{id}}{\longleftarrow} \mathbb{N} \overset{\mathrm{inj}_2}{\longrightarrow} \mathbb{N}+\mathbb{N} \overset{[\mathrm{id},+1]}{\longrightarrow} \mathbb{N}$

This says that Fin 0 has one constructor of arity zero, while Fin (succ n) has two constructors, one of arity zero and one which takes an input of type Fin n. Similarly, the identity type of X can be defined by the data

$\displaystyle X \longleftarrow 0 \longrightarrow X \overset{\Delta}{\longrightarrow} X\times X$

This says that there is one nullary constructor of type Id x x, for any x:X.

Now in intensional type theory, nothing mandates that every morphism in the category represents a dependent type; we can specify a suitable subclass of display maps which do. The display maps must be closed under pullback along arbitrary maps (for reindexing), composition (for dependent sums), and exponentials (for dependent products). The latter means that if p is a display map, then we have a functor $\Pi_p$ which acts on display maps. This means that in order for a dependent polynomial functor, defined as above, to take display maps to display maps, we must have p and s being display maps. This restriction would give us one notion of “inductive family” in a category with display maps.

However, if all we want to do is define inductive families, we don’t actually need to require s to be a display map. We do need to require p to be a display map in order for the functor $\Pi_p$ to exist; but even if s is not a display map, the functor $\Sigma_s$ still exists (it is just composition with s), though it may not take display maps to display maps. Thus, if only p is a display map, we have a “dependent polynomial functor”

$\displaystyle F = \Sigma_s \Pi_{p} r^* \colon \mathrm{Disp}/X \to \mathcal{C}/X$

taking the category of display maps over X into the full slice category over X. We can then still define what an algebra for this functor is (a display map $q\colon C\to X$ with a map $F q \to q$ over X) and thereby a (weakly) initial algebra, and call such a thing an inductive family.

I claim that what gives rise to “extra stuff” in inductive families that we didn’t “put into them” is precisely this fact that s may not be a display map. On the one hand, if s is a display map, then it’s quite easy to prove that everything in the inductive family comes from some constructor. This is done at the beginning of this file. Note that there is no large elim here; the large elim comes in when constructing the dependent type corresponding to s in examples such as Fin.

On the other hand, of course the diagonal $X\to X\times X$ is not generally a display map. Saying that it is is more or less tantamount to saying that the type X has computationally decidable equality, and this is known to imply that it is a set; i.e. that there’s nothing other than refl in its identity type.

But what about other cases when s is not a display map? Consider the general case when the object B is empty, so that the dependent polynomial functor is constant at s. (In particular, the functor for identity types is of this form.) If s is a display map, then an initial algebra for such a functor must be s itself, so that what we get out is exactly what we put in. But if s is not a display map, then a weakly initial algebra for this functor will instead be some display map $\hat{s}\colon \hat{A} \to X$ equipped with a map $\check{s}\colon s \to \hat{s}$ over X, having the property that any other map $s \to q$ over X, with q a display map, factors through $\check{s}$ . The “extra stuff” that might turn up in the inductive family is precisely the failure of $\check{s}$ to be an isomorphism, since A is what we “put in” and $\hat{A}$ is what we “get out.”

Here’s what that inductive family looks like in Coq:

Inductive hfiber {A X} (f : A -> X) : (X -> Type) :=
  inj : forall (x : A), hfiber f (f x).

I’ve called it hfiber because in homotopy theory, this type represents the homotopy fiber of the map f. Now since display maps are closed under pullback, the property of $\check{s}$ cited above implies that $\check{s}$ has the left lifting property with respect to all display maps. Therefore, if we have all inductive families, then there is a weak factorization system whose right class is generated by the display maps; the factorizations are given by $s = \hat{s} \check{s}$ . Conversely, such a weak factorization system amounts more or less to having inductive families of the hfiber sort.

From this point of view, of course, the identity type of X is just the homotopy fiber of the diagonal $X\to X\times X$ (where we can either regard both copies of X as indices, or one as a parameter and one as an index, as Dan described). In terms of homotopy theory, these are the path objects relative to the weak factorization system. On the other hand, Nicola Gambino and Richard Garner proved that from only the identity types, one can construct the whole weak factorization system. (Their argument is precisely analogous to the “mapping path space” in homotopy theory, which constructs factorizations out of path objects.)

Furthermore, if we combine hfiber with inductive families for dependent polynomials where s is a display map, then we can construct the more general sort of inductive families where s isn’t a display map, by first constructing the homotopy fiber of s (and using a large elimination). Such a construction is also implemented here (same file as before). Thus, general inductive families can be reduced to a combination of inductive families where s is a display map — which behave in more of the way a type theorist might naively expect (there is nothing in them that we didn’t put in) — plus a weak factorization system (or, equivalently, identity types), which both (1) introduces homotopy theory and (2) allows the definition of more general inductive families.

As a homotopy theorist, I find this a satisfying answer as to why identity types seem to be special among inductive families. But I’m interested to hear the response of the type theorists.

9 Responses to What’s Special About Identity Types

Jesse C. McKeown says:

12 May 2011 at 16:21

As an algebraic-topologist-in-formation, what I find weird about the definition of x~~>y is that it appears to be described as an initial functor; and seemingly strictly initial, at that. I’m used to x ~~> y being the weak pull-back of (x’:*→ X) along (y’:*→X). Of course, things like this are happening all the time. The inductive point
Inductive point : Type := the_point : point.
is defined as the initial provable type; but it is provably contractible, and so (weakly) terminal. And back in the older world of CW-type homotopy types, one can also realize, say ΣΩₓX as the weak pull-back of X∨ₓX→X² along Δ:X→X², where it would ordinarily by the weak push-out of ΩₓX→* along itself. But still, it seems more than a bit weird that an important family of spaces should have concise descriptions in both directions.

- Mike Shulman says:
  
  27 January 2013 at 12:08
  
  Looking back at this comment from over a year ago, I think I have an answer now. (Higher) inductive types are freely generated types. Recalling that types are (like) weak ∞-groupoids, for a fixed object x:X, the identity type $(y:X) \vdash (x=y) \mathsf{type}$ is the presheaf $X \to \mathsf{Type}$ freely generated by a single generator $\mathsf{refl}_x : (x=x)$ . And it’s well-known that the presheaf freely generated by one generator is a representable functor (this is essentially the Yoneda lemma). I think this is a good way of seeing why you get identity types described as a free structure.
  
  - jessemckeown says:
    
    28 January 2013 at 00:33
    
    Interesting!
    
Mike Nahas says:

26 January 2013 at 21:56

Why is the identity type special? One possible answer is that it’s the propositional analog to a definitional construct.

The simplest definitional construct is the horizontal bar. Given the things above the bar, we get the result below it. But inside a proposition, we can’t refer to the horizontal bar. The result is that the most primitive type operator is “->”, which is works a lot like the horizontal bar (prerequisites giving a conclusion) but is inside the language. (The horizontal bar and -> have to be different, or you get the infinite list in What the Tortoise Said to Achilles.)

My thought is propositional equality is special for the same reason. We have a judgement of “a=b:A”. We need an analog for it inside the type theory that lets us capture the concept.

- Mike Shulman says:
  
  26 January 2013 at 22:45
  
  Hmm… is there an internal analogue of the judgment “a:A”?
  
  - Michael Nahas says:
    
    27 January 2013 at 08:37
    
    I’m sure we can find out by looking at Dan Grayson’s implementation of TS in LF. In that, every rule of TS would have had to be written as a theorem of the system in LF. Of course, the LF system is so close to TS that “a:A” may just be “a:A”. (However, “A is a Type” probably looks a little different.)
    
    My other thought is that this could just be parallel development: that the same motivations for the horizontal bar and definitional equals give rise to -> and propositional equals. (In my first post, my thinking was that the similarity was some sort of reflection, that the propositional equals was a way to refer to definitional equals inside a type.)
    
    - Mike Shulman says:
      
      27 January 2013 at 12:04
      
      No, I think when you implement a type theory in a logical framework, the LF theorems are exactly the judgments of the object theory, which is different from some internalized representation of them in the object theory. For instance, there will be an LF type that describes the definitional equality judgment of TS, but that is not the same as the identity type of TS, which is a TS type, not an LF type.
      
      - Michael Nahas says:
        
        27 January 2013 at 16:06
        
        Sorry, there were a few leaps in my thought process that I forgot to write down.
        
        Yes, it’s my understanding too that the theorems in LF will be the judgements in TS.
        
        If we look at how the rules of TS are written in LF, I think we’ll see that the “horizontal bar” in TS is the “->” in LF. Thus, confirming the connection between the two concepts. My (too abbreviated) thought was: if we want to see how TS internalizes “a:A”, we can start by looking at how LF does it for TS. Then we might find a similar internal representation inside TS. Likewise, we can look at how LF implements TS’s definitional equality to see if the identity type in TS is fulfilling the same role.
        
        My intuition is that definitional and propositional equality fulfill the same role in most type systems. Most type systems have a computational component and equality in a type system usually means convertibility – the values reduce to the same normal form. That is, if you compute both “(add 1 3)” and “(add 2 2)”, they’ll both reduce to “4”, which means they’re equal.
        
        My (rudimentary) understanding of TS is that it doesn’t have a computational component. The univalent axiom can introduce equality without a way to compute conversion. (It’s axiomatic, after all.) So, either we need to work on that aspect of HoTT or we need to look at non-computational type systems for inspiration.
        
        
        Mike Shulman says:
        
        27 January 2013 at 16:46
        
        As far as I can tell, in homotopy type theory, definitional and propositional equality play very different roles. Propositional equalities can be nontrivial, like automorphisms giving rise to paths in the universe under univalence, whereas definitional equalities cannot.