Type Theoretic Interpretation of the Final Chain

From cLab
Revision as of 10:23, 14 January 2016 by H.basold (talk | contribs) (Create stub)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

This is a placeholder for the discussion of how to encode coinductive types into MLTT with inductive types and the related problems.