11
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 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$
    – Mike Shulman
    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

0

Reset to default

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.