Zulip Chat Archive

Stream: general

Topic: Generating isomorphisms?


view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:47):

I have some definition definition foo (X : Type) : Type := blah

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:47):

If I have two types X and Y plus isomorphisms f:X\to Y and g:Y\to X (i.e. the composites both ways are the identity functions)

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:48):

can I deduce that foo X is isomorphic to foo Y? Does this even make sense?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:53):

an isomorphism version of eq.subst?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:54):

Or does this have to somehow be proved on a case by case basis?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:55):

Mathematicians are so happy to identify objects which are canonically isomorphic and I find this much more of a struggle in Lean.

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 17:57):

can I deduce that foo X is isomorphic to foo Y?

Yes, if you define isomorphic as "there exist isomorphisms f and g such that ...". :smile:

This notion of isomorphism does not allow you to substitute isomorphic structures in arbitrary contexts, though.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:58):

yes this is absolutely how I want to define isomorphic.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:58):

How do I construct the map foo X -> foo Y?

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 17:59):

The axiom of univalence would allow you to lift isomorphisms to equality, then you can substitute in arbitrary contexts.

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 17:59):

Ooops, sorry missed the foo part.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:59):

Oh great :-)

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:59):

I don't see any reason why I should be able to get a map foo X -> foo Y just given a map X -> Y

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:59):

but can I use the inverse somehow?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 18:00):

Or is what I want not even true?

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 18:00):

So yeah, univalence is the axiomatic principle that would allow you to do that (in HoTT).

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 18:00):

In Lean, you need to prove it yourself for each instance, such as foo here.

view this post on Zulip Mario Carneiro (Mar 04 2018 at 18:00):

It's definitely not true in general; for example if foo X was X = nat

view this post on Zulip Mario Carneiro (Mar 04 2018 at 18:01):

(not true without univalence that is)

view this post on Zulip Mario Carneiro (Mar 04 2018 at 18:03):

@Gabriel Ebner do you know if you can get a contradiction in classical lean from X ~= Y -> X = Y?

view this post on Zulip Gabriel Ebner (Mar 04 2018 at 18:20):

This is an interesting question. I think it is strictly weaker than univalence because it is not an isomorphism. It looks inconsistent, but I don't immediately see how to derive a contradiction from it.


Last updated: May 11 2021 at 13:22 UTC