Epilogue

I’ve had an enquiry for more details on quotients in the new Epigram setup, so I’ll take that as a cue to blog a bit.

First, I’d better sketch some basics about propositions and equality. It’s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible thus far in a decidable type theory. The headlines:

• quotients given by a ‘carrier’ set, equivalence relation
• definitional equality on equivalence classes inherited from carrier on representatives
• propositional equality on equivalence classes is equivalence of representatives
• propositional equality is substitutive

The tabloid headline is STUFF YOUR SETOIDS.
Read the rest of this entry »