We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Computer Science > Logic in Computer Science

Title: Isomorphism Revisited

Abstract: 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.
Comments: This paper lacks adequate proofs of the claims
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:1912.02885 [cs.LO]
  (or arXiv:1912.02885v2 [cs.LO] for this version)

Submission history

From: David McAllester [view email]
[v1] Thu, 5 Dec 2019 21:33:49 GMT (12kb)
[v2] Tue, 12 May 2020 01:39:23 GMT (0kb,I)

Link back to: arXiv, form interface, contact.