Simplicial sets & cartesian closed

Stream: general

[Dean Young]

I've been delving into what Mathlib has on simplicial sets with two different kinds of lifting conditions (the one for quasi categories and the Kan lifting conditions) Is there anywhere a proof that these categories are cartesian closed?

Specifically, X × Y and [X,Y] ought to satisfy the respective lifting condition when X and Y do.

[Adam Topaz]

Do we have a definition of quasi categories already? That’s news to me. Pinging @Jack McKoen since he’s interested in this.