Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.

9 files changed, 528 insertions, 439 deletions

diff --git a/src/Example.idr b/src/Example.idr
new file mode 100644
index 0000000..83d6acc
--- /dev/null
+++ b/src/Example.idr
@@ -0,0 +1,85 @@
+module Example
+
+import Data.Singleton
+import SOAS
+
+infixr 3 -:>
+
+-- Writing the descriptions directly is fine
+-- but deriving their functoriality and strength is annoying
+-- and not needed with enough metaprogramming
+
+data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
+
+data STLC : TypeSTLC .SortedFunctor  where
+  App : (f : a (ty1 -:> ty2) ctx) ->
+        (x : a ty1 ctx) -> STLC a ty2 ctx
+  Lam : (x : String) ->
+        (body : a ty2 (ctx :< (x :- ty1))) ->
+        STLC a (ty1 -:> ty2) ctx
+
+%hint
+strSTLC : Strength STLC
+strSTLC = MkStrength
+  { strength = \p,x,mon => \case
+    (App f x) => \theta => App (f theta) (x theta)
+    (Lam str {ty1} body) => \theta =>
+        Lam str $ body $ extend p (mon.var (%% str))
+      $ \v => mon.ren (theta v)
+                      (\u => ThereVar u) -- Bug: can't eta-reduce
+  }
+
+%hint
+functorialitySTLC : STLC .Map
+functorialitySTLC = MkMap
+  { map = \h => \case
+    (App f x) => App (h f) (h x)
+    (Lam str body) => Lam str (h body)
+  }
+
+data Term : (meta : type.SortedFamily) -> type.SortedFamily where
+  Va : Var -|> Term meta
+  Me : meta -|> Term meta ^ Term meta
+  Op : STLC (Term meta) -|> Term meta
+--   -- La : (x : String) -> bind [< x :- ty1 ] (Term meta) ty2 -||> Term meta (ty1 -:> ty2)
+--   -- bug: unification error in Ex1
+--   La : (x : String) -> Term meta ty2 (ctx :< (x :- ty1)) -> Term meta (ty1 -:> ty2) ctx
+--   -- Ap : Term meta (ty1 -:> ty2) -||> Term meta ty1 =||> Term meta ty2
+--   Ap : Term meta (ty1 -:> ty2) ctx -> Term meta ty1 ctx -> Term meta ty2 ctx
+
+%hint
+TermMetaAlg : STLC .MetaAlg meta (Term meta)
+TermMetaAlg = MkMetaAlg
+  { alg = Op
+  , var = Va
+  , mvar = Me
+  }
+
+%hint
+TermInitial : STLC .Initial meta (Term meta)
+TermInitial = MkInitial
+  { metalg = TermMetaAlg
+  , bang = bang
+  }
+  where
+    bang : (0 b : TypeSTLC .SortedFamily) -> (metalg : STLC .MetaAlg meta b) -> Term meta -|> b
+    bang b metalg (Va v) = metalg.var v
+    bang b metalg (Me m theta) = metalg.mvar m (\v => bang b metalg (theta v))
+    bang b metalg (Op (Lam str body)) = metalg.alg (Lam str (bang b metalg body))
+    bang b metalg (Op (App f x)) = metalg.alg (App (bang b metalg f) (bang b metalg x))
+
+Ex1 : Term Var (B -:> (B -:> B) -:> B) [<]
+Ex1 = Op $ Lam "x" $ Op $ Lam "f" $ Op $ App (Va $ %% "f") (Va $ %% "x")
+
+beta :
+  {0 body : Term Var ty2 (ctx :< (x :- ty1))} ->
+  Singleton (Op $ App (Op $ Lam x body) t) -> Term Var ty2 ctx
+beta (Val (Op $ App (Op $ Lam x body) t)) = TermInitial .monStruct.sub body t
+
+Ex2 : Term Var (B -:> B) [<]
+Ex2 = Op $ App
+        (Op $ Lam "f" $ Op $ Lam "x" $ Op $ App (Va $ %% "f") (Va $ (%% "x") {pos = Here}))
+        (Op $ Lam "x" $ Va $ %% "x")
+
+Ex3 : Term Var (B -:> B) [<]
+Ex3 = beta $ Val Ex2
diff --git a/src/SOAS.idr b/src/SOAS.idr
index eee2416..892f039 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -1,443 +1,94 @@
 module SOAS
 
-import Data.List.Quantifiers
-import Data.Singleton
-import Data.DPair
-import Syntax.WithProof
-
-prefix 4 %%
-infixr 3 -|> , -||> , ~> , ~:> , -<>, ^
-infixl 3 <<<
-infixr 4 :-
-
-record (.extension) (types : Type) where
-  constructor (:-)
-  0 name : String
-  ofType : types
-
-data (.Ctx) : (type : Type) -> Type where
-  Lin : type.Ctx
-  (:<) : (ctx : type.Ctx) -> (namety : type.extension) -> type.Ctx
-
-(.Family), (.SortedFamily) : Type -> Type
-type.Family = type.Ctx -> Type
-type.SortedFamily = type -> type.Family
-
-data (.varPos) : type.Ctx -> (0 x : String) -> type -> Type
-    where [search x]
-  Here  : (ctx :< (x :- ty)).varPos x ty
-  There : ctx.varPos x ty -> (ctx :< sy).varPos x ty
-
-data (.var) : type.Ctx -> type -> Type where
-  (%%) : (0 name : String) -> {auto pos : ctx.varPos name ty} -> ctx.var ty
-
-0
-(.name) : ctx.var ty -> String
-(%% name).name = name
-
-(.pos) : (v : ctx.var ty) -> ctx.varPos v.name ty
-((%% name) {pos}).pos = pos
-
-(.toVar) : (v : ctx.varPos x ty) -> ctx.var ty
-pos.toVar {x} = (%% x) {pos}
-
-ThereVar : (v : ctx.var ty) -> (ctx :< ex).var ty
-ThereVar v = (%% v.name) {pos = There v.pos}
-
-Var : type.SortedFamily
-Var = flip (.var)
-
-0
-(-||>) : {type : Type} -> (src,tgt : type.Family) -> Type
-(src -||> tgt) = {0 ctx : type.Ctx} -> src ctx -> tgt ctx
-
-0
-(-|>) : {type : Type} -> (src,tgt : type.SortedFamily) -> Type
-(src -|> tgt) = {ty : type} -> src ty -||> tgt ty
-
-(++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
-ctx1 ++ [<] = ctx1
-ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
-
-(<<<) : type.SortedFamily -> type.Ctx -> type.SortedFamily
-(f <<< ctx0) ty ctx = f ty (ctx ++ ctx0)
-
-(.subst) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
-f.subst ctx1 ctx2 = {ty : type} -> ctx1.var ty -> f ty ctx2
-
-0 (.substNamed) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
-f.substNamed ctx1 ctx2 = {0 x : String} -> {ty : type} -> ctx1.varPos x ty -> f ty ctx2
-
-(~>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
-(~>) = (Var).subst
-
-0 (~:>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
-(~:>) = (Var).substNamed
-
-weakl : (ctx1, ctx2 : type.Ctx) -> ctx1 ~> (ctx1 ++ ctx2)
-weakl ctx1 [<] x = x
-weakl ctx1 (ctx2 :< z) x = ThereVar (weakl ctx1 ctx2 x)
-
-weakrNamed : (ctx1, ctx2 : type.Ctx) -> ctx2 ~:> (ctx1 ++ ctx2)
-weakrNamed ctx1 (ctx :< (x :- ty)) Here = (%% x) {pos = Here}
-weakrNamed ctx1 (ctx :< sy) (There pos) =
-  ThereVar $ weakrNamed ctx1 ctx pos
-
-weakr : (ctx1, ctx2 : type.Ctx) -> ctx2 ~> (ctx1 ++ ctx2)
-weakr ctx1 ctx2 ((%% name) {pos}) = weakrNamed ctx1 ctx2 pos
-
-(.copairPos) : (0 x : type.SortedFamily) -> {ctx2 : type.Ctx} ->
-  x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.substNamed (ctx1 ++ ctx2) ctx
-x.copairPos {ctx2 = [<]} g1 g2 pos = g1 $ pos.toVar
-x.copairPos {ctx2 = (ctx :< (name :- ty))} g1 g2 Here = g2 (Here .toVar)
-x.copairPos {ctx2 = (ctx2 :< namety)} g1 g2 (There pos) =
-  x.copairPos g1 (g2 . ThereVar) pos
-
-(.copair) : (0 x : type.SortedFamily) -> {ctx2 : type.Ctx} ->
-  x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.subst (ctx1 ++ ctx2) ctx
-x.copair g1 g2 v = x.copairPos g1 g2 v.pos
-
-extend : (0 x : type.SortedFamily) -> {0 ctx1 : type.Ctx} -> {ty : type} ->
-  x ty ctx2 -> x.subst ctx1 ctx2 -> x.subst (ctx1 :< (n :- ty)) ctx2
-extend x {ctx2, ty} u theta =
-  x.copair {ctx2 = [< n :- ty]} theta workaround -- (\case {Here => x})
-    where
-      workaround : x.subst [< (n :- ty)] ctx2
-      workaround ((%% _) {pos = Here}) = u
-      workaround ((%% _) {pos = There _}) impossible
-
-0
-(-<>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
-(src -<> tgt) ty ctx = {0 ctx' : type.Ctx} -> src ty ctx' ->
-  tgt ty (ctx ++ ctx')
-
--- TODO: (Setoid) coalgebras
-
-0
-(^) : (tgt, src : type.SortedFamily) -> type.SortedFamily
-(tgt ^ src) ty ctx =
-  {0 ctx' : type.Ctx} -> src.subst ctx ctx' -> tgt ty ctx'
-
-0
-Nil : type.SortedFamily -> type.SortedFamily
-Nil f = f ^ Var
-
-hideCtx : {0 a : type.Ctx -> Type} ->
-  ((0 ctx : type.Ctx) -> a ctx) -> {ctx : type.Ctx} -> a ctx
-hideCtx f {ctx} = f ctx
-
-0
-(*) : (derivative, tangent : type.SortedFamily) -> type.SortedFamily
-(derivative * tangent) ty ctx =
-  (ctx' : type.Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx))
-
-record MonStruct (m : type.SortedFamily) where
-  constructor MkSubstMonoidStruct
-  var : Var -|> m
-  mult : m -|> (m ^ m)
-
-(.sub) : {m : type.SortedFamily} -> {ty,sy : type} -> {0 ctx : type.Ctx} ->
-  (mon : MonStruct m) => m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
-t.sub s = mon.mult t (extend m s mon.var)
-
-(.sub2) : {m : type.SortedFamily} -> {ty1,ty2,sy : type} ->
-  {0 ctx : type.Ctx} ->
-  (mon : MonStruct m) => m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
-  m ty1 ctx ->  m ty2 ctx -> m sy ctx
-t.sub2 s1 s2 = mon.mult t (extend m s2 (extend m s1 mon.var))
-
-record (.PointedCoalgStruct) type (x : type.SortedFamily) where
-  constructor MkPointedCoalgStruct
-  ren : x -|> [] x
-  var : Var -|> x
-
-%hint
-(.VarPointedCoalgStruct) : (0 type : Type) -> type.PointedCoalgStruct Var
-type.VarPointedCoalgStruct = MkPointedCoalgStruct
-  { ren = \i, f => f i
-  , var = id
-  }
-
-liftPos : (ctx : type.Ctx) -> (mon : type.PointedCoalgStruct p) =>
-  {ctx2 : type.Ctx} ->
-  (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx)
-liftPos [<] f x = f x.toVar
-liftPos (ctx :< (_ :- _)) f Here = mon.var (Here .toVar)
-liftPos (ctx :< namety) f (There pos) = mon.ren (liftPos ctx f pos)
-  ThereVar
-
-
-lift : (ctx : type.Ctx) -> (mon : type.PointedCoalgStruct p) =>
-  {ctx2 : type.Ctx} ->
-  (p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx)
-lift ctx f v = liftPos ctx f v.pos
-
-0
-(.SortedFunctor) : (type : Type) -> Type
-type.SortedFunctor = type.SortedFamily -> type.SortedFamily
-
-record Strength (f : type.SortedFunctor) where
-  constructor MkStrength
-  strength :
-    (0 p,x : type.SortedFamily) ->
-    (mon : type.PointedCoalgStruct p) ->
-    (f (x ^ p)) -|> ((f x) ^ p)
-
-(.str) :
-  Strength f ->
-  {0 p,x : type.SortedFamily} ->
-  (mon : type.PointedCoalgStruct p) =>
-  (f (x ^ p)) -|> ((f x) ^ p)
-strength.str {p,x,mon} = strength.strength p x mon
-
-record (.Map) (signature : type.SortedFunctor) where
-  constructor MkMap
-  map :
-    {0 a,b : type.SortedFamily} -> (a -|> b) ->
-    signature a -|> signature b
-
-record (.MonoidStruct)
-         (signature : type.SortedFunctor)
-         (x : type.SortedFamily) where
-  constructor MkSignatureMonoid
-  mon : MonStruct x
-  alg : signature x -|> x
-
-record (.MetaAlg)
-         (signature : type.SortedFunctor)
-         (meta : type.SortedFamily)
-         (a : type.SortedFamily) where
-  constructor MkMetaAlg
-  alg : signature a -|> a
-  var : Var -|> a
-  mvar : meta -|> (a ^ a)
-
-
-traverse : {0 p,a : type.SortedFamily} ->
-      {0 signature : type.SortedFunctor} ->
-      (functoriality : signature.Map) =>
-      (str : Strength signature) =>
-      (coalg : type.PointedCoalgStruct p) =>
-      (alg : signature a -|> a) ->
-      (phi : p -|> a) ->
-      (chi : meta -|> (a ^ a)) -> signature.MetaAlg meta (a ^ p)
-traverse {p,a} alg phi chi = MkMetaAlg
-      { alg = \h,s => alg $ str.str h s
-      , var = \v,s => phi (s v)
-      , mvar = \m,e,s => chi m (\v => e v s)
-      }
-
--- Does this follow from everything else?
-mapSubstPos : {0 a,b : type.SortedFamily} -> (a -|> b) -> {0 ctx : type.Ctx} ->
-  {0 ctx' : type.Ctx} ->
-  a.subst ctx ctx' -> b.substNamed ctx ctx'
-mapSubstPos f {ctx = (ctx :< (x :- ty))} theta Here
-  = f $ theta {ty} $ (%% _) {pos = Here}
-mapSubstPos f {ctx = (ctx :< sy)} theta (There pos)
-  = mapSubstPos {a,b} f (theta . ThereVar) pos
-
-mapSubst : {0 a,b : type.SortedFamily} -> (a -|> b) -> {0 ctx : type.Ctx} ->
-   (a.subst ctx -||> b.subst ctx)
-mapSubst f {ctx = ctx0} theta v = mapSubstPos {a,b} f theta v.pos
-
-(.MetaCtx) : Type -> Type
-type.MetaCtx = SnocList (type.Ctx, type)
-
-(.metaEnv) : type.SortedFamily -> type.MetaCtx -> type.Family
-x.metaEnv [<]            ctx = ()
-x.metaEnv (mctx :< meta) ctx =
-  (x.metaEnv mctx ctx, (x <<< (fst meta)) (snd meta) ctx)
-
-{- alas, non obviously strictly positive because we can't tell
-   Idris that signature must be strictly positive.
-
-   It will be, though, if we complete the termination project
--}
-
-data (.Term) : (signature : type.SortedFunctor) ->
-               type.SortedFamily -> type.SortedFamily where
-  Op : {0 signature : type.SortedFunctor} ->
-       signature (signature.Term x) ty ctx ->
-       signature.Term x ty ctx
-  Va : Var ty ctx -> signature.Term x ty ctx
-  Me : {0 ctx1, ctx2 : type.Ctx} ->
-       {0 signature : type.SortedFunctor} ->
-       x ty ctx2 ->
-       (signature.Term x).subst ctx2 ctx1 ->
-       signature.Term {type} x ty ctx1
-
-(.sem) : (0 a : type.SortedFamily) ->
-         {0 signature : type.SortedFunctor} ->
-         (functoriality : signature.Map) =>
-         (str : Strength signature) =>
-         (metalg : signature.MetaAlg x a) =>
-         signature.Term x -|> a
-a.sem (Op args) = metalg.alg $ functoriality.map a.sem args
-a.sem (Va x   ) = MetaAlg.var metalg x
-a.sem (Me  m env)
-  = MetaAlg.mvar metalg m
-  $ mapSubst {a=signature.Term x, b = a} a.sem env
-
-(.envSem) : (0 a : type.SortedFamily) ->
-            {0 signature : type.SortedFunctor} ->
-            (str : Strength signature) =>
-            (functoriality : signature.Map) =>
-            (metalg : signature.MetaAlg x a) =>
-            {mctx : type.MetaCtx} ->
-            (signature.Term x).metaEnv mctx ctx ->
-                             a.metaEnv mctx ctx
-
-a.envSem {mctx = [<]         } menv = ()
-a.envSem {mctx = mctx :< meta} (menv,v) = (a.envSem menv, a.sem v)
-
-(.TermAlg) :
-  (0 signature : type.SortedFunctor) ->
-  (str : Strength signature) =>
-  (functoriality : signature.Map) =>
-  (0 x : type.SortedFamily) ->
-  signature.MetaAlg x (signature.Term x)
-signature.TermAlg x = MkMetaAlg
-  { alg = Op
-  , mvar = \m => Me m  -- bug: type-checker complains if we
-                       -- eta-reduce
-  , var = Va
-  }
-
-(.BoxTermAlg) :
-  (0 signature : type.SortedFunctor) ->
-  (str : Strength signature) =>
-  (functoriality : signature.Map) =>
-  (0 x : type.SortedFamily) ->
-  signature.MetaAlg x ([] (signature.Term x))
-signature.BoxTermAlg x = traverse Op Va (\m => Me m)
-
-(.TermPointedCoalg) :
-  (0 signature : type.SortedFunctor) ->
-  (str : Strength signature) =>
-  (functoriality : signature.Map) =>
-  (0 x : type.SortedFamily) ->
-  type.PointedCoalgStruct (signature.Term x)
-signature.TermPointedCoalg x = MkPointedCoalgStruct
-  { ren =
-    ([] (signature.Term x)).sem
-      {metalg = signature.BoxTermAlg x}
-  , var = Va
-  }
-
-(.SubstTermAlg) :
-  (0 signature : type.SortedFunctor) ->
-  (str : Strength signature) =>
-  (functoriality : signature.Map) =>
-  (0 x : type.SortedFamily) ->
-  signature.MetaAlg x (signature.Term x ^ signature.Term x)
-signature.SubstTermAlg x = traverse
-  { coalg = signature.TermPointedCoalg x
-  , alg = Op
-  , phi = id
-  , chi = \m => Me m
-  }
-
-%hint
-(.TermMon) :
-  (0 signature : type.SortedFunctor) ->
-  (str : Strength signature) =>
-  (functoriality : signature.Map) =>
-  (0 x : type.SortedFamily) ->
-  MonStruct (signature.Term x)
-signature.TermMon x = MkSubstMonoidStruct
-  { var = Va
-  , mult =
-    (signature.Term x ^ signature.Term x).sem
-      {metalg = signature.SubstTermAlg x}
-  }
-
-%hint
-(.TermMonoid) :
-  (0 signature : type.SortedFunctor) ->
-  (str : Strength signature) =>
-  (functoriality : signature.Map) =>
-  (0 x : type.SortedFamily) ->
-  signature.MonoidStruct (signature.Term x)
-signature.TermMonoid x = MkSignatureMonoid
-  { mon = signature.TermMon x
-  , alg = Op
-  }
-
--- Not sure these are useful
-data (+) : (signature1, signature2 : type.SortedFunctor) ->
-  type.SortedFunctor where
-  Lft  :  {signature1, signature2 : type.SortedFunctor} ->
-    (op : sig1 x ty ctx) -> (sig1 + sig2) x ty ctx
-  Rgt :  {signature1, signature2 : type.SortedFunctor} ->
-    (op : sig2 x ty ctx) -> (sig1 + sig2) x ty ctx
-
-sum : (signatures : List $ (String, type.SortedFunctor)) ->
-  type.SortedFunctor
-(sum signatures) x ty ctx = Any (\(name,sig) => sig x ty ctx) signatures
-
-prod : (signatures : List $ type.SortedFunctor) ->
-  type.SortedFunctor
-(prod signatures) x ty ctx = All (\sig => sig x ty ctx) signatures
-
+import public SOAS.Algebra
+import public SOAS.Context
+import public SOAS.Family
+import public SOAS.Strength
+import public SOAS.Structure
+import public SOAS.Theory
+import public SOAS.Var
+
+-- -- TODO: (Setoid) coalgebras
+
+-- -- Does this follow from everything else?
+-- mapSubstPos : {0 a,b : type.SortedFamily} -> (a -|> b) -> {0 ctx : type.Ctx} ->
+--   {0 ctx' : type.Ctx} ->
+--   a.subst ctx ctx' -> b.substNamed ctx ctx'
+-- mapSubstPos f {ctx = (ctx :< (x :- ty))} theta Here
+--   = f $ theta {ty} $ (%% _) {pos = Here}
+-- mapSubstPos f {ctx = (ctx :< sy)} theta (There pos)
+--   = mapSubstPos {a,b} f (theta . ThereVar) pos
+
+-- mapSubst : {0 a,b : type.SortedFamily} -> (a -|> b) -> {0 ctx : type.Ctx} ->
+--    (a.subst ctx -||> b.subst ctx)
+-- mapSubst f {ctx = ctx0} theta v = mapSubstPos {a,b} f theta v.pos
+
+-- (.MetaCtx) : Type -> Type
+-- type.MetaCtx = SnocList (type.Ctx, type)
+
+-- (.metaEnv) : type.SortedFamily -> type.MetaCtx -> type.Family
+-- x.metaEnv [<]            ctx = ()
+-- x.metaEnv (mctx :< meta) ctx =
+--   (x.metaEnv mctx ctx, (x <<< (fst meta)) (snd meta) ctx)
+
+-- {- alas, non obviously strictly positive because we can't tell
+--    Idris that signature must be strictly positive.
+
+--    It will be, though, if we complete the termination project
+-- -}
+
+-- data (.Term) : (signature : type.SortedFunctor) ->
+--                type.SortedFamily -> type.SortedFamily where
+--   Op : {0 signature : type.SortedFunctor} ->
+--        signature (signature.Term x) ty ctx ->
+--        signature.Term x ty ctx
+--   Va : Var ty ctx -> signature.Term x ty ctx
+--   Me : {0 ctx1, ctx2 : type.Ctx} ->
+--        {0 signature : type.SortedFunctor} ->
+--        x ty ctx2 ->
+--        (signature.Term x).subst ctx2 ctx1 ->
+--        signature.Term {type} x ty ctx1
+
+-- (.sem) : (0 a : type.SortedFamily) ->
+--          {0 signature : type.SortedFunctor} ->
+--          (functoriality : signature.Map) =>
+--          (str : Strength signature) =>
+--          (metalg : signature.MetaAlg x a) =>
+--          signature.Term x -|> a
+-- a.sem (Op args) = metalg.alg $ functoriality.map a.sem args
+-- a.sem (Va x   ) = MetaAlg.var metalg x
+-- a.sem (Me  m env)
+--   = MetaAlg.mvar metalg m
+--   $ mapSubst {a=signature.Term x, b = a} a.sem env
+
+-- (.envSem) : (0 a : type.SortedFamily) ->
+--             {0 signature : type.SortedFunctor} ->
+--             (str : Strength signature) =>
+--             (functoriality : signature.Map) =>
+--             (metalg : signature.MetaAlg x a) =>
+--             {mctx : type.MetaCtx} ->
+--             (signature.Term x).metaEnv mctx ctx ->
+--                              a.metaEnv mctx ctx
+
+-- a.envSem {mctx = [<]         } menv = ()
+-- a.envSem {mctx = mctx :< meta} (menv,v) = (a.envSem menv, a.sem v)
+
+-- -- Not sure these are useful
+-- data (+) : (signature1, signature2 : type.SortedFunctor) ->
+--   type.SortedFunctor where
+--   Lft  :  {signature1, signature2 : type.SortedFunctor} ->
+--     (op : sig1 x ty ctx) -> (sig1 + sig2) x ty ctx
+--   Rgt :  {signature1, signature2 : type.SortedFunctor} ->
+--     (op : sig2 x ty ctx) -> (sig1 + sig2) x ty ctx
+
+-- sum : (signatures : List $ (String, type.SortedFunctor)) ->
+--   type.SortedFunctor
+-- (sum signatures) x ty ctx = Any (\(name,sig) => sig x ty ctx) signatures
+
+-- prod : (signatures : List $ type.SortedFunctor) ->
+--   type.SortedFunctor
+-- (prod signatures) x ty ctx = All (\sig => sig x ty ctx) signatures
+
+public export
 bind : (tys : type.Ctx) -> type.SortedFunctor
 bind tys = (<<< tys)
-
-infixr 3 -:>
-
--- Writing the descriptions directly is fine
--- but deriving their functoriality and strength is annoying
--- and not needed with enough metaprogramming
-
-data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
-
-data STLC : TypeSTLC .SortedFunctor  where
-  App : {ty1, ty2 : TypeSTLC} ->
-        (f : a (ty1 -:> ty2) ctx) ->
-        (x : a ty1 ctx) -> STLC a ty2 ctx
-  Lam : (x : String) -> {ty1 : TypeSTLC} ->
-        (body : a ty2 (ctx :< (x :- ty1))) ->
-        STLC a (ty1 -:> ty2) ctx
-
-%hint
-strSTLC : Strength STLC
-strSTLC = MkStrength
-  { strength = \p,x,mon => \case
-    (App f x) => \theta => App (f theta) (x theta)
-    (Lam str {ty1} body) => \theta =>
-        Lam str $ body $ extend p (mon.var (%% str))
-      $ \v => mon.ren (theta v)
-                      (\u => ThereVar u) -- Bug: can't eta-reduce
-  }
-
-%hint
-functorialitySTLC : STLC .Map
-functorialitySTLC = MkMap
-  { map = \h => \case
-    (App f x) => App (h f) (h x)
-    (Lam str body) => Lam str (h body)
-  }
-
-Ex1 : STLC .Term Var (B -:> (B -:> B) -:> B) [<]
-Ex1 = Op $ Lam "x" $
-      Op $ Lam "f" $
-      Op $ App (Va $ %% "f")
-               (Va $ %% "x")
-
-beta : Singleton
-       {a = STLC .Term Var ty ctx}
-       (Op $ App (Op $ Lam x body) t) -> STLC .Term Var ty ctx
-beta (Val (Op $ App (Op $ Lam x body) t)) =
-  (.sub) {mon = STLC .TermMon Var} body t -- bug: cannot determine mon automagically
-
-Ex2 : STLC .Term Var (B -:> B) [<]
-Ex2 = Op $ App
-        (Op $ Lam "f" $
-         Op $ Lam "x" $
-         Op $ App
-              (Va $ %% "f")
-              (Va $ %% "x"))
-        (Op $ Lam "x" $
-              Va $ %% "x")
-
-Ex3 : STLC .Term Var (B -:> B) [<]
-Ex3 = beta $ Val Ex2
diff --git a/src/SOAS/Algebra.idr b/src/SOAS/Algebra.idr
new file mode 100644
index 0000000..7dff735
--- /dev/null
+++ b/src/SOAS/Algebra.idr
@@ -0,0 +1,40 @@
+module SOAS.Algebra
+
+import SOAS.Context
+import SOAS.Family
+import SOAS.Strength
+import SOAS.Structure
+import SOAS.Var
+
+public export
+record (.MonoidStruct)
+         (signature : type.SortedFunctor)
+         (x : type.SortedFamily) where
+  constructor MkSignatureMonoid
+  mon : type.MonStruct x
+  alg : signature x -|> x
+
+public export
+record (.MetaAlg)
+         (signature : type.SortedFunctor)
+         (meta : type.SortedFamily)
+         (a : type.SortedFamily) where
+  constructor MkMetaAlg
+  alg : signature a -|> a
+  var : Var -|> a
+  mvar : meta -|> (a ^ a)
+
+export
+traverse : {0 p,a : type.SortedFamily} ->
+      {0 signature : type.SortedFunctor} ->
+      (functoriality : signature.Map) =>
+      (str : Strength signature) =>
+      (coalg : type.PointedCoalgStruct p) =>
+      (alg : signature a -|> a) ->
+      (phi : p -|> a) ->
+      (chi : meta -|> (a ^ a)) -> signature.MetaAlg meta (a ^ p)
+traverse {p,a} alg phi chi = MkMetaAlg
+      { alg = \h,s => alg $ str.str h s
+      , var = \v,s => phi (s v)
+      , mvar = \m,e,s => chi m (\v => e v s)
+      }
diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr
new file mode 100644
index 0000000..25d2308
--- /dev/null
+++ b/src/SOAS/Context.idr
@@ -0,0 +1,24 @@
+module SOAS.Context
+
+infixr 4 :-
+
+public export
+record (.extension) (type : Type) where
+  constructor (:-)
+  0 name : String
+  ofType : type
+
+public export
+data (.Ctx) : (type : Type) -> Type where
+  Lin : type.Ctx
+  (:<) : (ctx : type.Ctx) -> (namety : type.extension) -> type.Ctx
+
+public export
+data (.Erased) : type.Ctx -> Type where
+  Z : [<].Erased
+  S : ctx.Erased -> (ctx :< x).Erased
+
+public export
+(++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
+ctx1 ++ [<] = ctx1
+ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
diff --git a/src/SOAS/Family.idr b/src/SOAS/Family.idr
new file mode 100644
index 0000000..cd3ae58
--- /dev/null
+++ b/src/SOAS/Family.idr
@@ -0,0 +1,43 @@
+module SOAS.Family
+
+import SOAS.Context
+
+infixr 3 -|> , -||> , -<>, =||> , =|> , >>> , ^
+infixl 3 <<<
+
+public export
+(.Family), ( .SortedFamily) : Type -> Type
+type.Family = type.Ctx -> Type
+type.SortedFamily = type -> type.Family
+
+public export 0
+(-||>) : {type : Type} -> (src,tgt : type.Family) -> Type
+(src -||> tgt) = {0 ctx : type.Ctx} -> src ctx -> tgt ctx
+
+public export 0
+(-|>) : {type : Type} -> (src,tgt : type.SortedFamily) -> Type
+(src -|> tgt) = {0 ty : type} -> src ty -||> tgt ty
+
+public export
+(<<<) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f <<< ctx0) ty ctx = f ty (ctx ++ ctx0)
+
+public export
+(>>>) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f >>> ctx0) ty ctx = f ty (ctx0 ++ ctx)
+
+public export 0
+(-<>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src -<> tgt) ty ctx = src ty -||> (tgt >>> ctx) ty
+
+public export
+(=||>) : (src, tgt : type.Family) -> type.Family
+(src =||> tgt) ctx = src ctx -> tgt ctx
+
+public export
+(=|>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src =|> tgt) ty = src ty =||> tgt ty
+
+public export 0
+(.gensubst) : (type : Type) -> (from,to : type.SortedFamily) -> (src,tgt : type.Ctx) -> Type
+type.gensubst from to src tgt = {0 ty : type} -> from ty src -> to ty tgt
diff --git a/src/SOAS/Strength.idr b/src/SOAS/Strength.idr
new file mode 100644
index 0000000..f902ad4
--- /dev/null
+++ b/src/SOAS/Strength.idr
@@ -0,0 +1,33 @@
+module SOAS.Strength
+
+import SOAS.Family
+import SOAS.Structure
+import SOAS.Var
+
+public export
+0
+(.SortedFunctor) : (type : Type) -> Type
+type.SortedFunctor = type.SortedFamily -> type.SortedFamily
+
+public export
+record Strength (f : type.SortedFunctor) where
+  constructor MkStrength
+  strength :
+    (0 p,x : type.SortedFamily) ->
+    (mon : type.PointedCoalgStruct p) ->
+    (f (x ^ p)) -|> ((f x) ^ p)
+
+export
+(.str) :
+  Strength f ->
+  {0 p,x : type.SortedFamily} ->
+  (mon : type.PointedCoalgStruct p) =>
+  (f (x ^ p)) -|> ((f x) ^ p)
+strength.str {p,x,mon} = strength.strength p x mon
+
+public export
+record (.Map) (signature : type.SortedFunctor) where
+  constructor MkMap
+  map :
+    {0 a,b : type.SortedFamily} -> (a -|> b) ->
+    signature a -|> signature b
diff --git a/src/SOAS/Structure.idr b/src/SOAS/Structure.idr
new file mode 100644
index 0000000..854725f
--- /dev/null
+++ b/src/SOAS/Structure.idr
@@ -0,0 +1,54 @@
+module SOAS.Structure
+
+import SOAS.Context
+import SOAS.Family
+import SOAS.Var
+
+-- Pointed Coalgebra
+
+public export
+record (.PointedCoalgStruct) type (x : type.SortedFamily) where
+  constructor MkPointedCoalgStruct
+  ren : x -|> [] x
+  var : Var -|> x
+
+%hint
+(.VarPointedCoalgStruct) : (0 type : Type) -> type.PointedCoalgStruct Var
+type.VarPointedCoalgStruct = MkPointedCoalgStruct
+  { ren = \i, f => f i
+  , var = id
+  }
+
+liftPos :
+  (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
+  (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx)
+liftPos Z     f x = f x.toVar
+liftPos (S l) f Here        = mon.var (Here .toVar)
+liftPos (S l) f (There pos) = mon.ren (liftPos l f pos) ThereVar
+
+export
+lift :
+  (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
+  (p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx)
+lift ctx f v = liftPos ctx f v.pos
+
+-- Substitution Monoid
+
+public export
+record (.MonStruct) (type : Type) (m : type.SortedFamily) where
+  constructor MkSubstMonoidStruct
+  var : Var -|> m
+  mult : m -|> (m ^ m)
+
+export
+(.sub) :
+  (mon : type.MonStruct m) ->
+  m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
+mon.sub t s = mon.mult t (extend m s mon.var)
+
+export
+(.sub2) :
+  (mon : type.MonStruct m) ->
+  m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
+  m ty1 ctx ->  m ty2 ctx -> m sy ctx
+mon.sub2 t s1 s2 = mon.mult t (extend m s2 (extend m s1 mon.var))
diff --git a/src/SOAS/Theory.idr b/src/SOAS/Theory.idr
new file mode 100644
index 0000000..f36e7a1
--- /dev/null
+++ b/src/SOAS/Theory.idr
@@ -0,0 +1,58 @@
+module SOAS.Theory
+
+import SOAS.Algebra
+import SOAS.Context
+import SOAS.Family
+import SOAS.Strength
+import SOAS.Structure
+import SOAS.Var
+
+public export
+record (.Initial)
+         (signature : type.SortedFunctor)
+         (meta : type.SortedFamily)
+         (a : type.SortedFamily) where
+  constructor MkInitial
+  metalg : signature.MetaAlg meta a
+  bang :
+    (0 b : type.SortedFamily) ->
+    (metalg : signature.MetaAlg meta b) ->
+    a -|> b
+
+public export
+(.sem) :
+  signature .Initial meta a ->
+  (0 b : type.SortedFamily) -> (metalg : signature.MetaAlg meta b) =>
+  a -|> b
+init.sem b = init.bang b metalg
+
+%hint
+public export
+(.pointedCoalgStruct) :
+  (functoriality : signature.Map) =>
+  (str : Strength signature) =>
+  signature.Initial meta a -> type.PointedCoalgStruct a
+init.pointedCoalgStruct = MkPointedCoalgStruct
+  { ren = init.sem ([] a) @{traverse init.metalg.alg init.metalg.var init.metalg.mvar}
+  , var = init.metalg.var
+  }
+
+
+%hint
+public export
+(.monStruct) :
+  (functoriality : signature.Map) =>
+  (str : Strength signature) =>
+  signature.Initial meta a -> type.MonStruct a
+init.monStruct = MkSubstMonoidStruct
+  { var = init.metalg.var
+  , mult = init.sem (a ^ a) @{traverse init.metalg.alg id init.metalg.mvar}
+  }
+
+%hint
+public export
+(.monoidStruct) :
+  (functoriality : signature.Map) =>
+  (str : Strength signature) =>
+  signature.Initial meta a -> signature.MonoidStruct a
+init.monoidStruct = MkSignatureMonoid { mon = init.monStruct , alg = init.metalg.alg }
diff --git a/src/SOAS/Var.idr b/src/SOAS/Var.idr
new file mode 100644
index 0000000..f3129f9
--- /dev/null
+++ b/src/SOAS/Var.idr
@@ -0,0 +1,101 @@
+module SOAS.Var
+
+import SOAS.Context
+import SOAS.Family
+
+prefix 4 %%
+infixr 3 ~> , ~:>
+
+public export
+data (.varPos) : (ctx : type.Ctx) -> (0 x : String) -> type -> Type
+    where [search x]
+  Here  : (ctx :< (x :- ty)).varPos x ty
+  There : ctx.varPos x ty -> (ctx :< sy).varPos x ty
+
+public export
+data (.var) : type.Ctx -> type -> Type where
+  (%%) : (0 name : String) -> {auto pos : ctx.varPos name ty} -> ctx.var ty
+
+0
+(.name) : ctx.var ty -> String
+(%% name).name = name
+
+export
+(.pos) : (v : ctx.var ty) -> ctx.varPos v.name ty
+((%% name) {pos}).pos = pos
+
+export
+(.toVar) : (v : ctx.varPos x ty) -> ctx.var ty
+pos.toVar {x} = (%% x) {pos}
+
+export
+ThereVar : (v : ctx.var ty) -> (ctx :< ex).var ty
+ThereVar v = (%% v.name) {pos = There v.pos}
+
+public export
+Var : type.SortedFamily
+Var = flip (.var)
+
+public export 0
+(.subst) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
+f.subst ctx1 ctx2 = type.gensubst Var f ctx1 ctx2
+
+public export 0
+(.substNamed) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
+f.substNamed ctx1 ctx2 = {0 x : String} -> {0 ty : type} -> ctx1.varPos x ty -> f ty ctx2
+
+public export 0
+(~>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
+(~>) = (Var).subst
+
+public export 0
+(~:>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
+(~:>) = (Var).substNamed
+
+weakl : (ctx1, ctx2 : type.Ctx) -> ctx1 ~> (ctx1 ++ ctx2)
+weakl ctx1 [<] x = x
+weakl ctx1 (ctx2 :< z) x = ThereVar (weakl ctx1 ctx2 x)
+
+weakrNamed : (ctx1, ctx2 : type.Ctx) -> ctx2 ~:> (ctx1 ++ ctx2)
+weakrNamed ctx1 (ctx :< (x :- ty)) Here = (%% x) {pos = Here}
+weakrNamed ctx1 (ctx :< sy) (There pos) =
+  ThereVar $ weakrNamed ctx1 ctx pos
+
+weakr : (ctx1, ctx2 : type.Ctx) -> ctx2 ~> (ctx1 ++ ctx2)
+weakr ctx1 ctx2 ((%% name) {pos}) = weakrNamed ctx1 ctx2 pos
+
+(.copairPos) :
+  (0 x : type.SortedFamily) -> {auto length : ctx2.Erased} ->
+  x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.substNamed (ctx1 ++ ctx2) ctx
+x.copairPos {length = Z} g1 g2 pos = g1 $ pos.toVar
+x.copairPos {length = S l} g1 g2 Here = g2 (Here .toVar)
+x.copairPos {length = S l} g1 g2 (There pos) =
+  x.copairPos g1 (g2 . ThereVar) pos
+
+(.copair) :
+  (0 x : type.SortedFamily) -> {auto length : ctx2.Erased} ->
+  x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.subst (ctx1 ++ ctx2) ctx
+x.copair g1 g2 v = x.copairPos g1 g2 v.pos
+
+export
+extend :
+  (0 x : type.SortedFamily) ->
+  x ty ctx2 -> x.subst ctx1 ctx2 ->
+  x.subst (ctx1 :< (n :- ty)) ctx2
+extend x {ctx2, ty} u theta = x.copair {length = S Z} theta workaround -- (\case {Here => x})
+    where
+      workaround : x.subst [< (n :- ty)] ctx2
+      workaround ((%% _) {pos = Here}) = u
+
+public export 0
+(^) : (tgt, src : type.SortedFamily) -> type.SortedFamily
+(tgt ^ src) ty ctx = src.subst ctx -||> tgt ty
+
+public export 0
+Nil : type.SortedFamily -> type.SortedFamily
+Nil f = f ^ Var
+
+0
+(*) : (derivative, tangent : type.SortedFamily) -> type.SortedFamily
+(derivative * tangent) ty ctx =
+  (ctx' : type.Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx))