When we say "let X be a type", we are not moving to the classifying topos
"S[X]" (unless we wish to claim that "Let X be a type; then X^X = 1+X holds" is
valid).

This works better than 'bend right', which can sometimes create weird
fish-shaped adjunction pictures.