All Questions
Tagged with equality type-theory
6
questions
0
votes
0
answers
119
views
MLTT with first-order reasoning and equality-reasoning information preservation
Terms in Extensional MLTT don't contain equality-reasoning information (implicit transports), effectively meaning data is lost, which is bad. But at the same time, higher-order reasoning (reasoning ...
- 345
3
votes
1
answer
160
views
Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?
The short version:
Is this statement correct? If it is, is it provable in Coq?
...
- 33
4
votes
1
answer
99
views
General method for disproving possibility of judgemental equality
There is a slick definition of categories (as a record type with eta-equality) such that taking the opposite category twice results in the original one judgementally. Similar tricks seems to exist for ...
- 4,025
2
votes
1
answer
105
views
Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?
Suppose we work inside MLTT with equality reflection (extensional MLTT).
Assume I postulate existence of Streams as final co-algebra for the suitable functor.
Is that enough to prove the bisimulation ...
- 345
2
votes
1
answer
245
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:
“algorithmic” definitional ...
- 9,150
16
votes
2
answers
404
views
What are the upsides and downsides of typed vs untyped conversion?
What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?
Background
Generally speaking, in dependent type ...
- 394