cedille-cast-07-08.ced

import core.cast.

module cedille-cast-07-08 (F: ★ ➔ ★) (mono : CastMap ·F).

--
Monotinic : (★ ➔ ★) ➔ ★ = λ F: ★ ➔ ★. CastMap ·F.
--

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

AlgM : ★ ➔ ★ = λ X: ★. ∀ R: ★. (R ➔ X) ➔ F ·R ➔ X.
FixM : ★ = ∀ X: ★. AlgM ·X ➔ X.
foldM : ∀ X: ★. AlgM ·X ➔ FixM ➔ X = Λ X. λ alg. λ d. d alg.

inM : F ·FixM ➔ FixM = λ ds. Λ X. λ alg. alg (foldM alg) ds.
--EOF alg

--outM : FixM ➔ F ·FixM
--  = λ d. d (Λ R. λ rec. λ ds. ●).

PrfAlgM : Π X: ★. (X ➔ ★) ➔ (F ·X ➔ X) ➔ ★
  = λ X: ★. λ P: X ➔ ★. λ in: F ·X ➔ X.
    ∀ R : ★. ∀ c : Cast ·R ·X. Π ih: (Π r: R. P (elimCast -c r)).
    Π rs: F ·R. P (in (elimCast ·(F ·R) ·(F ·X) -(mono -c) rs)).

InductiveM : FixM ➔ ★
  = λ x: FixM. ∀ P: FixM ➔ ★. PrfAlgM ·FixM ·P inM ➔ P x.

FixIndM : ★ = ι x : FixM. InductiveM x.

castFixIndM2FixM : Cast ·FixIndM ·FixM
  = intrCast ·FixIndM ·FixM -(λ x. x.1) -(λ _. β).

inIndM1 : F ·FixIndM ➔ FixM
  = λ ds. inM (elimCast ·(F ·FixIndM) ·(F ·FixM) -(mono -castFixIndM2FixM) ds).

_ : {inIndM1 ≃ inM} = β.

inIndM2 : Π ds: F ·FixIndM. InductiveM (inIndM1 ds)
  = λ ds. Λ P. λ alg. alg ·FixIndM -castFixIndM2FixM (λ d. d.2 ·P alg) ds.

_ : {inIndM2 ≃ inM} = β.

inIndM : F ·FixIndM ➔ FixIndM
  = λ ds. [ inIndM1 ds , inIndM2 ds ].

--inductionM : ∀ P: FixIndM ➔ ★. PrfAlgM ·FixIndM ·P inIndM ➔ Π d : FixIndM. P d
-- = Λ P. λ alg. λ d. d.2 ·P ●.

-- Cedille Cast #8 --

toFixM : Cast ·FixIndM ·FixM = castFixIndM2FixM.
IndM : ★ = FixIndM.

import data.sigma.

Lift : (IndM ➔ ★) ➔ FixM ➔ ★
  = λ P: IndM ➔ ★. λ x: FixM.
    Sigma ·IndM ·(λ y: IndM. Sigma ·({y ≃ x}) ·(λ eq: {y ≃ x}. P (φ eq - y {|x|}))).

IhPlus : Π R: ★. Cast ·R ·FixM ➔ (IndM ➔ ★) ➔ ★
  = λ R: ★. λ c : Cast ·R ·FixM. λ P: IndM ➔ ★.
    Π r: R. Lift ·P (elimCast -c r).

{-
r : R, c : Cast ·R ·FixM
proj1 (ih r) : indM
proj1 (proj2 (ih r)) : {proj1 (ih r) ≃ r}
-}

castIhPlus : ∀ R: ★. ∀ c: Cast ·R ·FixM. ∀ P : IndM ➔ ★. IhPlus ·R c ·P  ➔ Cast ·R ·IndM
  = Λ R. Λ c. Λ P. λ ih.
    intrCast -(λ r. fst (ih r)) -(λ r. fst (snd (ih r))).

prfIhPlus : ∀ R: ★. ∀ c: Cast ·R ·FixM. ∀ P: IndM ➔ ★. Π ih: IhPlus ·R c ·P. Π r : R.
            P (elimCast -(castIhPlus -c ih) r)
  = Λ R. Λ c. Λ P. λ ih. λ r. snd (snd (ih r)).

convAlg : ∀ P: IndM ➔ ★. PrfAlgM ·IndM ·P inIndM ➔ PrfAlgM ·FixM ·(Lift ·P) inM
  = Λ P. λ alg. Λ R. Λ c. λ ih. λ xs.
    [ c' = castIhPlus -c ih ]
  - [ xs' = elimCast -(mono -c') xs ]
  - [ ih' = prfIhPlus -c ih ]
  - sigma (inIndM xs') (sigma β (alg ·R -c' ih' xs)).

inductionM : ∀ P: FixIndM ➔ ★. PrfAlgM ·FixIndM ·P inIndM ➔ Π d : FixIndM. P d
  = Λ P. λ alg. λ d. snd (snd (d.2 (convAlg alg))).

outM : IndM ➔ F ·IndM
  = inductionM ·(λ _: IndM. F ·IndM) (Λ R. Λ c. λ _. λ xs. elimCast -(mono -c) xs).