Questions tagged [intensional-equality]
Intensional equality usually refers to the equality relation encoded by an equality type in an intensional type theory. Equivalently, you may say it's encoded by an equality type that does not satisfy equality reflection.
2
questions
10
votes
0
answers
159
views
What are the practical differences between intensional and extensional type theories?
It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
- 3,688
7
votes
1
answer
147
views
How to state and prove the associativity of append of sized vectors with homogeneous equality?
Append (denoted ++) for sized vectors is obviously associative, i.e. a ++ (b ++ c) = (a ++ b) ++ c for ...
- 5,857