[FOM] A question about isomorphic structures

[Till Mossakowski]

In ZFC, you prove sets to be equal by proving the two inclusions. If you 
look at actual proofs of equality of two types A and B in HoTT (like 
this one: http://homotopytypetheory.org/2015/01/20/ts1s1-cubically/), 
they are in reality proofs of isomorphism. You have to prove the 
existence of two maps f:A->B and g:B->A, and also that they are inverses 
of each other. From such an isomorphism, by univalence, you get 
equality. I have the feeling that this is more a declarative act. It has 
the convenient consequence that you can omit the isomorphism maps f and 
g when transporting structure from A to B. E.g. when you have h:A->A, by 
A=B you also get h:B->B. However, under the carpet, f and g are still 
there, and h:B->B "in reality" (say, in an appropriate model of HoTT) is 
f . h:A->A . g (where . is composition).

Till Mossakowski


Am 26.03.2016 um 21:59 schrieb Hendrik Boom:
> On Sat, Mar 26, 2016 at 08:01:24PM +0300, Arnon Avron wrote:
>> 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.
>> It is also certainly not true that mathematicians always identify two
>> structures whenever they are isomorphic. indeed, Bruno Bentzen
>> was careful to write: "mathematicians OFTEN identify two structures
>> whenever they are isomorphic", adding the fuzzy word "often" here. So
>> I wonder: does HoTT make this "often" precise and does not the fact
>> that mathematicians do not always make this identification
>> "clearly in conflict with foundational theories such as" HoTT?
> The identification is not made in normal constructive type theory.
>
> However, in HoTT, everything isn't even a topological space;
> everything is a homotopy equivalence class.  So calling things equal
> is pretty natural there.
>
> -- hendrik
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom