[FOM] A question about isomorphic structures

[Bruno Bentzen]

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.


The univalence axiom implies that if two types are equivalent, they are equal.

Since a bijection need not be an equivalence, this is not the case in general.

However, this holds for types that "behave like sets".


This is an interesting question, because it leads indirectly to Avron's point:


Arnon Avron wrote:

> By the way,  is "the carrier of a structure A" not
> a *set*? If not - what is it? And if yes - does not it means that

> we still need some set theory for the alleged "alternative foundations"? .


Yes, we have "sets" in HoTT. But they are defined in terms of types that behave like so.

Categorically, they are just discrete grupoids, which are given by a collection of objects

and identity morphisms as the only higher morphisms. In terms of HoTT, we say that

for any two terms x and y of A, every term of x=y is equal (up to homotopy).


There is something that is worth making explicit here, namely, the fact that we are

treating equality as a type (since it contains terms). Indeed, 'equality' actually means two

different things in HoTT - and all other flavors of (intensional) Martin-Loef type theory.

There are two notions of equality, *judgmental equality* and *propositional equality*.

Roughly, the former is a judgment meaning that two objects are equal by definition.

Deciding judgmental equality is just a matter of unfolding the definitions.

The latter is a *type* of identifications of two objects. One thing many people like about

HoTT is that it brings a nice interpretation to the once very obscure notion of propositional

equality: it is just meant to grasp the idea of two things being equal up to homotopy.


Specifically, the univalence axiom implies that isomorphic structures  are propositionally equal.

It does not trivialize anything to the point that they are completely indistinguishable.

To use Frege's terminology, it suggests that isomorphic things have the same reference:

but in general they need not have the same sense sense, since it does not imply

judgmental equality. This is perhaps a formal embodiment of the view  "isomorphic

systems differ only notationally" that Corcoran attributed to some mathematicians.


Arnon Avron:

> I cannot quite understand the claim that
> in mathematics "isomorphic" means  "equal". Showing that two
> *different* structures are actually isomorphic is sometimes
> a non-trivial mathematical theorem. It would not make much sense
> to prove such theorems if the two structures are completely identified.


Avron is certainly correct that it does not make sense to prove that two *propositionally* different

structures are isomorphic. On the other hand, to show that two *judgementally*

different structures are isomorphic need not be a trivial matter.

This should be the natural HoTT way to think of such theorems -

Leading HoTTists, please correct me if I am wrong.


Bruno Bentzen

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160329/cb48c640/attachment-0001.html>