Kan extensions for quasicategories

• We only need Kan extensions along inclusions of subquasicategories [HTT 4.3.2]. Lurie introduces the more general notion of p-Kan extension. For us D’ will be the terminal quasicategory and p the unique map.

• We will need HTT Prop 4.3.2.8, and Cor. 4.3.2.16

• We need the example of Kan extensions along the Yoneda embedding into presheaves of spaces. Specifically we need Thm 5.1.5.6 (which uses Lma 5.1.5.5)

https://docs.google.com/document/d/1llPzCxlhWSucYymRenInm861KK-QVJxQS0MeEQZdjE8/edit