ICat.idr

module ICat2

%default total

data Ft       -- functors
  = Var Nat
  | Terminal
  | Prod Ft Ft
  | Exp Ft Ft

-- "Nt output input" -form. natural transformations.
data Nt : Ft -> Ft -> Type where
   Atom : (n:Nat) -> Nt (Var n) (Var n)
   Const : (a:Ft) -> Nt Terminal a
   Pair : Nt a c -> Nt b c -> Nt (Prod a b) c
   Fst  : (a:Ft) -> (b:Ft) -> Nt a (Prod a b)
   Snd  : (a:Ft) -> (b:Ft) -> Nt b (Prod a b)
   Cur  : Nt a (Prod b c) -> Nt (Exp a c) b
   Ap   : (a:Ft) -> (b:Ft) -> Nt a (Prod (Exp a b) b)
   Comp : Nt a b -> Nt b c -> Nt a c

ft2nt : (a:Ft) -> Nt a a
ft2nt (Var k) = Atom k
ft2nt Terminal = Const Terminal
ft2nt (Prod x y) = Pair (Fst x y) (Snd x y)
ft2nt (Exp x y) = Cur (Ap x y)

prod : Nt a b -> Nt c d -> Nt (Prod a c) (Prod b d)
prod {a} {b} {c} {d} f g = Pair (Comp f (Fst b d)) (Comp g (Snd b d))
 
left : Nt a b -> Nt (Prod a c) (Prod b c)
left {a} {b} {c} f = Pair (Comp f (Fst b c)) (Snd b c)
 
right : Nt a b -> Nt (Prod c a) (Prod c b)
right {a} {b} {c} f = Pair (Fst c b) (Comp f (Snd c b))

exp : Nt a b -> Nt c d -> Nt (Exp a d) (Exp b c)
exp {a} {b} {c} {d} f g = Cur (Comp f (Comp (Ap b c) (right g)))

data Cv : Nt a b -> Nt a b -> Type where
  InPairCv : Cv x y -> Cv z w -> Cv (Pair x z) (Pair y w)
  InCurCv : Cv x y -> Cv (Cur x) (Cur y)
  InCompCv : Cv x y -> Cv z w -> Cv (Comp x z) (Comp y w)
  AtomCv : Cv f g -> Cv (Comp (Atom n) f) g
  ConstCv : Cv (Comp (Const k) f {c=c}) (Const c)
  PairCv : Cv (Comp f h) x
        -> Cv (Comp g h) y
        -> Cv (Comp (Pair f g) h) (Pair x y)
  FstCv : Cv f h -> Cv (Comp (Fst a b) (Pair f g)) h
  SndCv : Cv g h -> Cv (Comp (Snd a b) (Pair f g)) h
  CurCv : Cv (Comp f (left g)) x
       -> Cv (Comp (Cur f) g) (Cur x)
  ApCv : Cv (Pair (ft2nt c) g) h
      -> Cv (Comp (Ap a b) (Pair (Cur f) g {c=c})) (Comp f h)

  ReflCv : Cv a a
  AssCv : Cv (Comp (Comp f g) h) (Comp f (Comp g h))
  InvCv  : Cv a b -> Cv b a
  CompCv : Cv a b -> Cv b c -> Cv a c

-- This thing constructs something that resembles a neutral term.
-- A path that tells how to retrieve a value.
data Path : Ft -> Ft -> Type where
  PathId : Path a a
  PathComp : Nt a b -> Path b c -> Path a c
  PathAp : Path (Exp a b) c -> Nt b c -> Path a c
  PathPump : Nt b c -> Path a b -> Path a c

mutual
  path : Path a b -> Nt c a -> Nt c b
  path PathId nt = nt
  path (PathComp x p) nt = Comp nt (path p x)
  path (PathAp p x {a} {b}) nt = (Comp nt (Comp (Ap a b) (Pair (fpath p) x)))
  path (PathPump tail p) nt = Comp nt (pathcomp p tail)

  fpath : Path (Exp a b) c -> Nt (Exp a b) c
  fpath PathId {a} {b} = ft2nt (Exp a b)
  fpath (PathComp x p) = path p x
  fpath (PathAp p x {a=Exp a d} {b}) = (Comp (Ap (Exp a d) b) (Pair (fpath p) x))
  fpath (PathPump tail p) = pathcomp p tail

  pathcomp : Path a b -> Nt b c -> Nt a c
  pathcomp PathId nt = nt
  pathcomp (PathComp x p) nt = Comp x (pathcomp p nt)
  pathcomp (PathAp x y {a} {b}) nt = Comp (Ap a b) (Pair (pathcomp x nt) (Comp y nt))
  pathcomp (PathPump tail p) nt = pathcomp p (Comp tail nt)

varpath : (k:Nat) -> Path (Var k) b -> Nt (Var k) b
varpath k PathId = Atom k
varpath k (PathComp x p) = path p x
varpath k (PathAp p x) = ?teuih_3
varpath k (PathPump tail p) = pathcomp p tail

Trans : Ft -> Ft -> Type
Trans p q = {a:Ft} -> Path a p -> Path a q

ft_sem : Ft -> Ft -> Type
ft_sem p (Var k) = Path (Var k) p
ft_sem p Terminal = ()
ft_sem p (Prod x y) = (ft_sem p x, ft_sem p y)
ft_sem p (Exp x y) = (q:Ft) -> Trans p q -> ft_sem q y -> ft_sem q x

-- Lift a term into a different scope.
tlift : Trans p q -> ft_sem p x -> ft_sem q x
tlift trans term {x = (Var k)} = (trans term)
tlift trans () {x = Terminal} = ()
tlift trans (a, b) {x = (Prod x y)} = (tlift trans a, tlift trans b)
tlift trans func {x = (Exp x y)} = \q, qtrans => func q (qtrans . trans)

ev : (p:Ft) -> Nt a b -> ft_sem p b -> ft_sem p a
ev p (Atom n) arg = arg
ev p (Const b) arg = ()
ev p (Pair x y) arg = (ev p x arg, ev p y arg)
ev p (Fst a b) (x,y) = x
ev p (Snd a b) (x,y) = y
ev p (Cur x) env {b} = \q, qtrans, arg => ev q x (tlift qtrans env, arg)
ev p (Ap a b) (fn, x) = fn p id x
ev p (Comp x y) arg = (ev p x . ev p y) arg

mutual
  reify : {a:Ft} -> ft_sem b a -> Nt a b
  reify {a = (Var k)} val = varpath k val
  reify {a = Terminal} {b} val = Const b
  reify {a = (Prod x y)} (a, b) = Pair (reify a) (reify b)
  reify {a = (Exp x y)} {b} fn
    = Cur (reify (fn (Prod b y)
          (PathPump (Fst b y))
          (reflect (PathComp (Snd b y) PathId))))

  reflect : {a:Ft} -> Path a b -> ft_sem b a
  reflect {a = (Var k)} term = term
  reflect {a = Terminal} term = ()
  reflect {a = (Prod x y)} term
    = (reflect (PathComp (Fst x y) term),
       reflect (PathComp (Snd x y) term))
  reflect {a = (Exp x y)} term
    = \q, smap, arg => reflect (PathAp (smap term) (reify arg))

nf : Nt a b -> Nt a b
nf {a} {b} nt = reify (ev b nt (reflect PathId))

complete : (f : Nt a Terminal) -> Cv f (nf f)

-- Soundness may have to take order of compositions into account.
sound : Cv f g -> nf f = nf g