# * New modular approach to formalizing complex types in type theory *

## by Aleksey Nogin

2000-2001

I will present a new modular approach to formalizing complex types in type theory, in particular - the quotient type. I will show how the new building blocks that I create for the quotient type can be successfully reused for other purposes, in particular - to formalize Mark's collection types.