search

rzk-lang / sHoTT

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

Further progress on right orthogonal calculus #112

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

1) Right orthogonal maps are closed under composition and right cancel.

2) Right orthogonal maps are closed under relative products (=pullback).

Point 2 was surprisingly tricky. Maybe there was an easier way to do this. I did this by setting up a theory of relative extension types and generalized relative extension types which might be of independent interest.

The two main steps are:

3) A map is right orthogonal if and only if all its relative extension types are contractible if and only if all its generalized relative extension types are contractible.

4) Each relative extension type of the pulled back map appears as retract of a generalized relative extension type of the original map.

Notes:

TashiWalde commented 1 year ago

@fredrik-bakke I have dismissed (marked as resolved) some of your suggestions which should be addressed in the PR #111 on which this one builds.

fredrik-bakke commented 1 year ago

In case you missed it, there's a single comment left to resolve. After that, this PR seems ready to merge to me.

fredrik-bakke commented 1 year ago

Okay, I've had enough of making all these formatting corrections, and I'm sure you are done with formatting code and seeing my comments as well. I'll write an autoformatting script over the weekend so we can move on to more productive things.

I had a chat with Nikolai before the weekend. He and his student will try to set up basic autoformatting functionality built into the Rzk ecosystem instead, so the autoformatting will have to wait a little.