The general goal of this project is to formalize basic theory of quasi-categories. Most of the work is based on Kerodon.
The current goal is 0066: the internal hom between quasi-categories is again a quasi-category. This has been reduced to 0077 and 007F.
Remaining tasks:
0077:
- the collection of monomorphisms of simplicial sets is stable under transfinite composition
- the maps
$B(k - 1) \hookrightarrow B(k)$ belong to$T'$ (requires simplicial subset and skeleton API)
007F:
- the pushout-product of
$\partial\Delta^m \hookrightarrow \Delta^m$ with$\Lambda^2_1 \hookrightarrow \Delta^2$ is inner anodyne for$0 \le m$ (requires simplicial subset API)
01BR:
- the class of inner anodyne morphisms is generated by inner horn inclusions (should be done when #20245 is merged)