Refactor to support concrete names in support

2 files changed, 229 insertions, 155 deletions

diff --git a/soas.ipkg b/soas.ipkg
index 096c6a0..9371eb8 100644
--- a/soas.ipkg
+++ b/soas.ipkg
@@ -13,10 +13,10 @@ authors = "Ohad Kammar"
 -- langversion
 
 -- packages to add to search path
--- depends =
+depends = contrib
 
 -- modules to install
-modules = Soas
+modules = SOAS
 
 -- main file (i.e. file to load at REPL)
 -- main =
diff --git a/src/SOAS.idr b/src/SOAS.idr
index 83a7c33..1cb52ab 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -1,141 +1,208 @@
 module SOAS
 
 import Data.List.Quantifiers
+import Data.Singleton
+import Data.DPair
+import Syntax.WithProof
 
-parameters {Ty : Type}
-  data Ctx : Type where
-    Lin : Ctx
-    (:<) : (ctx : Ctx) -> (ty : Ty) -> Ctx
+prefix 4 %%
+infixr 3 -|> , ~> , ~:> , -<>, ^
+infixl 3 <<<
+infixr 4 :-
 
-  data (.var) : Ctx -> Ty -> Type where
-    Here  : (ctx :< ty).var ty
-    There : ctx.var ty -> (ctx :< sy).var ty
+record (.extension) (types : Type) where
+  constructor (:-)
+  0 name : String
+  ofType : types
 
-  Family, SortedFamily : Type
-  Family = Ctx -> Type
-  SortedFamily = Ty -> Family
+data (.Ctx) : (type : Type) -> Type where
+  Lin : type.Ctx
+  (:<) : (ctx : type.Ctx) -> (namety : type.extension) -> type.Ctx
 
-  Var : SortedFamily
-  Var = flip (.var)
+(.Family), (.SortedFamily) : Type -> Type
+type.Family = type.Ctx -> Type
+type.SortedFamily = type -> type.Family
 
-  infixr 3 -|> , ~> , -<>, ^
+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
 
-  infixl 3 <<<
+data (.var) : type.Ctx -> type -> Type where
+  (%%) : (0 name : String) -> {auto pos : ctx.varPos name ty} -> ctx.var ty
 
-  (-|>) : (src,tgt : SortedFamily) -> Type
-  (src -|> tgt) = {ty : Ty} -> {ctx : Ctx} -> src ty ctx -> tgt ty ctx
+0
+(.name) : ctx.var ty -> String
+(%% name).name = name
 
-  (++) : (ctx1,ctx2 : Ctx) -> Ctx
-  ctx1 ++ [<] = ctx1
-  ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
+(.pos) : (v : ctx.var ty) -> ctx.varPos v.name ty
+((%% name) {pos}).pos = pos
 
-  (<<<) : SortedFamily -> Ctx -> SortedFamily
-  (f <<< ctx0) ty ctx = f ty (ctx ++ ctx0)
+(.toVar) : (v : ctx.varPos x ty) -> ctx.var ty
+pos.toVar {x} = (%% x) {pos}
 
-  (.subst) : SortedFamily -> Ctx -> Ctx -> Type
-  f.subst ctx1 ctx2 = {ty : Ty} -> ctx1.var ty -> f ty ctx2
+ThereVar : (v : ctx.var ty) -> (ctx :< ex).var ty
+ThereVar v = (%% v.name) {pos = There v.pos}
 
-  (~>) : (src, tgt : Ctx) -> Type
-  (~>) = (flip (.var)).subst
+Var : type.SortedFamily
+Var = flip (.var)
 
-  weakl : (ctx1, ctx2 : Ctx) -> ctx1 ~> (ctx1 ++ ctx2)
-  weakl ctx1 [<] x = x
-  weakl ctx1 (ctx2 :< z) x = There $ weakl ctx1 ctx2 x
+0
+(-|>) : {type : Type} -> (src,tgt : type.SortedFamily) -> Type
+(src -|> tgt) = {ty : type} -> {0 ctx : type.Ctx} ->
+  src ty ctx -> tgt ty ctx
 
-  weakr : (ctx1, ctx2 : Ctx) -> ctx2 ~> (ctx1 ++ ctx2)
-  weakr ctx1 (ctx2 :< _) Here = Here
-  weakr ctx1 (ctx2 :< sy) (There x) = There (weakr ctx1 ctx2 x)
+(++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
+ctx1 ++ [<] = ctx1
+ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
 
-  (.copair) : (f : SortedFamily) -> {ctx2 : Ctx} -> f.subst ctx1 ctx -> f.subst ctx2 ctx -> f.subst (ctx1 ++ ctx2) ctx
-  f.copair {ctx2 = [<]       } g1 g2 x = g1 x
-  f.copair {ctx2 = ctx2 :< ty} g1 g2 Here = g2 Here
-  f.copair {ctx2 = ctx2 :< ty} g1 g2 (There x) = f.copair g1 (g2 . There) x
+(<<<) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f <<< ctx0) ty ctx = f ty (ctx ++ ctx0)
 
-  extend : (f : SortedFamily) -> {ctx1 : Ctx} -> {ty : Ty} -> f ty ctx2 -> f.subst ctx1 ctx2 -> f.subst (ctx1 :< ty) ctx2
-  extend f {ctx2, ty} x theta = f.copair {ctx2 = [< ty]} theta workaround -- (\case {Here => x})
-    where
-      workaround : f.subst [< ty] ctx2
-      workaround Here = x
+(.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
 
-  (-<>) : (src, tgt : SortedFamily) -> SortedFamily
-  (src -<> tgt) ty ctx = {ctx' : Ctx} -> src ty ctx' -> tgt ty (ctx ++ ctx')
+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)
 
-  Nil : SortedFamily -> SortedFamily
-  Nil f ty ctx = {ctx' : Ctx} -> ctx ~> ctx' -> f ty ctx'
+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
 
-  -- TODO: (Setoid) coalgebras
+weakr : (ctx1, ctx2 : type.Ctx) -> ctx2 ~> (ctx1 ++ ctx2)
+weakr ctx1 ctx2 ((%% name) {pos}) = weakrNamed ctx1 ctx2 pos
 
-  (^) : (tgt, src : SortedFamily) -> SortedFamily
-  (tgt ^ src) ty ctx = {ctx' : Ctx} -> src.subst ctx ctx' -> tgt ty ctx'
+(.copairPos) : (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) : (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 : (x : type.SortedFamily) -> {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
 
-  hideCtx : {0 a : Ctx -> Type} ->
-    ((ctx : Ctx) -> a ctx) -> {ctx : Ctx} -> a ctx
-  hideCtx f {ctx} = f ctx
+0
+(-<>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src -<> tgt) ty ctx = {0 ctx' : type.Ctx} -> src ty ctx' ->
+  tgt ty (ctx ++ ctx')
 
-  (*) : (derivative, tangent : SortedFamily) -> SortedFamily
-  (derivative * tangent) ty ctx = (ctx' : Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx))
+0
+Nil : type.SortedFamily -> type.SortedFamily
+Nil f ty ctx = {0 ctx' : type.Ctx} -> ctx ~> ctx' -> f ty ctx'
 
-record MonStruct {Ty : Type} (m : SortedFamily {Ty}) where
+-- 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'
+
+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) : {Ty : Type} -> {m : SortedFamily {Ty}} -> {ty,sy : Ty} -> {ctx : Ctx {Ty}} ->
-  (mon : MonStruct m) => m sy (ctx :< ty) -> m ty ctx -> m sy ctx
+(.sub) : {m : type.SortedFamily} -> {ty,sy : type} -> {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) : {Ty : Type} -> {m : SortedFamily {Ty}} -> {ty1,ty2,sy : Ty} -> {ctx : Ctx {Ty}} ->
-  (mon : MonStruct m) => m sy (ctx :< ty1 :< ty2) -> m ty1 ctx -> m ty2 ctx -> m sy ctx
+(.sub2) : {m : type.SortedFamily} -> {ty1,ty2,sy : type} ->
+  {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 (x : SortedFamily) where
+record PointedCoalgStruct (x : type.SortedFamily) where
   constructor MkPointedCoalgStruct
   ren : x -|> [] x
   var : Var -|> x
 
-lift : (ctx : Ctx) -> (mon : PointedCoalgStruct p) => {ctx2 : Ctx} ->
-  (p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx)
-lift [<] f x = f x
-lift (ctx :< ty) f Here = mon.var Here
-lift (ctx :< ty) f (There x) = mon.ren (lift ctx f x) There
+liftPos : (ctx : type.Ctx) -> (mon : 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
 
 
-Strength : {Ty : Type} -> (f : SortedFamily {Ty} -> SortedFamily {Ty}) -> Type
-Strength f = {p,x : SortedFamily {Ty}} -> (mon : PointedCoalgStruct p) =>
+lift : (ctx : type.Ctx) -> (mon : 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
+Strength : (f : type.SortedFamily -> type.SortedFamily) -> Type
+Strength f = {0 p,x : type.SortedFamily} -> (mon : PointedCoalgStruct p) =>
   (f (x ^ p)) -|> ((f x) ^ p)
 
-SortedFunctor : {type : Type} -> Type
-SortedFunctor {type} = SortedFamily {Ty=type} ->
-                       SortedFamily {Ty=type}
+0
+(.SortedFunctor) : (type : Type) -> Type
+type.SortedFunctor = type.SortedFamily -> type.SortedFamily
 
-SortedFunctorMap : {type : Type} -> SortedFunctor {type} -> Type
-SortedFunctorMap {type} signature
-  = {a,b : SortedFamily {Ty = type}} -> (a -|> b) ->
+0
+(.Map) : type.SortedFunctor -> Type
+signature.Map
+  = {0 a,b : type.SortedFamily} -> (a -|> b) ->
     signature a -|> signature b
 
-
-
-parameters {Ty : Type} (signature : SortedFunctor {type = Ty})
-                       (str : Strength {Ty} signature)
-  record (.MonoidStruct) (x : SortedFamily {Ty}) where
-    constructor MkSignatureMonoid
-    mon : MonStruct x
-    alg : signature x -|> x
-
-  parameters (meta : SortedFamily {Ty})
-    record MetaAlg (a : SortedFamily {Ty}) where
-      constructor MkMetaAlg
-      alg : signature a -|> a
-      var : Var -|> a
-      mvar : meta -|> (a ^ a)
-
-    traverse : {p,a : SortedFamily {Ty}} ->
+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 : PointedCoalgStruct p) =>
       (alg : signature a -|> a) ->
       (phi : p -|> a) ->
-      (chi : meta -|> (a ^ a)) -> MetaAlg (a ^ p)
-    traverse {p,a} alg phi chi = MkMetaAlg
+      (chi : meta -|> (a ^ a)) -> signature.MetaAlg meta (a ^ p)
+traverse {p,a} alg phi chi = MkMetaAlg
       { alg = \h,s => alg $ str h s
       , var = \v,s => phi (s v)
       , mvar = \m,e,s => chi m (\v => e v s)
@@ -143,100 +210,107 @@ parameters {Ty : Type} (signature : SortedFunctor {type = Ty})
 
 namespace TermDef
  mutual
-
-    {- alas, non obviously strictly positive because we can't tell
+  {- 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
-    -}
+  -}
 
   public export
-  data Sub : {type : Type} -> {signature : SortedFunctor {type}} ->
-       SortedFamily {Ty = type} -> Ctx {Ty = type} ->
-       Ctx {Ty = type} -> Type where
+  data Sub : {0 signature : type.SortedFunctor} ->
+       type.SortedFamily -> type.Ctx ->
+       type.Ctx -> Type where
       Lin :  Sub {type, signature} x [<] ctx
       (:<) : Sub {type, signature} x shape ctx ->
              signature.Term x ty ctx ->
-             Sub {type,signature} x (shape :< ty) ctx
+             Sub {type,signature} x (shape :< (n :- ty)) ctx
 
   public export
-  data (.Term) : {type : Type} ->
-       (signature : SortedFunctor {type}) ->
-       SortedFamily {Ty = type} ->
-       SortedFamily {Ty = type}
-       where
-    Op : {signature : SortedFunctor {type}} ->
+  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 : {ctx1, ctx2 : Ctx {Ty = type}} ->
+    Me : {0 ctx1, ctx2 : type.Ctx} ->
+         {0 signature : type.SortedFunctor} ->
          x ty ctx2 ->
-         Sub (signature.Term {type} x)
-             ctx2 ctx1 ->
+         Sub (signature.Term x) ctx2 ctx1 ->
          signature.Term {type} x ty ctx1
 
-parameters {type : Type} {signature : SortedFunctor {type}}
-  MetaContext : Type
-  MetaContext = SnocList (Ctx {Ty=type}, type)
-
-  (.metaEnv) : SortedFamily {Ty=type} -> MetaContext ->
-               Family {Ty=type}
-  x.metaEnv [<]            ctx = ()
-  x.metaEnv (mctx :< meta) ctx =
-    (x.metaEnv mctx ctx, (x <<< (fst meta)) (snd meta) ctx)
-
-parameters {type : Type} {signature : SortedFunctor {type}}
-           {auto signatureMap : SortedFunctorMap signature}
-           {auto str : Strength {Ty = type} signature}
-  parameters {x : SortedFamily {Ty = type}}
-             (a : SortedFamily {Ty = type})
-             {auto metalg : MetaAlg {Ty = type} signature str x a}
-    (.envSem) : {ctx : Ctx} -> {mctx : MetaContext {signature}} ->
-                (signature.Term x).metaEnv mctx ctx ->
-                                 a.metaEnv mctx ctx
-    (.subSem) : Sub (signature.Term x) ctx1 ctx2  ->
-      a.subst ctx1 ctx2
-    (.sem) : signature.Term x -|> a
-
-    (.envSem) {mctx = [<]         } menv = ()
-    (.envSem) {mctx = mctx :< meta} (menv,v) =
-      ( (.envSem) menv
-      , (.sem) v
+(.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)
+
+(.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
+(.subSem) : (0 a : type.SortedFamily) ->
+            {0 x : type.SortedFamily} ->
+            {0 signature : type.SortedFunctor} ->
+            (functoriality : signature.Map) =>
+            (str : Strength signature) =>
+            Sub (signature.Term x) ctx1 ctx2  ->
+            a.subst ctx1 ctx2
+(.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.envSem {mctx = [<]         } menv = ()
+a.envSem {mctx = mctx :< meta} (menv,v) =
+      ( a.envSem {signature,x,str,functoriality} menv
+      , a.sem {signature,x,str,functoriality} v
       )
-
-    (.sem) (Op args) = MetaAlg.alg _ _ _ metalg
-                     $ signatureMap {b = a} (.sem) args
-    (.sem) (Va x   ) = MetaAlg.var _ _ _ metalg x
-    (.sem) {ctx = ctx1''} (Me  m env) = MetaAlg.mvar _ _ _ metalg m $ ((.subSem) env)
-
-
-data (+) : {type : Type} -> (signature1, signature2 : SortedFunctor {type}) ->
-  SortedFunctor {type} where
-  Lft  :  {signature1, signature2 : SortedFunctor {type}} ->
+a.sem (Op args) = metalg.alg
+                 $ functoriality {b = a}
+                   (a.sem {signature,x,str,functoriality}) args
+a.sem (Va x   ) = MetaAlg.var metalg x
+a.sem {ctx = ctx1''} (Me  m env) =
+  MetaAlg.mvar metalg m $ (a.subSem {signature,x,str,functoriality} env)
+
+-- 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 : SortedFunctor {type}} ->
+  Rgt :  {signature1, signature2 : type.SortedFunctor} ->
     (op : sig2 x ty ctx) -> (sig1 + sig2) x ty ctx
 
-
-sum : {type : Type} -> (signatures : List $ (String, SortedFunctor {type})) ->
-  SortedFunctor {type}
+sum : (signatures : List $ (String, type.SortedFunctor)) ->
+  type.SortedFunctor
 (sum signatures) x ty ctx = Any (\(name,sig) => sig x ty ctx) signatures
 
-prod : {type : Type} -> (signatures : List $ SortedFunctor {type}) ->
-  SortedFunctor {type}
+prod : (signatures : List $ type.SortedFunctor) ->
+  type.SortedFunctor
 (prod signatures) x ty ctx = All (\sig => sig x ty ctx) signatures
 
-bind : {type : Type} -> (tys : Ctx {Ty = type}) ->  SortedFunctor {type}
+bind : (tys : type.Ctx) -> type.SortedFunctor
 bind tys = (<<< tys)
 
 infixr 3 -:>
 
 data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
 
-data STLC : SortedFunctor {type = TypeSTLC} where
+data STLC : TypeSTLC .SortedFunctor  where
   App : (f : a (ty1 -:> ty2) ctx) -> (x : a ty1 ctx) -> STLC a ty2 ctx
-  Lam : (body : a ty2 (ctx :< ty1)) ->
+  Lam : (x : String) ->
+        (body : a ty2 (ctx :< (x :- ty1))) ->
         STLC a (ty1 -:> ty2) ctx
 
 foo : STLC .Term Var (B -:> (B -:> B) -:> B) [<]
-foo = Op (Lam (Op (Lam (Op (App (Va Here) (Op (App (Va Here) (Va (There Here)))))))))
+foo = Op $ Lam "x" $
+      Op $ Lam "f" $
+      Op $ App (Va $ %% "f")
+               (Va $ %% "x")