# nLab codependent type theory

Contents

foundations

## Set theory

set theory

• fundamentals of set theory
• presentations of set theory
• structuralism in set theory
• class-set theory

# Contents

## Idea

When attempting to define coinductive types, there is an obstacle to the complete dualization of the usual rules for inductive types in dependent type theory, including dualizing the induction principle to a “coinduction principle”. For this some form of “codependent types” would be needed. In the context of homotopy type theory, Ahrens, Capriotti, and Spadotti write:

The universal property defining (internal) coinductive types in HoTT is dual to the one defining (internal) inductive types. One might hence assume that their existence is equivalent to a set of type-theoretic rules dual (in a suitable sense) to those given for external W-types… However, the rules for external W-types cannot be dualized in a naïve way, due to some asymmetry of HoTT related to dependent types as maps into a “type of types” (a universe) (ACS15)

Codependent type theory is a hypothetical type theory where one should be able to define codependent types, and coinductive types with a coinduction principle.

## References

• Benedikt Ahrens, Paolo Capriotti, Régis Spadotti, Non-wellfounded trees in Homotopy Type Theory, (arXiv:1504.02949)

Created on June 3, 2022 at 15:39:22. See the history of this page for a list of all contributions to it.