class CA (A : Type u_1) extends HasDot A : Type u_1

A (total) combinatory structure on a set A.

• dot : A → A → A
• K : A
• S : A
• eq_K : ∀ {a b : A}, CA.K ⬝ a ⬝ b = a
• eq_S : ∀ {a b c : A}, CA.S ⬝ a ⬝ b ⬝ c = a ⬝ c ⬝ (b ⬝ c)

def Part.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Part α) (v : Part β) : Part γ

Missing from Part

Equations

• Part.map₂ f u v = { Dom := u ⇓ ∧ v ⇓ , get := fun (p : u ⇓ ∧ v ⇓ ) => f (u.get ⋯) (v.get ⋯) }

@[simp]

theorem Part.map₂_get {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Part α) (v : Part β) (p : u ⇓ ∧ v ⇓ ) : (Part.map₂ f u v).get p = f (u.get ⋯) (v.get ⋯)

@[simp]

theorem Part.map₂_Dom {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Part α) (v : Part β) : ((Part.map₂ f u v) ⇓ ) = (u ⇓ ∧ v ⇓ )

@[simp]

theorem Part.eq_map₂_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : Part.map₂ f (Part.some a) (Part.some b) = Part.some (f a b)

@[reducible]

instance CA.partialApp {A : Type} [d : HasDot A] : PartialApplication A

A total application induces a partial application

Equations

• CA.partialApp = { app := Part.map₂ HasDot.dot }

theorem CA.eq_app {A : Type} [HasDot A] {u v : Part A} (hu : u ⇓ ) (hv : v ⇓ ) : u ⬝ v = Part.some (u.get hu ⬝ v.get hv)

instance CA.isPCA {A : Type} [CA A] : PCA A

A combinatory algebra is a PCA

Equations

• CA.isPCA = PCA.mk (Part.some CA.K) (Part.some CA.S) True.intro ⋯ True.intro ⋯ ⋯ ⋯ ⋯