cedille-cast-05.ced

module cedille-cast-05.

import core.top.
import data.sigma.
import data.sum.


NatF : ★ ➔ ★ = λ R: ★. Sum ·Top ·R. -- jenostka = 0; R = succ
ListF : ★ ➔ ★ ➔ ★ =  λ A : ★. λ R: ★. Pair ·Top ·R. -- jedn = nil; (a,r) = cons

Alg : (★ ➔ ★) ➔ ★ ➔ ★ = λ F: ★ ➔ ★. λ X: ★. F ·X ➔ X.

import data.bool.

isEvenAlg : Alg ·NatF ·Bool = λ n. case n (λ _. tt) not.

Fix : (★ ➔ ★) ➔ ★ = λ F: ★ ➔ ★. ∀ X: ★. Alg ·F ·X ➔ X.


fold :  ∀ F: ★ ➔ ★. ∀ X: ★. Alg ·F ·X ➔ Fix ·F ➔ X
  = Λ F. Λ X. λ alg. λ fix. fix alg.

isEven : Fix ·NatF ➔ Bool = fold isEvenAlg.

AlgM : (★ ➔ ★) ➔ ★ ➔ ★
  = λ F: ★ ➔ ★. λ X: ★. ∀ R: ★. (R ➔ X) ➔ F ·R ➔ X.

FixM : (★ ➔ ★) ➔ ★ = λ F: ★ ➔ ★. ∀ X: ★. AlgM ·F ·X ➔ X.

isEvenAlgM : AlgM ·NatF ·Bool
  = Λ R. λ rec. λ n. case n (λ _. tt) (λ n' . not (rec n')).

foldM :  ∀ F: ★ ➔ ★. ∀ X: ★. AlgM ·F ·X ➔ FixM ·F ➔ X
  = Λ F. Λ X. λ alg. λ fix. fix alg.

isEvenM : FixM ·NatF ➔ Bool = foldM isEvenAlgM.

in : ∀ F: ★ ➔ ★. F ·(FixM ·F) ➔ FixM ·F
  = Λ F. λ d. Λ X . λ alg. alg ·(FixM ·F {-Jaki typ zapodać za R -}) (foldM alg) d.

Functor : (★ ➔ ★) ➔ ★ = λ F: ★ ➔ ★. ∀ A: ★. ∀ B: ★. (A ➔ B) ➔ F ·A ➔ F ·B.

out: ∀ F: ★ ➔ ★. Functor ·F ➔ FixM ·F ➔ F ·(FixM ·F)
  = Λ F. λ fmap. λ d. d ·(F ·(FixM ·F))
      (Λ R. λ rec. λ fr. fmap ·R ·(FixM ·F) (λ r. in  (rec r)) fr).