[FOM] A question about isomorphic structures

[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