is_homotopic_to

Stream: maths

[Kevin Buzzard]

I just saw this in @Luca Gerolla 's code.

definition is_homotopic_to { x y : β } (f : path x y) ( g : path x y) : Prop := nonempty ( path_homotopy f g)

I feel like is_homotopic_to is an important concept and it sounds like a prop to me, but of course there might well be many homotopies between f and g. Is Luca unwise to use nonempty or is this exactly what he wants? I still feel very unsure about this kind of thing. Given an explicit homotopy from f to g and an explicit homotopy from g to h he will surely want an explicit homotopy from f to h, and of course he proves this, but...I think what I'm saying is that I am confused about both wanting a proposition and wanting to keep track of the homotopy at the same time.

[Reid Barton]

You need both, I think. And here we do have both, since we also have path_homotopy itself.

[Reid Barton]

What you don't want to do is define is_homotopic_to without path_homotopy

[Mario Carneiro]

I think you will want a quotient type over the is_homotopic_to relation

[Mario Carneiro]

so the homotopy itself won't be in the structure

[Luca Gerolla]

So you think this is the appropriate way to define the equivalence relation that I will define the quotient on? When needed to get an actual path_homotopy f g from H : is_homotopic_to f g I use cases ; while to show (for example) is_homotopic_to f g I construct an actual F : path_homotopy f g and feed this with nonempty.intro . Would this be a good way to manage the homotopy binary relation? At first, I just felt I was loosing some information with nonempty in later proofs.

[Kenny Lau]

I think Kevin wants a trunc instead of a nonempty

[Kenny Lau]

but this will be to HoTT-like

[Mario Carneiro]

To take a quotient you need a Prop

[Mario Carneiro]

Consider the way cardinal is defined - it is a quotient over the relation nonempty (A ≃ B)

[Luca Gerolla]

I see.. thank you! I will stick to nonempty