Involution

Set

context $X$ … set
definiendum $ f\in \mathrm{it}(X,X) $
postulate $ f:X\to X $
postulate $ f\circ f=\mathrm{id_X} $


Subset of

Unary operation