[FOM] A question about isomorphic structures

[David McAllester]

I strongly encourage people to read the first two pages of the introduction
to my manuscript <http://arxiv.org/abs/1407.7274> of morphoid type theory.
The centerpiece of morphoid type theory is a proof of soundness for the
substitution of isomorphics.

Sigma; x:tau |- e[x]:sigma
x is not free in sigma
Sigma |- u =_tau w
------------------------------
Sigma |- e[u] =_sigma e[w]

Here x =_sigma y is read x is sigma-isomorphic to y.  Isomorphism is
defined at every type, most importantly at dependent pair types.  In MorTT
there is no propositions-as-types, path-induction, squashing or higher
order isomorphism.

Isomorphic objects are not substitutable in all contexts.  Consider the
Cauchy sequence representation of the reals.

Sigma |- R:Field
Sigma |- Phi[R]:Bool

Here the statement Phi[R] can reference the Cauchy sequence representation
rather than abstract field structure of R.  In this case we do NOT have
Sigma; F:Field |- Phi[F]:Bool and substitution into Phi[R] is blocked.

Anyway, I do encourage people to read the first two pages of the
introduction.

David
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160328/a1ee6046/attachment-0001.html>