Isomorphism within Naive Type Theory

TL;DR

This paper develops a set-theoretic approach to isomorphism in dependent type theory, defining a groupoid structure on definable values to handle isomorphisms systematically.

Contribution

It introduces a novel set-theoretic framework for treating isomorphisms in dependent type theory using morphoids and groupoid structures.

Findings

Defines a set-theoretic semantics for types and isomorphisms.

Establishes sound inference rules for isomorphism handling.

Models isomorphisms as morphoids within a groupoid structure.

Abstract

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.