2014/07/27 by David McAllester, McAllester, David · 1 voice
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies #cs.LO
paper · pdf · doi:10.48550/arxiv.1407.7274
openalex publication_date 2014/07/27 · arxiv published 2014/07/27 · arxiv updated 2018/01/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We provide a treatment of isomorphism within a set-theoretic formulation of dependent type theory. Type expressions are assigned their natural set-theoretic compositional meaning. Types are divided into small and large types --- sets and proper classes respectively. Each proper class, such as "group" or "topological space", has an associated notion of isomorphism in correspondence with standard definitions. Isomorphism is handled by definging a groupoid structure on the space of all definable values. The values are simultaneously objects (oids) and morphism --- they are "morphoids". Soundness can then be proved for simple and natural inference rules deriving isomorphisms and for the substitution of isomorphics.