Bear with me, I'm a physicist.

In homotopy type theory, as I understand it, a type $X$ is a set if all the morphisms over its terms $x:X$ are identies. When I say "morphisms", then I view the term as objects of a category, so I interpret the statement as follows:

"Per definition, a category $X$ has the identity for each object in any case, which being a morphism is a member of what we call $\mathrm{Id}_X(x,x)\subseteq\hom_X(x,x)$. And if a category is descrete (and hence there is only a structureless proper set) then these are the only morphisms to be found in the category. From a type theory perspective, we can syntactically form $\mathrm{Id}_X(x,y)$, with categorically $\mathrm{Id}_X(x,y)\subseteq\hom_X(x,y)$, and if there is a term $\mathrm{p}$ (a proof) with $\mathrm{p}:\mathrm{Id}_X(x,y)$, then it's inhabitated and true as a proposition, i.e. '$x=y$'."

Now from this, I'd define "$X$ is a set $\Longleftrightarrow$ for all elements of $X$, their homs are identities at best": $$\forall (x,y\in X).\ \hom_X(x,y)=\mathrm{Id}_X(x,y).$$ i.e. in the dependend type/fibrations lingua $$\mathrm{isSet}(X):=\Pi_{x,y:X}.\ \hom_X(x,y)=\mathrm{Id}_X(x,y),$$ In this way, the category drops (truncates?) all the non-trivial morphsism. However, what they do in the book at the beginning of chapter 3 is writting $$\mathrm{isSet}(X):=\Pi_{x,y:X}.\ \Pi_ {p,q:\mathrm{Id}_X(x,y)}.\ \mathrm{Id}_{\mathrm{Id}_X}(p,q),$$ which I read as the statement about $\mathrm{Id}_X$ of being either $\{\}$ or at best $\{*\}$. I.e. they only say $\hom(x,x)$ must be simple. The explanation seems to have to do with a "only one member like a proposition" demand.

Now the question is why my idea is wrong and how to interpret the actual definition. The book generally doesn't use the word hom so much, and so it seems they just start with the idea to call all morphsims of a category $X$ identites - is that so? It should rather be only paths like maps $[0,1]\to X$, no? Is it maybe that the univalence axiom is the ingredient which makes proper "morphism spaces" out of the more type theoretical identity type? Or does HoTT model "normal functions" only via maps $X\Rightarrow Y$ with $X,Y$ types. Let me put it like this: Where are the normal homs?

And regarding the interpretation of $\mathrm{Id}_X$ to begin with: Should I visualize, in category being a bunch of dots and arrows, one and the same object put in multiple times? E.g. in the graphics of a NNO, $\mathbb N$ is "in the category more than once, for drawing purposes". I feel I need to view $X$ this way to make sense of (the empty) $\mathrm{Id}_X(x,y)$, when $x$ isn't $y$.

edit: To interpret the HoTT $\mathrm{isSet}$, and discard my idea, I must understand what a general $\mathrm{Id}$ in HoTT is and contains, and I must contrast it to $\hom$ in category theory. In fact, I wrote the question as if each type naturally comes with the $\hom$-concept, which isn't true. It's kinda evident to me now, that the general type theory with equality/identity they set up shouldn't be though of like the general category framework. But in the end they are able to do general category theory, so it's the question what they identify with what. A friend of mine says $\mathrm{Cat} = Σ(X:\mathrm{Type}).Σ(\hom : X → X → \mathrm{Type}).(\dots)$ and the question if $\mathrm{Id}$ is "in" $\hom$ is a discussion of saturated categories, precategories??

  • 1
    $\begingroup$ This is a tricky one. I know the structure they're using as the basis for the type theory, and can explain what it means for a Kan complex to be a "set". But I don't know the type theory well enough (still reading the book) to explain it in that context :p $\endgroup$ – Malice Vidrine Dec 5 '13 at 20:15
  • $\begingroup$ Coming back to this question a year later, I can add that the following concepts helped me understand the Identity type in homotopy theory, and are my suggestion to get into if someone comes up with the same question: The general concept of the "principle of equivalence" and all that weak categories pov, groupoids and why thinking of "hom" was too general (all identity proofs are invertible) and lastly to think of Id as proper path space and as "identity" maybe only as one use. $\endgroup$ – Nikolaj-K Nov 10 '14 at 14:12

There are several views of HoTT.

The homotopic interpretation of $p:Id_X(a,b)$ (or as the book writes, of $p:a=b$) is that $p$ is a path in space $X$ with endpoints $a$ and $b$. We do have concatenation of paths, constructing by path induction, so it indeed gives a category-like structure per se.
But! In general, associativity holds only up to the next level of $Id$. So that, if $f:a=b$, $\ g:b=c$, $\ h:c=d$ are paths of type $X$, then we don't have judgemental equality $(fg)h\equiv f(gh)$, but only an 'associator homotopy' between the two paths $\alpha:(fg)h=f(gh)$.

This introduces higher categorical structure, namely (...(arrows between) arrows between) arrows.

Additionally, in this category each arrow is invertible (up to the next level of $Id$), and such a structure is called an infinite dimensional weak grupoid.

A type $X$ is contractible ($-2$-type) if there is a point which is connected to every other point by path: $${\rm isContr}(X):\equiv\ \sum_{x:X}\prod_{y:X}(x=y)$$ Note that $\ {\rm isContr}(X)\simeq (X=1) $ by the univalence axiom.
A type $X$ is proposition ($-1$-type) if all types $x=y$ are contractible. If we assume excluded middle, then this is equivalent to saying that either $X\simeq 1$ (the one point type) or $X\simeq 0$ (the empty type).
A type $X$ is set ($0$-type) if all types $x=y$ are propositions. In the homotopy setting, this corresponds to disjoint union of contractible spaces. (But, e.g. $S^1$ generated by one point and one loop is not set.)

Over the basic grupoid structure (given for any type), one can define categories in HoTT setting, but classic one dimensional categories are not embedded feature in the language, or just partly, let's say. (Indeed, we have $(x=y)\to \hom(x,y)$ for any (pre-)category, using path induction.)

  • $\begingroup$ Thank you for the answer. Is the word "judgemental" in the first paragraph right? What does it mean to "have $(x=y)\to\hom(x,y)$"? Are $x,y$ bounded? Is this an embedding? And are you saying the basic HoTT setting is the types/categories with the $\mathrm{Id}$-types/secondary categories, and we can put other structres and/or depended types into them, next to it. I.e. can I consider a group as category with object $g$, and then $\hom{g,g}=\mathrm{group elements}+\mathrm{Id}$. The last question probably becomes clear later in the book. $\endgroup$ – Nikolaj-K Dec 6 '13 at 8:39
  • 1
    $\begingroup$ 1. Judgmental equality ($\equiv$) is a metanotion, it is mostly used by introducing new letters (e.g. $u:\equiv (a,b):A\times B$ or $f:\equiv \lambda x.x+x$). The arrows that naturally arise in HoTT are the paths $p:x=y$ where $x=y$ stands for the identity type $Id_A(x,y)$ and $x,y:A$ is assumed (in this sense, yes, $x,y$ are 'bounded'). Since a (pre-)category $C$ by definition contains identities $1_x$ for all $x:C$, by path induction, we can extend these cases ${\rm refl}_x:x=x \ \mapsto\ 1_x$ altogether to mappings $(x=y)\to \hom(x,y)$. $\endgroup$ – Berci Dec 7 '13 at 23:32
  • $\begingroup$ If the type $C$ is set, then, it is an 'embedding', but one has to be careful because the meaning of $=$ became a bit sensitive. Please read the book at least for the basic terms. homotopytypetheory.org/book $\endgroup$ – Berci Dec 7 '13 at 23:34
  • $\begingroup$ Yeah, just forgot that "judgemental" is used alternatively to "definitional" and so thought you might mean the other one, namely "propositional". $\endgroup$ – Nikolaj-K Dec 8 '13 at 15:31
  • 1
    $\begingroup$ Why in the world don't we have $(fg)h≡f(gh)$? Surely they're the same in precisely one way. $\endgroup$ – goblin Apr 6 '14 at 10:13

I new to this stuff and so I don't grant of the correctness of what follows.

Before addressing your principal question let me insert some material to explain to context in which we have to work.

Homotopy type theory is just an intensional dependent type theory where semantics take place in $(\infty,1)$-categories, i.e. in context for homotopy theory.

The idea is that in HoTT the types should be interpreted as space of a nice category of spaces (for instance $\mathbf{SSet}$) instead of sets.

Since it's a dependent type theory we can define the concept of category in its language, just as a term of special type. Basically a category amounts to:

  • a type of object $\mathbf C$;

  • a dependent type $\hom_{\mathbf{C}} \colon \mathbf C \times \mathbf C \to \mathbf{Type}$;

  • some terms: $${c} \colon \prod_{x,y,z \in \mathbf C}\left(\hom_{\mathbf C}(y,z) \rightarrow \left(\hom_{\mathbf C}(x,y) \rightarrow \hom_{\mathbf C}(x,z)\right)\right)$$(a composition operation) $$\text{id} \colon \prod_{x \in \mathbf C} \hom(x,x)$$ (identity operation) $$a \colon \prod_{x,y,z,w \in \mathbf C} c_{x,z,w} \circ (1_{\hom(z,w)} \times c_{x,y,z})=c_{x,y,w} \circ (1_{\hom(z,w)}\times c_{x,y,z}) $$ (an associativity witness) $$\text{l} \colon \prod_{x,y} c \circ (\text{id}_{y},1_{\hom(x,y)}) = 1_{\hom(x,y)}$$ $$r \colon \prod_{x,y} c \circ (1_{\hom(x,y)},\text{id}_x) = 1_{\hom(x,y)}$$ (witness for left and right identity).

The models of this structure in the semantic $(\infty,1)$-category are internal categories object and they are called precategories.

Categories are pre-categories aren't just types but they are structured types.

In homotopy type theory you can build very easily a lot of categories, namely for every type $X$ there's a category which has

  • the type $X$ as type of objects;
  • the identity type $\text{Id} \colon X \times X \to \mathbf{Type}$ as $\hom_{X}$ dependent type (for morphisms)
  • some terms which play the roles of composition, identity and witness of associativity and left and right identity.

From the semantic point of view since $X$ is interpreted as a space and the identity type $\text{Id}$ is interpreted as the space of paths in $X$ this category associated with the space $X$ is nothing more than the fundamental groupoid of $X$. This can be proved from the rule for identity types.

That said if I'm still right the various axioms of HoTT should imply that every $\infty$-groupoid (i.e. an internal category in which all the morphisms are invertible) is the fundamental groupoid of some space.

Now back to the main problem on the definition of identity types.

Sets should be those types (or spaces) which are contractible, i.e. whose fundamental groupoids is a discrete one.
This property is expressed in type theory by requiring $$\mathbf{isSet}(X)\colon =\prod_{x,y \colon X} \prod_{p,q \colon \text{Id}_X(x,y)} \text{Id}_{\text{Id}_X}(p,q)$$ that means that all parallel paths (the morphisms of the fundamental groupoids) are (homotopically) equal.

Your request is a stronger one: you are requiring that for a set to being a type (i.e. a space) such that there are no two terms (points) equals (i.e. connected by a path). This in homotopic semantics can be rephrased as requiring that all path components should be singletons and that's not an homotopic property: for instance $\mathbb R$ is homotopy equivalent to the pointed space $\{\bullet\}$ and so it has one path component, nonetheless it doesn't have just one point but infinite many.

Now one final remarks you interpretation of $\hom_X$ above seems wrong: a type is not a category (a category is given by the structure described above). So it doesn't make sense to talk about $\hom_X$ unless your considering the fundamental groupoid associated to the type $X$, in which case $\hom_X=\text{Id}$ by definition.

Hope this helps.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.