Modular approach to formalization of the quotient types

by Aleksey Nogin
2000-2001

I will finish presenting the modular approach to formalization of the quotient types. I will show how the modular theory I presented in the last two seminars can be used to formalize the notion of collection types. If I have time, I will present the rule that states that a type is uniquely determined by its equivalence relation. I will also show how this new rule can be used to establish Z2 intersect Z3 = Z6 and I will also explain why this equality can not be proven in a theory without the new rule.

Modular approach to formalization of the quotient types

by Aleksey Nogin 2000-2001

by Aleksey Nogin
2000-2001