related golfing work

Stream: Infinity-Cosmos

[Emily Riehl]

Finally, the is some related work in progress on quasi-categories that can currently be found in various mathlib branches. This includes:

• definitions and lemmas by @Joseph Tooby-Smith on the homotopy relation for 1-simplices in a quasi-category
• a proof by @Johan Commelin that nerves of 1-categories are quasi-categories; update, now in Mathlib thanks to @Nick Ward
• a construction by @Mario Carneiro and myself of the reflective nerve adjunction now as PR #16784, depending on #16779, #16780, #16781, #16782, #16783; update all except the final #16784 are in mathlib, thanks to the heroic efforts of @Joël Riou
• These constructions/definitions/proofs could all use streamlining and golfing by expert Lean users. So if someone wants to get their hands dirty right away, please help us clean up our code.