Exponentials in a left-exact reflective subcategory (source code)

= Exponentials in a left-exact reflective subcategory

For a <left-exact reflective subcategory> of a <Cartesian closed category>, an ambient exponential $B^A$ is already fixed by the reflector when $A,B$ are fixed. Indeed maps into $B^A$ transpose to maps from $X\times A$ into $B$, and reflection gives $L(X\times A)\cong LX\times A$. Precomposition with the reflection unit is therefore bijective for maps into $B^A$, characterizing a fixed object.