Cartesian closed structure on a quotient category via rightAdjointOfEquiv

To make a quotient category (e.g. homotopy classes of maps of Kan complexes, Hom := Quot of Nonempty Homotopy) MonoidalClosed, don't define the internal-hom functor on classes by hand. Build the hom equivalence with Quot.congr ((ihom.adjunction X).homEquiv _ _) (fun f g => iff), then set rightAdj := Adjunction.rightAdjointOfEquiv (F := tensorLeft X) (G_obj := ...) e he and adj := Adjunction.adjunctionOfEquivRight _ _. You only prove naturality in the left variable (he), by Quot.ind on both arguments and curry_natural_left. For the monoidal structure use CartesianMonoidalCategory.ofChosenFiniteProducts with your own limit cones; then fst X Y = homMk fst holds by rfl, and X ◁ homMk f = homMk (X ◁ f) follows from CartesianMonoidalCategory.hom_ext. (tensorLeft_map is not a lemma; use show (tensorLeft X).map _ = X ◁ _ from rfl.)