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.

Filter by
Sorted by
Tagged with
10 votes
0 answers
164 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 ...
7 votes
1 answer
161 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 ...