# Rules for mutual inductive/coinductive types

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?

• 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). Mar 6 at 23:09
• What is "$\omega$-completion"? Mar 6 at 23:14
• 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). Mar 6 at 23:26
• 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). Mar 23 at 1:30