Positive inductive-recursive definitions
From MaRDI portal
Publication:2848936
Recommendations
Cited in
(12)- Finitary higher inductive types in the groupoid model
- A categorical semantics for inductive-inductive definitions
- Small induction recursion
- Constructing a universe for the setoid model
- scientific article; zbMATH DE number 7168146 (Why is no real title available?)
- Indexed induction-recursion
- Indexed containers
- Fibred data types
- Positive inductive-recursive definitions
- Variations on inductive-recursive definitions
- Impredicative encodings of inductive-inductive data in Cedille
- For Finitary Induction-Induction, Induction is Enough
This page was built for publication: Positive inductive-recursive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848936)