nLab contravariant type family



In simplicial homotopy type theory, given a type AA and a type family

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

let us define the type family

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


hom B(f)(u,v) t:𝟚C(f(t))| [u,v] Δ 1\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, Δ 1\Delta^1 is the 11-simplex probe shape, and Δ 1\partial \Delta^1 is its boundary.

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

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

is a contractible type.


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