Dependent Type Theory as Related to the Bourbaki Notions of Structure and Isomorphism

TL;DR

This paper extends dependent type theory by incorporating a Bourbaki-inspired approach to isomorphism, enabling straightforward, set-theoretic transport and constructive proofs of isomorphic substitution.

Contribution

It generalizes Bourbaki's structure and isomorphism definitions to dependent types, providing a clear set-theoretic framework and constructive validation of isomorphic substitution.

Findings

Defines isomorphism via set-theoretic bijections and transport conditions.

Provides a constructive proof for substitution of isomorphic structures.

Differentiates from groupoid and homotopy type theories by explicit set-theoretic transport.

Abstract

This paper develops a version of dependent type theory in which isomorphism is handled through a direct generalization of the 1939 definitions of Bourbaki. More specifically we generalize the Bourbaki definition of structure from simple type signatures to dependent type signatures. Both the original Bourbaki notion of isomorphism and its generalization given here define an isomorphism between two structures $N$ and $N'$ to consist of bijections between their sorts that transport the structure of $N$ to the structure of $N'$. Here transport is defined by commutativity conditions stated with set-theoretic equality. This differs from the dependent type theoretic treatments of isomorphism given in the groupoid model and homotopy type theory where no analogously straightforward set-theoretic definition of transport is specified. The straightforward definition of transport also leads to a straightforward constructive proof (constructive content) for the validity of the substitution of isomorphics -- something that is difficult in the groupoid model or homotopy type theory.