module A201602.AltArtemovS4 where

open import Relation.Binary.PropositionalEquality using (_≑_ ; refl)

import A201602.AltArtemov as πœ†βˆž
import A201602.S4 as S4


forget : πœ†βˆž.Ty β†’ S4.Ty
forget πœ†βˆž.βŠ₯      = S4.βŠ₯
forget (A πœ†βˆž.βŠƒ B) = forget A S4.βŠƒ forget B
forget (A πœ†βˆž.∧ B) = forget A S4.∧ forget B
forget (A πœ†βˆž.∨ B) = forget A S4.∨ forget B
forget (x πœ†βˆž.∢ A) = S4.β–‘ forget A


πœ†βˆž-drop : βˆ€{A} β†’ πœ†βˆž.⊩ A β†’ πœ†βˆž.Ty
πœ†βˆž-drop {A} _ = A

S4-drop : βˆ€{A} β†’ S4.⊩ A β†’ S4.Ty
S4-drop {A} _ = A


tI : βˆ€{A} β†’ forget (πœ†βˆž-drop (πœ†βˆž.PL.I {A})) ≑ S4-drop (S4.SKICombinators.I {forget A})
tI = refl

tIΒ² : βˆ€{A} β†’ forget (πœ†βˆž-drop (πœ†βˆž.PLExamples.IΒ² {A})) ≑ S4-drop (S4.SKICombinators.IΒ² {forget A})
tIΒ² = refl


tK : βˆ€{A B} β†’ forget (πœ†βˆž-drop (πœ†βˆž.PL.K {A} {B})) ≑ S4-drop (S4.SKICombinators.K {forget A} {forget B})
tK = refl

tKΒ² : βˆ€{A B} β†’ forget (πœ†βˆž-drop (πœ†βˆž.PLExamples.KΒ² {A} {B})) ≑ S4-drop (S4.SKICombinators.KΒ² {forget A} {forget B})
tKΒ² = refl


tS : βˆ€{A B C} β†’ forget (πœ†βˆž-drop (πœ†βˆž.PL.S {A} {B} {C})) ≑ S4-drop (S4.SKICombinators.S {forget A} {forget B} {forget C})
tS = refl

tSΒ² : βˆ€{A B C} β†’ forget (πœ†βˆž-drop (πœ†βˆž.PLExamples.SΒ² {A} {B} {C})) ≑ S4-drop (S4.SKICombinators.SΒ² {forget A} {forget B} {forget C})
tSΒ² = refl


tE13 : βˆ€{A B} β†’ forget (πœ†βˆž-drop (πœ†βˆž.Example1.E13 {A} {B})) ≑ S4-drop (S4.Example1.E13 {forget A} {forget B})
tE13 = refl

tE14 : βˆ€{x y A B} β†’ forget (πœ†βˆž-drop (πœ†βˆž.Example1.E14 {x} {y} {A} {B})) ≑ S4-drop (S4.Example1.E14 {forget A} {forget B})
tE14 = refl