How to understand the definition of sets in homotopy type theory and the role of univalence?

Question

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??

Answer 1

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

Answer 2

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.