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.
4
questions
2
votes
0
answers
114
views
An unexpectedly hard question about type equality (of sigma types)
Suppose you have A: Type and P Q: A -> Prop such that {x : A | P x} = {x : A | Q x}. Can ...
- 121
2
votes
0
answers
48
views
A module signature is silently changed when it is imported. Its `eq_dec` lemma has its `=` operator changed to `eq` and no longer works
This following works as I'd expect it to. But if I place the TypeDef_S signature in another file then the apply typeDef.eq_dec. ...
- 75
10
votes
0
answers
181
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 ...
- 4,087
7
votes
1
answer
181
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 ...
- 6,346