cedille-cast-04.ced

module cedille-cast-04.

NatF ◂ ★ ➔ ★ = λ R: ★. ∀ X: ★. X ➔ (R ➔ X ➔ X) ➔ X.

zero-1 ◂ ∀ R: ★. NatF ·R = Λ R. Λ X. λ z. λ s. z.

zero-2 ◂ ∀ R: ★. NatF ·(NatF ·R) = Λ R. Λ X. λ z. λ s. z.

one-1 ◂ ∀ R: ★. NatF ·(NatF ·R)
  = Λ R. Λ X. λ z. λ s. s (zero-1 ·R) z.

one-2 ◂ ∀ R: ★. NatF ·(NatF· (NatF ·R))
  = Λ R. Λ X. λ z. λ s. s (zero-2 ·R) z.

eq-zero ◂ { zero-1 ≃ zero-2 } = β.
eq-one ◂ { one-1 ≃ one-2 } = β.

-- import cedille-cast-03.
import core.cast.
-- a <= b  ==>  f a <= f b
Monotonic ◂ (★ ➔ ★) ➔ ★
  = λ F: ★ ➔ ★. ∀ X: ★. ∀ Y: ★. Cast ·X ·Y ➔ Cast ·(F ·X) ·(F ·Y).

-- zamknięte <==> ∀ a. fa <= a
F-Closed ◂ (★ ➔ ★) ➔ ★ ➔ ★
  = λ F: ★ ➔ ★. λ X: ★. Cast ·(F ·X) ·X.

Fix ◂ (★ ➔ ★) ➔ ★
  = λ F: ★ ➔ ★. ∀ X: ★. F-Closed ·F ·X ➾ X.

-- ежэли a ест f-замкнеътэ, то fix f <= a.
castFix ◂ ∀ F: ★ ➔ ★. ∀ A: ★. F-Closed ·F ·A ➾ Cast ·(Fix ·F) ·A
  = Λ F. Λ A. Λ fc. intrCast ·(Fix ·F) ·A -(λ fix. fix ·A -fc) -(λ a. β).

-- тэраз теъжка чэъсть
castInFix ◂ ∀ F: ★ ➔ ★. Monotonic ·F ➾ Cast ·(F ·(Fix·F)) ·(Fix ·F)
  = Λ F. Λ mono.
    [ f ◂ F ·(Fix·F) ➔ Fix ·F
      = λ ffix.  Λ X. Λ fc.  elimCast ·(F ·X) ·X -fc (elimCast ·(F ·(Fix ·F)) ·(F ·X) -(mono (castFix -fc)) ffix) ]
    - intrCast ·(F ·(Fix ·F)) ·(Fix ·F) -f -(λ _ . β).

castOutFix ◂ ∀ F: ★ ➔ ★. Monotonic ·F ➾ Cast ·(Fix ·F) ·(F ·(Fix·F))
  = Λ F. Λ mono.
    [ f ◂ Fix ·F ➔ F ·(Fix ·F)
      = λ fix. fix -(mono (castInFix -mono)) ]
    - intrCast ·(Fix ·F) ·(F ·(Fix ·F))  -f  -(λ _. β).

-- ∀ F : ★ ➔ ★ . Monotonic ·F ➾ F ·(Fix ·F) ➔ Fix ·F
inFix = Λ F: ★ ➔ ★. Λ mono: Monotonic ·F. elimCast -(castInFix -mono).
-- ∀ F : ★ ➔ ★ . Monotonic ·F ➾ Fix ·F ➔ F ·(Fix ·F)
outFix = Λ F: ★ ➔ ★. Λ mono: Monotonic ·F. elimCast -(castOutFix -mono).

fixEquil1 ◂ ∀ F: ★ ➔ ★. ∀ X: Fix ·F. { outFix X ≃ X } = Λ _. Λ _. β.
fixEquil2 ◂ ∀ F: ★ ➔ ★. ∀ X: F ·(Fix ·F). { inFix X ≃ X } = Λ _. Λ _. β.

fixEquilA ◂ ∀ F: ★ ➔ ★. ∀ X: Fix ·F. { outFix X ≃ inFix X} = Λ _. Λ _. β.
fixEquilB ◂ ∀ F: ★ ➔ ★. ∀ X: F ·(Fix ·F). { inFix X ≃ outFix X} = Λ _. Λ _. β.