xx Set\mathbf{Set}
xˉx\bar x \in x
xˉ ⁣:1Setx\bar x_♯\colon 1_\mathbf{Set} → x
 ⁣:xˉ\colon * \mapsto \bar x

f ⁣:xyf\colon x→y
(f(xˉ))=(xˉ;;f)=xˉ;f(f(\bar x))_♯ = (\bar x;;f)_♯ = \bar x_♯ ;f