Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what the type-theoretic introduction/elimination rules should be for such a family, and as shown in this question their behavior can be kind of unexpected. The implementation, I guess, allows general "matches" and "comatches", with a separate "termination/productivity checker"; but this is not a semantic explanation suitable for, say, finding category-theoretic models.

Has anyone written down an inference-rule presentation of a type theory including mutual or nested inductive/coinductive definitions?

  • 3
    $\begingroup$ I might add that even if there's a more rigorous presentation of what Agda/Coq does, it'd probably also be nice to have something better. A while back it was observed that trying to define ω-completion as a mixed higher-inductive/coinductive definition gets you something contractible. But now I wonder if it's just because you can't write down the right thing in Agda (i.e. you really want uses of the higher constructor to be well-founded, but they aren't in Agda). $\endgroup$
    – Dan Doel
    Mar 6 at 23:09
  • 1
    $\begingroup$ What is "$\omega$-completion"? $\endgroup$ Mar 6 at 23:14
  • 1
    $\begingroup$ I mean the 'partiality monad', which you can model as a HIT/QIT via the free ω-complete partial order on a type. As a mixed definition you try to define the same thing similarly to the coinductive definition of the extended natural numbers. Conceivably it might be better behaved than quotienting a coinductive type after the fact (which I think requires countable choice to be a monad). $\endgroup$
    – Dan Doel
    Mar 6 at 23:26
  • 1
    $\begingroup$ I'm aware of Hening Basold's thesis. And Danielsson and Altenkirch's Mixing Induction and Coinduction has a long list of related work, some of which may have rules (e.g. the work on sized types). $\endgroup$
    – gallais
    Mar 23 at 1:30


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.