[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Sequents and entailment rather than implication and universal quantification. coherent mathematics \section{Monomorphism and isomorphism classifiers} Maps $X \to [A, B]_\mathrm{iso}$ correspond to isomorphisms $(A \times X) \cong (B \times X)$ in the slice $C/X$ category: redirected to nlab