Quotient types | a modular approach

Abstract. In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen set of primitive operations. This modular formalization of quotient types turns out to be much easier to use andfree of many limitations of the traditional monolithic formalization. To illustrate the advantages of the new approach, we show how the type of collections (that is known to be very hardto formalize using traditional quotient types) can be naturally formalizedusing the new primitives. We also show how modularity allows us to reuse one of the new primitives to simplify andenhance the rules for the set types.