Cartesian closure for a finite-limit-preserving comonad

ID: cartesian-closure-for-a-finite-limit-preserving-comonad

Let be a Cartesian comonad on a Cartesian category that is Cartesian closed. Its forgetful functor creates finite limits. For coalgebras and , set , . Transpose to , and put . Their cofree coalgebra transposes have a coalgebra equalizer. A map into this equalizer is exactly a map respecting coalgebra structures, so it is the required exponential object. No subobject classifier on the base category is needed.

New to topics? Read the docs here!