All Questions
Tagged with soft-question type-theory
4
questions
16
votes
3
answers
308
views
Counterexamples in Type Theory
The title pretty much covers it. I'm wondering if someone is maintaining a list of counterexamples in type theory. I'm aware of Counterexamples in Type Systems, which I think is very nice, but I guess ...
- 368
4
votes
1
answer
252
views
How can you represent a dependent type visually?
So, obviously for a term $t$ of type $T$, I would represent it as:
T
+-----------+
| |
| t |
| |
+-----------+
That is a node ...
4
votes
2
answers
153
views
Pragmatic encodings of inductive inductive types
What's the most pragmatic encoding for inductive-inductive types such as for a universe of types?
In pseudo Coq syntax.
...
- 2,868
16
votes
1
answer
386
views
Why should you "never resort to polymorphism when initiality would do"?
In the concluding statement of "universe hierarchies", Conor McBride calls it
[...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do.
...
- 1,035