Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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…
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
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) }$?
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”?
1 to 9 of 9