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

CoRR（2021）

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.

MoreTranslated text

Key words

bourbaki notions,type,isomorphism,theory

AI Read Science

Must-Reading Tree

Example

Generate MRT to find the research sequence of this paper

Chat Paper

Summary is being generated by the instructions you defined