module lam where

data s = a

listCategory (A: U) (o: listObject A): U = undefined

histo (A:U) (F: U -> U) (X: functor F) (f: F (cofree F A) -> A) (z: fix F): A
  = extract A F ((cata (cofree F A) F X (\(x: F (cofree F A)) ->
    CoFree (Fix (CoBindF (f x) ((X.1 (cofree F A) (fix (cofreeF F A)) (uncofree A F) x)))))) z) where
  extract (A: U) (F: U -> U): cofree F A -> A = split
    | CoFree f -> unpack_fix f where
  unpack_fix: fix (cofreeF F A) -> A = split
    | Fix f -> unpack_cofree f where
  unpack_cofree: cofreeF F A (fix (cofreeF F A)) -> A = split
    | CoBindF a -> a

futu (A: U) (F: U -> U) (X: functor F) (f: A -> F (free F A)) (a: A): fix F
  = Fix (X.1 (free F A) (fix F) (\(z: free F A) -> w z) (f a)) where
  w: free F A -> fix F = split
    | Free x -> unpack x where
  unpack_free: freeF F A (fix (freeF F A)) -> fix F = split
    | ReturnF x -> futu A F X f x
    | BindF g -> Fix (X.1 (fix (freeF F A)) (fix F) (\(x: fix (freeF F A)) -> w (Free x)) g) where
  unpack: fix (freeF F A) -> fix F = split
    | Fix x -> unpack_free x

chrono (A B: U) (F: U -> U) (X: functor F)
       (f: F (cofree F B) -> B)
       (g: A -> F (free F A))
       (a: A): B = histo B F X f (futu A F X g a)

listAlg (A : U) : U
    = (X: U)
    * (nil: X)
    * (cons: A -> X -> X)
    * Unit

listMor (A: U) (x1 x2: listAlg A) : U
    = (map: x1.1 -> x2.1)
    * (mapNil: Path x2.1 (map (x1.2.1)) (x2.2.1))
    * (mapCons: (a:A) (x: x1.1) -> Path x2.1 (map (x1.2.2.1 a x)) (x2.2.2.1 a (map x)))
    * Unit

listObject (A: U) : U
    = (point: (x: listAlg A) -> x.1)
    * (map: (x1 x2: listAlg A)
            (m: listMor A x1 x2) ->
            Path x2.1 (m.1 (point x1)) (point x2))
    * Unit