# Zulip Chat Archive

## Stream: maths

### Topic: is_homotopic_to

#### Kevin Buzzard (Aug 09 2018 at 10:39):

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 (Aug 09 2018 at 13:14):

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

itself.

#### Reid Barton (Aug 09 2018 at 13:15):

What you don't want to do is define `is_homotopic_to`

without `path_homotopy`

#### Mario Carneiro (Aug 09 2018 at 13:24):

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

#### Mario Carneiro (Aug 09 2018 at 13:24):

so the homotopy itself won't be in the structure

#### Luca Gerolla (Aug 09 2018 at 13:36):

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 (Aug 09 2018 at 13:37):

I think Kevin wants a `trunc`

instead of a `nonempty`

#### Kenny Lau (Aug 09 2018 at 13:37):

but this will be to HoTT-like

#### Mario Carneiro (Aug 09 2018 at 13:37):

To take a quotient you need a Prop

#### Mario Carneiro (Aug 09 2018 at 13:38):

Consider the way `cardinal`

is defined - it is a quotient over the relation `nonempty (A ≃ B)`

#### Luca Gerolla (Aug 09 2018 at 14:07):

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

Last updated: May 14 2021 at 19:21 UTC