Core Concepts
Coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, and inductive predicates are equivalent to inductively generated basic covers in dependent type theory.
Abstract
The paper presents a topological interpretation of inductive and coinductive definitions in dependent type theory.
Key highlights:
- Inductive and coinductive predicates are defined in the Minimalist Foundation, a two-level dependent type theory.
- Inductive predicates are shown to be equivalent to inductively generated basic covers, while coinductive predicates are equivalent to coinductively generated positivity relations.
- The authors establish the compatibility of these (co)inductive constructions with the Minimalist Foundation and its interpretation in Martin-Löf type theory.
- Inductive and coinductive predicates are related to other (co)inductive schemes in Martin-Löf type theory, such as W-types and M-types.
- The paper formalizes all proofs in the Agda proof assistant.