[FOM] A question about isomorphic structures

[David McAllester]

On Mon, Mar 28, 2016 at 9:56 PM, Bruno Bentzen <b.bentzen at hotmail.com>
wrote:
>
> Till Mossakowski wrote:
>
> > I have a question to the HoTT community about the consequences of the
> > univalence axiom:
> > If I understand HoTT and univalence correctly: whenever you have two
> > types A and B, and there is some (definable) bijection between them,
> > then already A=B.

​Perhaps I can take this opportunity to contrast MorTT and HoTT with
respect to the equation A=B above.

Both systems distinguish isomorphism (propositional equality) from absolute
equality (judgemental equality).  In MorTT the semantics is constructed
from a model of set theory and all values are elements of that model.
Absolute equality simply means set-theoretic equality in the underlying
model of set theory.

In both systems propositional equality (isomorphism) is typed and we should
really write A =_type B.   Both systems have an infinite sequence of
universes. In MorTT this is written as type_0, type_1, type_2 ... ​where we
have type_i : type_j for i < j.  So A=B is really

 A =_{type_i} B

 for some i.

MorTT uses "SET" as an alternate notation for type_0.  This is different
from HoTT.   MorTT also uses the term "CLASS" as an alternate notion for
type_1.
We then have GROUP : CLASS and SET : CLASS stating that GROUP and SET are
types in type_1.  type_i for i > 2 does not come up much but we have
CATEGORY : type_2.

In MorTT all types S in type_0 (all "sets" S) are discrete in the sense
that S-isomorphism (the relation =_S) is the same as absolute equality.
This is different from HoTT but seems to be in correspondence with standard
mathematical language. For class-level types such as SET and GROUP we can
have distinct but isomorphic things. In MorTT, for two sets A and B we have
A =_SET B if and only if sets A and B have the same cardinality.  This is
the degenerate case of a carrier set with no additional structure. For two
groups G and H we have that G =_GROUP H is the standard isomorphism
relation on groups. In MorTT the notion of "same cardinality" between sets
does not require a computable bijection.  Computability does not even make
sense for sets of abstract points. The notion of set in MorTT is different
from the notion of set in HoTT --- in HoTT types must be "squashed" into
sets and this squashing occurs at all levels of type.

It is also worth noting that in MorTT the same value can have more than one
type.  An Abelian group is also a group.  Two permutation groups can be
group-isomorphic but not permutation-group-isomorphic.

Various additional point-by-point comparisons between MorTT and HoTT are
given in the last three pages of the introduction to my manuscript.

David
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160330/3e3863da/attachment.html>