search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

left version of ind-path #46

Closed TashiWalde closed 1 year ago

emilyriehl commented 1 year ago

Sorry to be so slow to review this. This seems like a useful function to have. I'm just wondering about the name. Any suggestions @fredrik-bakke @jonweinb @fizruk? Maybe ind-rev-path?

Currently we have a reference to codomain-based-path-spaces (which is a terrible name). Perhaps someone could suggest a better name for that too. We might also consider moving that into the contractible types file and proving it using this new reversed path induction.

fredrik-bakke commented 1 year ago

Your suggestion is good. And if I inferred the meaning of codomain-based-path-space correctly, then it could perhaps similarly be renamed to rev-based-path?

emilyriehl commented 1 year ago

@fredrik-bakke it's worse than that: it's meant to be Σ (x : A), x = a for some a : A.

fredrik-bakke commented 1 year ago

So given an a, it is the type of paths that are reversely based at a? Still seems to me the name rev-based-path fits. I guess actually based-rev-path is better, as it plays a similar role to ind-rev-path as based-path then should to ind-path.

TashiWalde commented 1 year ago

I don't like ind-rev-path because it implies that it has something to do with the rev function. Of course, the implementation uses it, but the induction principle itself is more of a primitive.

In order of my (mild) personal preference, here are some alternatives: ind-path-end, ind-op-path (suggested by Emily), ind-path-codomain

emilyriehl commented 1 year ago

So given an a, it is the type of paths that are reversely based at a? Still seems to me the name rev-based-path fits. I guess actually based-rev-path is better, as it plays a similar role to ind-rev-path as based-path then should to ind-path.

@fredrik-bakke it's worse than that: it's meant to be Σ (x : A), x = a for some a : A.

emilyriehl commented 1 year ago

I don't like ind-rev-path because it implies that it has something to do with the rev function. Of course, the implementation uses it, but the induction principle itself is more of a primitive.

In order of my (mild) personal preference, here are some alternatives: ind-path-end, ind-op-path (suggested by Emily), ind-path-codomain

As @TashiWalde knows, there is a sense, though, that the definition of ind-path-l is given by applying ind-path to the reverse path to a type family defined by reversing paths --- modulo a transport because the construction just described defines a term of type C x (rev rev p) rather than C x p.

Neither of us have strong feelings about this so it would be great if someone else could weigh in @fizruk @fredrik-bakke @jonweinb.

fredrik-bakke commented 1 year ago

I don't like ind-rev-path because it implies that it has something to do with the rev function. Of course, the implementation uses it, but the induction principle itself is more of a primitive.

In order of my (mild) personal preference, here are some alternatives: ind-path-end, ind-op-path (suggested by Emily), ind-path-codomain

That's a reasonable point and I think all your suggestions can work. One issue with ind-path-end and ind-path-codomain, is that they suggest that the original definition ind-path should be renamed to ind-path-start or ind-path-domain as well. Another point, the op in ind-op-path has more of a categorical connotation, and we would perhaps want to reserve it for if rzk gets an op involution. Lastly, although ind-rev-path can be considered a more primitive notion, it still has a clear relation to ind-path via the rev function, so I am still not against it.

TashiWalde commented 1 year ago

I don't like ind-rev-path because it implies that it has something to do with the rev function. Of course, the implementation uses it, but the induction principle itself is more of a primitive. In order of my (mild) personal preference, here are some alternatives: ind-path-end, ind-op-path (suggested by Emily), ind-path-codomain

That's a reasonable point and I think all your suggestions can work. One issue with ind-path-end and ind-path-codomain, is that they suggest that the original definition ind-path should be renamed to ind-path-start or ind-path-domain as well. Another point, the op in ind-op-path has more of a categorical connotation, and we would perhaps want to reserve it for if rzk gets an op involution. Lastly, although ind-rev-path can be considered a more primitive notion, it still has a clear relation to ind-path via the rev function, so I am still not against it.

I think my ideal solution would be to have ind-path-start and ind-path-end as primitives, to maintain the symmetry. Then one could add ind-path as a shorthand for ind-path-start (and for backwards compatibility).

I agree with reserving op for the categorical concept.

emilyriehl commented 1 year ago

Okay let's do ind-path-start (redefined from idJ and redefined to ind-path) and ind-path-end. We can change this later if we grow to dislike it. @TashiWalde while you're making the name change would you mind also renaming "codomain based path spaces" to "End based path spaces" (or similar; anything is better than the original name). Then I'll merge this.

TashiWalde commented 1 year ago

Okay let's do ind-path-start (redefined from idJ and redefined to ind-path) and ind-path-end. We can change this later if we grow to dislike it. @TashiWalde while you're making the name change would you mind also renaming "codomain based path spaces" to "End based path spaces" (or similar; anything is better than the original name). Then I'll merge this.

Do you mean the ones in "04-extension-types"?