module comb where infixr 50 _⟶_ data Ty : Set where ι : Ty _⟶_ : Ty -> Ty -> Ty data Tm : Ty -> Set where K : {σ τ : Ty} -> Tm (σ ⟶ τ ⟶ σ) S : {σ τ ρ : Ty} -> Tm ((σ ⟶ τ ⟶ ρ) ⟶ (σ ⟶ τ) ⟶ σ ⟶ ρ) _$_ : {σ τ : Ty} -> Tm (σ ⟶ τ) -> Tm σ -> Tm τ data Nf : Ty -> Set where Kⁿ : {σ τ : Ty} -> Nf (σ ⟶ τ ⟶ σ) Kⁿ¹ : {σ τ : Ty} -> Nf σ -> Nf (τ ⟶ σ) Sⁿ : {σ τ ρ : Ty} -> Nf ((σ ⟶ τ ⟶ ρ) ⟶ (σ ⟶ τ) ⟶ σ ⟶ ρ) Sⁿ¹ : {σ τ ρ : Ty} -> Nf (σ ⟶ τ ⟶ ρ) -> Nf ((σ ⟶ τ) ⟶ σ ⟶ ρ) Sⁿ² : {σ τ ρ : Ty} -> Nf (σ ⟶ τ ⟶ ρ) -> Nf (σ ⟶ τ) -> Nf (σ ⟶ ρ) _$$_ : {σ τ : Ty} -> Nf (σ ⟶ τ) -> Nf σ -> Nf τ Kⁿ $$ x = Kⁿ¹ x Kⁿ¹ x $$ y = x Sⁿ $$ x = Sⁿ¹ x Sⁿ¹ x $$ y = Sⁿ² x y Sⁿ² x y $$ z = (x $$ z) $$ (y $$ z) nf : {σ : Ty} -> Tm σ -> Nf σ nf K = Kⁿ nf S = Sⁿ nf (t $ u) = nf t $$ nf u data _$ⁿ_⇓_ : {σ τ : Ty} -> Nf (σ ⟶ τ) -> Nf σ -> Nf τ -> Set where rKⁿ : {σ τ : Ty} -> {x : Nf σ} -> Kⁿ {σ} {τ} $ⁿ x ⇓ Kⁿ¹ x rKⁿ¹ : {σ τ : Ty} -> {x : Nf σ} -> {y : Nf τ} -> Kⁿ¹ x $ⁿ y ⇓ x rSⁿ : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> Sⁿ $ⁿ x ⇓ Sⁿ¹ x rSⁿ¹ : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> {y : Nf (σ ⟶ τ)} -> Sⁿ¹ x $ⁿ y ⇓ Sⁿ² x y rSⁿ² : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> {y : Nf (σ ⟶ τ)} -> {z : Nf σ} -> {u : Nf (τ ⟶ ρ)} -> x $ⁿ z ⇓ u -> {v : Nf τ} -> y $ⁿ z ⇓ v -> {w : Nf ρ} -> u $ⁿ v ⇓ w -> Sⁿ² x y $ⁿ z ⇓ w data _⇓_ : {σ : Ty} -> Tm σ -> Nf σ -> Set where rK : {σ τ : Ty} -> K {σ} {τ} ⇓ Kⁿ rS : {σ τ ρ : Ty} -> S {σ} {τ} {ρ} ⇓ Sⁿ r$ : {σ τ : Ty} -> {t : Tm (σ ⟶ τ)} -> {f : Nf (σ ⟶ τ)} -> t ⇓ f -> {u : Tm σ} -> {a : Nf σ} -> u ⇓ a -> {v : Nf τ} -> f $ⁿ a ⇓ v -> t $ u ⇓ v data _==_ {A : Set}(a : A) : {B : Set} -> (b : B) -> Set where refl : a == a data Σ {A : Set}(B : A -> Set) : Set where sig : (a : A) -> (b : B a) -> Σ B σ₀ : {A : Set} -> {B : A -> Set} -> Σ B -> A σ₀ (sig x _) = x σ₁ : {A : Set} -> {B : A -> Set} -> (s : Σ B) -> B (σ₀ s) σ₁ (sig _ y) = y _$$⁼_&_ : {σ τ : Ty} -> (f : Nf (σ ⟶ τ)) -> (a : Nf σ) -> {n : Nf τ} -> f $ⁿ a ⇓ n -> Σ \(n' : Nf τ) -> n' == n Kⁿ $$⁼ x & rKⁿ = sig (Kⁿ¹ x) refl Kⁿ¹ x $$⁼ y & rKⁿ¹ = sig x refl Sⁿ $$⁼ x & rSⁿ = sig (Sⁿ¹ x) refl Sⁿ¹ x $$⁼ y & rSⁿ¹ = sig (Sⁿ² x y) refl Sⁿ² x y $$⁼ z & (rSⁿ² p q r) with x $$⁼ z & p | y $$⁼ z & q Sⁿ² x y $$⁼ z & (rSⁿ² p q r) | sig u refl | sig v refl with u $$⁼ v & r Sⁿ² x y $$⁼ z & (rSⁿ² p q r) | sig u refl | sig v refl | sig w refl = sig w refl nf⁼ : {σ : Ty} -> (t : Tm σ) -> {n : Nf σ} -> t ⇓ n -> Σ \(n' : Nf σ) -> n' == n nf⁼ K rK = sig Kⁿ refl nf⁼ S rS = sig Sⁿ refl nf⁼ (t $ u) (r$ p q r) with nf⁼ t p | nf⁼ u q nf⁼ (t $ u) (r$ p q r) | sig f refl | sig a refl with f $$⁼ a & r nf⁼ (t $ u) (r$ p q r) | sig f refl | sig a refl | sig v refl = sig v refl proof : {σ : Ty} -> (t : Tm σ) -> Σ \(n : Nf σ) -> t ⇓ n proof = {! !} nf⇓ : {σ : Ty} -> Tm σ -> Nf σ nf⇓ t = σ₀ (nf⁼ t (σ₁ (proof t)))