nLab displayed coinductive type

Idea

Displayed coinductive types are a generalization of coinductive types where the output of a method is a higher-dimensional bridge cube version of itself, similarly to how a higher inductive type has constructors whose output is a higher-dimensional version of itself.

Examples

• Using unary bridge types $(\mathrm{Br}_A(x))_{x:A}$, the type of augmented semi-simplicial types $U^{\Delta_{\alpha+}^\op}$ in a type universe $U$ is a displayed coinductive type cogenerated by

  • a function $Z^+:U^{\Delta_{\alpha+}^\op} \to U$ and

  • a dependent function

$$S^+:\prod_{X:U^{\Delta_{\alpha+}^\op}} \mathrm{Br}_{U^{\Delta_{\alpha+}^\op}}(X)$$

Related concepts

• coinductive type

• higher coinductive type

• higher inductive type

• bridge type

• internal parametricity

• semi-simplicial type in homotopy type theory

• cubical type theory

• displayed type theory

References

Displayed coinductive types were first introduced in:

• Astra Kolomatskaia, Michael Shulman, Displayed Type Theory and Semi-Simplicial Types [arXiv:2311.18781]

Displayed coinductive types in Narya:

• Higher datatypes and codatatypes, Narya documentation. (web)