NestIdCoe.ced

import Nat.
import List.
import Vec.
import VecL.
import IdCoe.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

mapCL ◂ ∀ A : ★ . ∀ B : ★ .  Π f : A ➔ B . List · A ➔ ListC · B
  = Λ A . Λ B . λ f . λ xs .
  Λ X . λ cN . λ cC . xs.1.1 · X cN (λ x . cC (f x)) .

mapPL ◂ ∀ A : ★ . ∀ B : ★ .
  Π f : A ➔ B .
  Π xs : List · A .
  ListP · B (mapCL · A · B f xs)
  = Λ A . Λ B . λ f . λ xs .
  Λ X . Λ P . Λ cN . Λ cC . λ pN . λ pC .
  xs.1.2 · X · P
    -cN -(λ x . cC (f x))
    pN (Λ xsC . λ x . pC -xsC (f x)) .

mapRL ◂ ∀ A : ★ . ∀ B : ★ .  Π f : A ➔ B . Π xs : List · A .
  ListR · B (mapCL · A · B f xs)
  = Λ A . Λ B . λ f . λ xs . elimList · A xs ·
  (λ xs : List · A . ListR · B (mapCL · A · B f xs))
  β
  (Λ xs . λ x . λ ih . ρ+ ih - β) . 

mapL ◂ ∀ A : ★ . ∀ B : ★ .  Π f : A ➔ B . List · A ➔ List · B
  = Λ A . Λ B . λ f . λ xs . mkList · B
  [ mapCL · A · B f xs
  , mapPL · A · B f xs ]
  -(mapRL · A · B f xs) .

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

v2l-v2l ◂ ∀ A : ★ . ∀ n : Nat . ∀ m : Nat .
  Vec · (Vec · A n) m ➔ List · (List · A)
  = Λ A . Λ n . Λ m . λ xss .
  mapL · (Vec · A n) · (List · A) (v2l · A -n)
    (v2l · (Vec · A n) -m xss) .

v2u-v2l ◂ ∀ A : ★ . ∀ n : Nat . ∀ m : Nat .
  Vec · (Vec · A n) m ➔ List · (VecL · A n)
  = Λ A . Λ n . Λ m . λ xss .
  (mapL · (Vec · A n) · (VecL · A n) (v2u · A -n)
    (v2l · (Vec · A n) -m xss)) .

u2l-l2l ◂ ∀ A : ★ . ∀ n : Nat .
  List · (VecL · A n) ➔ List · (List · A)
  = Λ A . Λ n . λ xss .
  mapL · (VecL · A n) · (List · A) (u2l · A -n) xss .

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%