search

rzk-lang / sHoTT

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

Uniqueness of adjunction data #131

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

This essentially proves that given a functor u : B -> A from a Rezk type to a Segal type, the question of whether u admits a left adjoint is a proposition.

Following RS 11.23 the strategy is to prove that the type of pairs (fa, ηa) defining a transposition equivalence hom B fa b -> hom A a (u b) is a proposition.

Thus pull request stops with a proof identifying two such pairs (fa, ηa) = (fa', ηa'). To finish I need a proof that is-equiv is a property so I'll wait for @floverity to finish with issues #56.

I added a few auxiliary functions along the way, in particular reversed versions of various complicated paths, which I called rev-name-of-original-path. I noticed in at least one instance in the library we've denoted this by name-of-original-path' so let me know if that is preferred.

emilyriehl commented 1 year ago

I'm a little rusty with formalization so feel free to take time reviewing this. In the meanwhile, I'll help with some of the open PRs!

emilyriehl commented 1 year ago

About to board a plane again. I'm going to work on switching the code over to the new style guide in progress.

emilyriehl commented 1 year ago

This and #132 are now ready for review.

emilyriehl commented 1 year ago

Good point @fizruk. Once I've actually completed of the proof of the theorem (waiting on some open issues to be finished first) I'll submit another PR with better commenting. But I'll merge this version now.