# these are built in to the language
# true <- λ x, y: x
# false <- λ x, y: y

𝐼 <- λ x: x

𝑌 <- λ f: (λ x: f (x x)) (λ x: f (x x))