Formalise adjunctions (Section 11 of RS17 paper)

[fizruk]

This should be split into sub-issues.

• Section 11.1 (Notions of adjunction) Adjunctions (notions of adjunctions) #32
  • Definition 11.1 (transposing adjunction)
  • Definition 11.2 (quasi-diagrammatic adjunction)
  • Definition 11.3 (half-adjoint diagrammatic adjunction)
  • Constructions 11.4, 11.5, and unnumbered diagrams right after
  • Definition 11.6 (bi-diagrammatic adjunction)
• Section 11.2 (Adjunctions between Segal types)
  • Definition 11.7 (quasi-transposing adjunction)
  • Theorem 11.8
  • Corollary 11.12
  • Theorem 11.13
  • Theorem 11.14
  • Corollary 11.21
  • Corollary 11.22
• Section 11.3 (Adjunctions between Rezk types)
  • Theorem 11.23

[emilyriehl]

This might be a good collaborative project, since it is so large, and will involve a lot of new definitions, which we should try to name properly, adhering to the conventions of the style guide, which is here:

https://github.com/rzk-lang/sHoTT/blob/main/src/STYLEGUIDE.md

So, for instance, if someone wants to work on this with me (multiple people, one computer, at least until everyone gets the hang of things) let me know.

[emilyriehl]

For those following along at home I'm working on Theorem 11.8.

[emilyriehl]

I'm going to pause my work on Theorem 11.8 because it will help to have section 8.5 finished first :)