I have added (here) the analogous discussion reflected in a type universe, with a reference to Theorem 4.8.3 in the HoTT book.

Then I added (here) a joint lead-in paragraph for this and the previous discussion

]]>Thanks.

In addition, I have taken the liberty of adding whitespace and parenthesis to the formulas (here) in order to optically resolve the syntax tree.

]]>one could -> one can

Anonymous

]]>I see, I was misled by expecting to read something else.

Do you mind if we write “one can” or “there is” instead of “one could”?

]]>no, I mean syntactically, not relative to a universe.

Anonymous

]]>you wrote (here):

Given a family of types, $x:A \vdash B(x)$, one could construct a family of elements $z:\sum_{x:A} B(x) \vdash \pi_1(z):A$ via the rules for dependent sum types. Conversely, given a family of elements $x:A \vdash f(x):B$ one could construct a family of types $y:B \vdash \sum_{x:A} f(x) =_B y$ as the family of fiber types of $x:A \vdash f(x):B$.

$\,$

This seems confusing to the point of being notationally wrong.

I guess you mean to talk about these two functions:

$\array{ \underset{ Y \,\colon\, Type }{\sum} \big( Y \to X \big) &\longrightarrow& \underset{x \,\colon\, X}{\prod} Type \\ (Y,f) &\mapsto& \big( x \colon X \;\vdash\; fib_x(f) \big) }$and

$\array{ \underset{x \,\colon\, X}{\prod} Type &\longrightarrow& \underset{ Y \,\colon\, Type }{\sum} \big( Y \to X \big) \\ \big( x \,\colon\, X \;\;\vdash\;\; E(x) \big) &\mapsto& \Big( \pi_1 \,\colon\, \big( \underset{x \,:\, X}{\sum} E(x) \big) \to X \Big) }$?

]]>added a section on the relation between families of types, families of elements, and functions, and how that results in the relation between type theory and category theory inside of dependent type theory itself.

Anonymous

]]>made “type family” (requested elsewhere) redirect here

]]>the entries *dependent type* and *indexed set* did not know of each other.

I have now cross-linked them minimally in their “Related entries”-sections. But this would deserve to be expanded on for exposition…

]]>