Skip to content

Instantly share code, notes, and snippets.

@AndrasKovacs
AndrasKovacs / HIIRT.md
Last active March 25, 2024 08:20
Higher induction-induction-recursion

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.