nLab null type

Definition

In dependent type theory, given a type $A$, a type $T$ is a $A$-null type if the function

$$\lambda x:T.\lambda y:A.x:T \to (A \to T)$$

is an equivalence of types.

More generally, given a type $A$ and a type family $B(a)$ indexed by $a:A$, a type $T$ is a $B$-null type if the function

$$\lambda x:T.\lambda y:B(a).x:T \to (B(a) \to T)$$

is an equivalence of types for all $a:A$.

 Examples

• Every type is $A$-null if the type $A$ is a contractible type.

• Every contractible type is $\emptyset$-null.

• Every mere proposition is boolean-null.

• Every h-set is $S^1$-null.

 Related concepts

• localization of a type

• axiom of cohesion

• local object

References

• Egbert Rijke, Mike Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, 16 1 (2020) [arXiv:1706.07526, episciences:6015, doi:10.23638/LMCS-16(1:2)2020]

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)