Is a type uniquely determined by its equivalence relation?

by Aleksey Nogin
2001-2002

In this PRL seminar I will discuss the "mystery of T//(E1 & E2) vs. ((T//E1) intersect (T/E2))." For these two types we can prove that they have the same membership and equality relations, but we cannot prove their (extentional) equality. I will attempt to explain why this is the case and will present a new rule that can be used to fix this problem
Slides

Is a type uniquely determined by its equivalence relation?

by Aleksey Nogin 2001-2002

by Aleksey Nogin
2001-2002