All Questions
Tagged with inductive-type universe
3
questions
1
vote
0
answers
69
views
Heterogeneous lists, large indices
Recently I had cause to define a type of heterogeneous lists in Lean, and wrote
...
- 111
1
vote
0
answers
179
views
Descriptions of heterogenous datatypes
When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples):
<...
- 547
6
votes
1
answer
253
views
Parameterized Datatypes in a Universe à la Tarski?
I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types?
For context, I'm trying ...
- 921