  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.
