Paper detail

Isomorphism Revisited

Isomorphism is central to the structure of mathematics and has been formalized in various ways within dependent type theory. All previous treatments have done this by replacing quantification over sets with quantification over groupoids of some form --- categories in which every morphism is an isomorphism. Quantification over sets is replaced by quantification over standard groupoids in the groupoid model, by quantification over infinity groupoid in Homotopy type theory, and by quantification over morphoids in the morphoid model. Here we give a treatment of isomorphism based on the intuitive notion of sets as collections without internal structure. Quantification over sets remains as quantification over sets. Isomorphism and groupoid structure then emerge from simple but subtle syntactic restrictions on set-theoretic language. This approach more fully unifies the classical ZFC foundations with a rigorous treatments of isomorphism, symmetry, canonicality, functors, and natural transformations. This is all done without reference to category theory.