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