Skip to main content

All Questions

2 votes
0 answers
102 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 ...
Veky's user avatar
  • 121