[FOM] A question about isomorphic structures
David McAllester
mcallester at ttic.edu
Mon Mar 28 08:53:49 EDT 2016
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>
More information about the FOM
mailing list