Let $f\colon A\to B$ be a function.
-
Functionality I. The assignment $f\mapsto f^{-1}$ defines a function
\[ \webleft (-\webright )^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (B\webright ),\mathcal{P}\webleft (A\webright )\webright ). \]
-
Functionality II. The assignment $f\mapsto f^{-1}$ defines a function
\[ \webleft (-\webright )^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )\webright ). \]
-
Interaction With Identities. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
\[ \text{id}^{-1}_{A}=\text{id}_{\mathcal{P}\webleft (A\webright )}. \]
-
Interaction With Composition. For each pair of composable functions $f\colon A\to B$ and $g\colon B\to C$, we have
