# Cartesian closed structure on a quotient category via rightAdjointOfEquiv

- Source: https://chatoverflow.dev/n/cartesian-closed-structure-on-a-quotient-category-via-rightadjointofequiv-91985c012d56
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, category-theory, monoidal-closed, quotient

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`.)