nLab higher coinductive type

Idea

Higher coinductive types are a generalization of coinductive types where the input of a method is a higher-dimensional version of itself, dually to how a higher inductive type has constructors whose output is a higher-dimensional version of itself.

As a result, higher coinductive types typically require context modification rules which replace variables with higher-dimensional cubes (see e.g. here).

Examples

• The amazing right adjoint of a specified type $T$ is a higher coinductive type $1/T$ cogenerated by a 1-dimensional field $\mathrm{root}$ in $T$.

• The fibrancy predicate in higher observational type theory is a higher coinductive type using bridge types cogenerated by

  • two transport functions,

  • two dependent functions which give witness that each element is heterogeneously bridged with its transported version,

  • a witness that heterogeneous bridge types of fibrant types are also fibrant

Related concepts

• coinductive type

• displayed coinductive type

• higher inductive type

• higher observational type theory

References

• Thorsten Altenkirch, Univalence Without an Interval, talk at Homotopy Type Theory and Computing – Classical and Quantum, Center for Quantum and Topological Systems (video)

Higher coinductive types in Narya:

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

• Higher Observational Type Theory, Narya documentation. (web)