natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
strong axioms
further
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.
Created on June 3, 2022 at 11:39:22. See the history of this page for a list of all contributions to it.