vamo brincar um cadinho com funções, currying, aplicação parcial e pattern matching

bool

true = λx.λy.x
false = λx.λy.y

not = λx.x false true
and = λx.λy.x y false
or = λx.λy.x true y

ifthenelse = λp.λa.λb.p a b

bool.agda

module bool where

data 𝔹 : Set where
  true : 𝔹
  false : 𝔹

¬_ : 𝔹 → 𝔹
¬ true = false
¬ false = true

_^_ : 𝔹 → 𝔹 → 𝔹
true ^ b = b
false ^ b = false

_∨_ : 𝔹 → 𝔹 → 𝔹
true ∨ b = true
false ∨ b = b

if_then_else : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if true then t else f = t
if false then t else f = f

bool.py

def true(a):
    return lambda b: a

def false(a):
   return lambda b: b

def NOT(a):
    return a(false)(true)

def AND(a):
    return lambda b: a(b)(false)

def OR(a):
    return lambda b: a(true)(b)

def IF_THEN_ELSE(a):
    return lambda b: lambda c: a(b)(c)

def tests():
    print("!true === false")
    print(NOT(true))

    print("\n!false === true")
    print(NOT(false))


    print("\n\ntrue AND true === true")
    print(AND(true)(true))

    print("\ntrue AND false === false")
    print(AND(true)(false))

    print("\nfalse AND true === false")
    print(AND(false)(true))

    print("\nfalse AND false === false")
    print(AND(false)(false))


    print("\n\ntrue OR true === true")
    print(OR(true)(true))

    print("\ntrue OR false === true")
    print(OR(true)(false))

    print("\nfalse OR true === true")
    print(OR(false)(true))

    print("\nfalse OR false === false")
    print(OR(false)(false))


    print("\n\nif true then t else f === t")
    print(IF_THEN_ELSE(true)(1)(2))

    print("\nif false then t else f === f")
    print(IF_THEN_ELSE(false)(1)(2))

tests()

As provas e alguns tipos haha