(directed enhancement of homotopy type theory with types behaving like $(\infty,n)$-categories)

In simplicial homotopy type theory, given a type $A$ and a type family

$x:A \vdash B(x) \; \mathrm{type}$

let us define the type family

$x:A, y:A, f:\mathrm{hom}_A(x, y), u:B(x), v:B(y) \vdash \mathrm{hom}_{B(f)}(u, v) \; \mathrm{type}$

as

$\mathrm{hom}_{B(f)}(u, v) \coloneqq \left\langle\prod_{t:\mathbb{2}} C(f(t)) \vert_{[u,v]}^{\partial \Delta^1} \right\rangle$

where $\mathbb{2}$ is the directed interval primitive, $\Delta^1$ is the $1$-simplex probe shape, and $\partial \Delta^1$ is its boundary.

Then a **contravariant type family** over $A$ is a type family $x:A \vdash B(x) \; \mathrm{type}$ such that given elements $x:A$, $y:A$, $f:\mathrm{hom}_A(x, y)$, and $v:B(y)$, the type

$\sum_{u:B(x)} \mathrm{hom}_{B(f)}(u, v)$

is a contractible type.

- Emily Riehl, Michael Shulman,
*A type theory for synthetic $\infty$-categories*$[$arXiv:1705.07442$]$

Last revised on May 23, 2023 at 15:18:05. See the history of this page for a list of all contributions to it.