From 4d12989a415be4fa8249f1966f431421cd579e80 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Tue, 25 Nov 2025 15:55:27 +0100
Subject: [PATCH 1/7] Fix whitespace

---
 src/LambdaBox/Term.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/LambdaBox/Term.hs b/src/LambdaBox/Term.hs
index ed3777b..a7312fd 100644
--- a/src/LambdaBox/Term.hs
+++ b/src/LambdaBox/Term.hs
@@ -56,10 +56,10 @@ instance Pretty Term where
             getLams t = ([], t)
 
             (ns, t') = getLams t
-        in 
+        in
         mparens (p > 0) $
         hang ("λ" <+> sep (map pretty (n:ns)) <+> "→") 2 $ pretty t'
-        
+
 
       LLetIn n e t ->
         mparens (p > 0) $ sep

From 956c90efe5f42589333a2cd47465f2b4ddbbbc5d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Tue, 25 Nov 2025 16:27:24 +0100
Subject: [PATCH 2/7] Remove "term" parameter from Def

---
 src/CoqGen.hs         | 2 +-
 src/LambdaBox/Term.hs | 8 ++++----
 src/SExpr.hs          | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/CoqGen.hs b/src/CoqGen.hs
index ea1697f..86e0733 100644
--- a/src/CoqGen.hs
+++ b/src/CoqGen.hs
@@ -88,7 +88,7 @@ instance ToCoq t Inductive where
            , ("inductive_ind",  pcoq t indInd)
            ]
 
-instance ToCoq t d => ToCoq t (Def d) where
+instance ToCoq t Def where
   pcoq t Def{..} =
     record [ ("dname", pcoq t dName)
            , ("dbody", pcoq t dBody)
diff --git a/src/LambdaBox/Term.hs b/src/LambdaBox/Term.hs
index a7312fd..7a84dbb 100644
--- a/src/LambdaBox/Term.hs
+++ b/src/LambdaBox/Term.hs
@@ -8,14 +8,14 @@ import LambdaBox.Names
 
 
 -- | Definition component in a mutual fixpoint.
-data Def t = Def
+data Def = Def
   { dName :: Name
-  , dBody :: t
+  , dBody :: Term
   , dArgs :: Int
   }
 
 -- | Mutual components of a fixpoint.
-type MFixpoint = [Def Term]
+type MFixpoint = [Def]
 
 -- | λ□ terms
 data Term
@@ -39,7 +39,7 @@ data Term
       Int       -- ^ Index of the fixpoint we keep.
 
 
-instance Pretty t => Pretty (Def t) where
+instance Pretty Def where
   -- prettyPrec _ (Def s _ _) = pretty s
   prettyPrec _ (Def _ t _) = pretty t
 
diff --git a/src/SExpr.hs b/src/SExpr.hs
index 994f6d3..2bc695c 100644
--- a/src/SExpr.hs
+++ b/src/SExpr.hs
@@ -85,7 +85,7 @@ instance ToSexp t KerName where
 instance ToSexp t Inductive where
   toSexp t Inductive{..} = ctor t "inductive" [S indMInd, S indInd]
 
-instance ToSexp t d => ToSexp t (Def d) where
+instance ToSexp t Def where
   toSexp t Def{..} = ctor t "def" [S dName, S dBody, S dArgs]
 
 instance ToSexp t Term where

From 078c004278f237679ab637f2cf2ef940d1853b17 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Wed, 26 Nov 2025 12:08:36 +0100
Subject: [PATCH 3/7] Add variable to agda2lambox binary in Makefile

---
 Makefile                            |  8 ++--
 src/Agda2Lambox/Compile/Function.hs |  4 +-
 src/Agda2Lambox/Compile/Target.hs   |  2 +-
 src/Agda2Lambox/Compile/Term.hs     | 14 +++---
 src/Agda2Lambox/Compile/Utils.hs    |  2 +-
 src/CoqGen.hs                       |  6 +--
 src/LambdaBox/Env.hs                |  2 +-
 src/LambdaBox/Term.hs               | 66 ++++++++++++++++-------------
 src/SExpr.hs                        |  6 +--
 9 files changed, 59 insertions(+), 51 deletions(-)

diff --git a/Makefile b/Makefile
index ee52477..5f9fdee 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,12 @@
+AGDA2LAMBOX_BIN ?= agda2lambox
+
 .PHONY: default
 
 default:
 	cabal install --overwrite-policy=always
 
 %.ast:
-	agda2lambox -o build test/$*.agda
+	$(AGDA2LAMBOX_BIN) -o build test/$*.agda
 
 %.wasm: %.ast
 	lbox wasm -o demo/$@ build/$*.ast
@@ -16,7 +18,7 @@ default:
 	lbox rust -o demo/$@ build/$*.ast
 
 %.v:
-	agda2lambox -o build --rocq test/$*.agda
+	$(AGDA2LAMBOX_BIN) -o build --rocq test/$*.agda
 
 %.typed:
-	agda2lambox -o build --typed --no-blocks test/$*.agda
+	$(AGDA2LAMBOX_BIN) -o build --typed --no-blocks test/$*.agda
diff --git a/src/Agda2Lambox/Compile/Function.hs b/src/Agda2Lambox/Compile/Function.hs
index 339454c..d0159e8 100644
--- a/src/Agda2Lambox/Compile/Function.hs
+++ b/src/Agda2Lambox/Compile/Function.hs
@@ -40,7 +40,7 @@ isFunction _ = False
 
 
 -- | Convert a function body to a Lambdabox term.
-compileFunctionBody :: [QName] -> Definition -> CompileM LBox.Term
+compileFunctionBody :: [QName] -> Definition -> CompileM (LBox.Term t)
 compileFunctionBody ms Defn{defName, theDef} = do
   Just t <- liftTCM $ treeless defName
 
@@ -94,7 +94,7 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
     --                they should be eta-expanded somehow,
     --                OR treated like projections
 
-  let builder :: LBox.Term -> Maybe (LBox.GlobalDecl t)
+  let builder :: LBox.Term t -> Maybe (LBox.GlobalDecl t)
       builder = Just . ConstantDecl . ConstantBody typ . Just
 
   -- if the function is not recursive, just compile the body
diff --git a/src/Agda2Lambox/Compile/Target.hs b/src/Agda2Lambox/Compile/Target.hs
index 737cd70..804b240 100644
--- a/src/Agda2Lambox/Compile/Target.hs
+++ b/src/Agda2Lambox/Compile/Target.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE DataKinds, GADTs, FlexibleInstances #-}
 -- | Compile targets for the backend
-module Agda2Lambox.Compile.Target 
+module Agda2Lambox.Compile.Target
   ( Typing(..)
   , Target(..)
   , WhenTyped(..)
diff --git a/src/Agda2Lambox/Compile/Term.hs b/src/Agda2Lambox/Compile/Term.hs
index 1902fc9..7d51950 100644
--- a/src/Agda2Lambox/Compile/Term.hs
+++ b/src/Agda2Lambox/Compile/Term.hs
@@ -78,11 +78,11 @@ compileTerm
   :: [QName]
      -- ^ Local fixpoints.
   -> TTerm
-  -> CompileM LBox.Term
+  -> CompileM (LBox.Term t)
 compileTerm ms = runC . withMutuals ms . compileTermC
 
 -- | Convert a treeless term to its λ□ equivalent.
-compileTermC :: TTerm -> C LBox.Term
+compileTermC :: TTerm -> C (LBox.Term t)
 compileTermC = \case
 
   TVar  n -> do
@@ -126,7 +126,7 @@ compileTermC = \case
     ces <- traverse compileTermC es
     pure $ foldl' LApp cu ces
 
-  TLam t -> underBinder $ LLambda Anon <$> compileTermC t
+  TLam t -> underBinder $ LLambda Anon undefined <$> compileTermC t
 
   TLit l -> compileLit l
 
@@ -151,7 +151,7 @@ compileTermC = \case
 
   TCoerce tt  -> genericError "Coerces not supported."
 
-compileLit :: Literal -> C LBox.Term
+compileLit :: Literal -> C (LBox.Term t)
 compileLit = \case
 
   LitNat i -> do
@@ -160,8 +160,8 @@ compileLit = \case
     qs <- liftTCM $ getBuiltinName_ builtinSuc
     lift do
       requireDef qn
-      iterate (toConApp qs . singleton =<<) 
-              (toConApp qz []) 
+      iterate (toConApp qs . singleton =<<)
+              (toConApp qz [])
         !! fromInteger i
 
   l -> genericError $ "unsupported literal: " <> prettyShow l
@@ -191,7 +191,7 @@ compileCaseType = \case
 --   perhaps there's already a treeless translation to prevent this
 --   to inverstigate...
 
-compileAlt :: TAlt -> C ([LBox.Name], LBox.Term)
+compileAlt :: TAlt -> C ([LBox.Name], (LBox.Term t))
 compileAlt = \case
   TACon{..}   -> let names = take aArity $ repeat LBox.Anon
                  in (names,) <$> underBinders aArity (compileTermC aBody)
diff --git a/src/Agda2Lambox/Compile/Utils.hs b/src/Agda2Lambox/Compile/Utils.hs
index ea704d6..08f08bb 100644
--- a/src/Agda2Lambox/Compile/Utils.hs
+++ b/src/Agda2Lambox/Compile/Utils.hs
@@ -78,7 +78,7 @@ toInductive q = do
 
 
 -- | Compile a constructor application to λ□.
-toConApp :: QName -> [LBox.Term] -> CompileM LBox.Term
+toConApp :: QName -> [LBox.Term t] -> CompileM (LBox.Term t)
 toConApp qn es = do
   dt   <- getConstructorData qn
   ctrs <- liftTCM $ getConstructors dt
diff --git a/src/CoqGen.hs b/src/CoqGen.hs
index 86e0733..29f5880 100644
--- a/src/CoqGen.hs
+++ b/src/CoqGen.hs
@@ -88,18 +88,18 @@ instance ToCoq t Inductive where
            , ("inductive_ind",  pcoq t indInd)
            ]
 
-instance ToCoq t Def where
+instance ToCoq t (Def t') where
   pcoq t Def{..} =
     record [ ("dname", pcoq t dName)
            , ("dbody", pcoq t dBody)
            , ("rarg",  pcoq t dArgs)
            ]
 
-instance ToCoq t Term where
+instance ToCoq t (Term t') where
   pcoqP p t v = case v of
     LBox                -> ctorP p "tBox"       []
     LRel k              -> ctorP p "tRel"       [pretty k]
-    LLambda n u         -> ctorP p "tLambda"    [pcoq t n, pcoqP 10 t u]
+    LLambda n _ u       -> ctorP p "tLambda"    [pcoq t n, pcoqP 10 t u]
     LLetIn n u v        -> ctorP p "tLetIn"     [pcoq t n, pcoqP 10 t u, pcoqP 10 t v]
     LApp u v            -> ctorP p "tApp"       [pcoqP 10 t u, pcoqP 10 t v]
     LConst c            -> ctorP p "tConst"     [pcoqP 10 t c]
diff --git a/src/LambdaBox/Env.hs b/src/LambdaBox/Env.hs
index e038e54..7b98a06 100644
--- a/src/LambdaBox/Env.hs
+++ b/src/LambdaBox/Env.hs
@@ -109,7 +109,7 @@ data MutualInductiveBody t = MutualInductive
 -- | Definition of a constant in the environment
 data ConstantBody t = ConstantBody
   { cstType :: WhenTyped t ([Name], LBox.Type)
-  , cstBody :: Maybe Term
+  , cstBody :: Maybe (Term t)
   }
 
 -- | Global declarations.
diff --git a/src/LambdaBox/Term.hs b/src/LambdaBox/Term.hs
index 7a84dbb..be0ea87 100644
--- a/src/LambdaBox/Term.hs
+++ b/src/LambdaBox/Term.hs
@@ -1,58 +1,64 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
 -- | Definition of λ□ terms.
 module LambdaBox.Term where
 
 import Data.Bifunctor (first)
 import Agda.Syntax.Common.Pretty
+import Agda2Lambox.Compile.Target
 import LambdaBox.Names
+import LambdaBox.Type
 
 
 -- | Definition component in a mutual fixpoint.
-data Def = Def
-  { dName :: Name
-  , dBody :: Term
-  , dArgs :: Int
-  }
+data Def (t :: Typing) where
+  Def :: { dName :: Name , dBody :: Term t , dArgs :: Int } -> Def t
 
 -- | Mutual components of a fixpoint.
-type MFixpoint = [Def]
+type MFixpoint t = [Def t]
 
 -- | λ□ terms
-data Term
-  = LBox          -- ^ Proofs and erased terms
-  | LRel Int      -- ^ Bound variable, with de Bruijn index
-  | LLambda Name Term  -- ^ Lambda abstraction
-  | LLetIn Name Term Term
+data Term (t :: Typing) where
+  LBox :: Term t -- ^ Proofs and erased terms
+  LRel :: Int -> Term t -- ^ Bound variable, with de Bruijn index
+  LLambda :: Name -> WhenTyped t Type -> Term t -> Term t -- ^ Lambda abstraction
+  LLetIn :: Name -> Term t -> Term t -> Term t
       -- ^ Let bindings.
       --   Unused in the backend, since Agda itself no longer has let bindings
       --   in the concrete syntac.
-  | LApp Term Term                   -- ^ Term application
-  | LConst KerName                   -- ^ Named constant.
-  | LConstruct Inductive Int [Term]  -- ^ Inductive constructor.
-  | LCase              -- ^ Pattern-matching case construct.
-      Inductive        -- ^ Inductive type we cae on.
-      Int              -- ^ Number of parameters
-      Term             -- ^ Discriminee
-      [([Name], Term)] -- ^ Branches
-  | LFix        -- ^ Fixpoint combinator.
-      MFixpoint
-      Int       -- ^ Index of the fixpoint we keep.
-
-
-instance Pretty Def where
+  LApp :: Term t -> Term t -> Term t -- ^ Term application
+  LConst :: KerName -> Term t -- ^ Named constant.
+  LConstruct
+    :: Inductive
+    -> Int
+    -> [Term t]
+    -> Term t  -- ^ Inductive constructor.
+  LCase -- ^ Pattern-matching case construct.
+    :: Inductive          -- ^ Inductive type we case on.
+    -> Int                -- ^ Number of parameters
+    -> Term t             -- ^ Discriminee
+    -> [([Name], Term t)] -- ^ Branches
+    -> Term t
+  LFix -- ^ Fixpoint combinator.
+    :: MFixpoint t
+    -> Int       -- ^ Index of the fixpoint we keep.
+    -> Term t
+
+instance Pretty (Def t) where
   -- prettyPrec _ (Def s _ _) = pretty s
   prettyPrec _ (Def _ t _) = pretty t
-
-instance Pretty Term where
+--
+instance Pretty (Term t) where
   prettyPrec p v =
     case v of
       LBox   -> "□"
 
       LRel k -> "@" <> pretty k
 
-      LLambda n t ->
-        let getLams :: Term -> ([Name], Term)
-            getLams (LLambda n t) = first (n:) $ getLams t
+      LLambda n _ t ->
+        let getLams :: Term t -> ([Name], Term t)
+            getLams (LLambda n _ t) = first (n:) $ getLams t
             getLams t = ([], t)
 
             (ns, t') = getLams t
diff --git a/src/SExpr.hs b/src/SExpr.hs
index 2bc695c..ba317ae 100644
--- a/src/SExpr.hs
+++ b/src/SExpr.hs
@@ -85,14 +85,14 @@ instance ToSexp t KerName where
 instance ToSexp t Inductive where
   toSexp t Inductive{..} = ctor t "inductive" [S indMInd, S indInd]
 
-instance ToSexp t Def where
+instance ToSexp t (Def t') where
   toSexp t Def{..} = ctor t "def" [S dName, S dBody, S dArgs]
 
-instance ToSexp t Term where
+instance ToSexp t (Term t') where
   toSexp t = \case
     LBox                -> ctor t "tBox"       []
     LRel k              -> ctor t "tRel"       [S k]
-    LLambda n u         -> ctor t "tLambda"    [S n, S u]
+    LLambda n _ u       -> ctor t "tLambda"    [S n, S u]
     LLetIn n u v        -> ctor t "tLetIn"     [S n, S u, S v]
     LApp u v            -> ctor t "tApp"       [S u, S v]
     LConst c            -> ctor t "tConst"     [S c]

From 36907738a1d2cc698bf3d5062d67f91482a37c33 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Thu, 27 Nov 2025 11:56:03 +0100
Subject: [PATCH 4/7] Refactor to accomodate types

---
 src/Agda2Lambox/Compile.hs            | 49 +++++++++---------
 src/Agda2Lambox/Compile/Function.hs   | 14 +++---
 src/Agda2Lambox/Compile/Inductive.hs  | 20 ++++----
 src/Agda2Lambox/Compile/Target.hs     |  5 +-
 src/Agda2Lambox/Compile/Term.hs       | 11 ++--
 src/Agda2Lambox/Compile/TypeScheme.hs |  2 +-
 src/CoqGen.hs                         | 16 ++++--
 src/LambdaBox/Env.hs                  | 72 ++++++++++++++++++++++++---
 src/LambdaBox/Term.hs                 | 31 +++++++++---
 src/Main.hs                           |  2 +-
 src/SExpr.hs                          | 15 ++++--
 11 files changed, 168 insertions(+), 69 deletions(-)

diff --git a/src/Agda2Lambox/Compile.hs b/src/Agda2Lambox/Compile.hs
index 625dc07..b0da518 100644
--- a/src/Agda2Lambox/Compile.hs
+++ b/src/Agda2Lambox/Compile.hs
@@ -7,6 +7,7 @@ import Control.Monad.IO.Class ( liftIO )
 import Data.IORef
 
 import Control.Monad.State
+import Data.Bifunctor (bimap)
 
 import Agda.Compiler.Backend
 import Agda.Syntax.Internal ( QName )
@@ -30,54 +31,53 @@ import Agda2Lambox.Compile.Type       ( compileTopLevelType )
 
 import LambdaBox ( emptyName, emptyDecl )
 import LambdaBox.Names
-import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
+import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), GlobalTermDecl(..), GlobalTypeDecl(..), ConstantBody(..))
 import LambdaBox.Term (Term(LBox))
 
 
 
 -- | Compile the given names into to a λ□ environment.
-compile :: Target t -> [QName] -> CompileM (GlobalEnv t)
-compile t qs = do
-  items <- compileLoop (compileDefinition t) qs
+compile :: [QName] -> CompileM (GlobalEnv Typed)
+compile qs = do
+  items <- compileLoop compileDefinition qs
   pure $ GlobalEnv $ map itemToEntry items ++ [(emptyName, emptyDecl t)]
   where
-    itemToEntry :: CompiledItem (GlobalDecl t) -> (KerName, GlobalDecl t)
-    itemToEntry CompiledItem{..} = (qnameToKName itemName, itemValue)
-
-
-compileDefinition :: Target t -> Definition -> CompileM (Maybe (GlobalDecl t))
-compileDefinition target defn@Defn{..} = setCurrentRange defName do
+    itemToEntry :: CompiledItem (Either (GlobalTermDecl Typed) (GlobalTypeDecl Typed))
+                    -> GlobalDecl Typed
+    itemToEntry CompiledItem{..} = case itemValue of
+      Left d -> GlobalTermDecl (qnameToKName itemName, d)
+      Right d -> GlobalTypeDecl (Some (qnameToKName itemName, d))
+
+compileDefinition :: Definition -> CompileM (Maybe (Either (GlobalTermDecl Typed) (GlobalTypeDecl Typed)))
+compileDefinition defn@Defn{..} = setCurrentRange defName do
   reportSDoc "agda2lambox.compile" 1 $ "Compiling definition: " <+> prettyTCM defName
 
   -- we skip definitions introduced by module application
 
   if defCopy then pure Nothing else do
 
-  typ <- whenTyped target $ compileTopLevelType defType
+  typ <- Some <$> compileTopLevelType defType
 
   -- logical definitions are immediately compiled to □
   ifM (liftTCM $ isLogical $ Arg defArgInfo defType)
-     (pure $ Just $ ConstantDecl $ ConstantBody typ $ Just LBox) do
+     (pure $ Just . Left $ ConstantDecl $ ConstantBody typ $ Just LBox) do
 
   case theDef of
     PrimitiveSort{}    -> pure Nothing
     GeneralizableVar{} -> pure Nothing
 
     Axiom{} -> do
-      typ <- whenTyped target $ compileTopLevelType defType
-      pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+      typ <- Some <$> compileTopLevelType defType
+      pure $ Just . Left $ ConstantDecl $ ConstantBody typ Nothing
 
     Constructor{conData} -> Nothing <$ requireDef conData
 
     Function{} -> do
-      ifNotM (liftTCM $ isArity defType) (compileFunction target defn) do
-        -- it's a type scheme
-        case target of
-          ToUntyped -> pure Nothing
-          -- we only compile it with --typed
-          ToTyped   -> Just <$> compileTypeScheme defn
+      ifNotM (liftTCM $ isArity defType)
+        ((Left <$>) <$> compileFunction defn)
+        ((Right <$>) <$> Just <$> compileTypeScheme defn)
 
-    d | isDataOrRecDef d -> compileInductive target defn
+    d | isDataOrRecDef d -> (Left <$>) <$> compileInductive defn
 
     Primitive{..} -> do
       reportSDoc "agda2lambox.compile" 5 $
@@ -113,12 +113,13 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
           liftTCM $ modifyGlobalDefinition defName $ const defn'
 
           -- and then we compile it as a regular function
-          compileFunction target defn'
+          (Left <$>) <$> compileFunction defn'
 
         -- otherwise, compiling it as an axiom
         _ -> do
           reportSDoc "agda2lambox.compile" 5 $ "Compiling it to an axiom."
-          typ <- whenTyped target $ compileTopLevelType defType
-          pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+            "Compiling it to an axiom."
+          typ <- Some <$> compileTopLevelType defType
+          pure $ Just . Left $ ConstantDecl $ ConstantBody typ Nothing
 
     _ -> genericError $ "Cannot compile: " <> prettyShow defName
diff --git a/src/Agda2Lambox/Compile/Function.hs b/src/Agda2Lambox/Compile/Function.hs
index d0159e8..b6062f0 100644
--- a/src/Agda2Lambox/Compile/Function.hs
+++ b/src/Agda2Lambox/Compile/Function.hs
@@ -40,7 +40,7 @@ isFunction _ = False
 
 
 -- | Convert a function body to a Lambdabox term.
-compileFunctionBody :: [QName] -> Definition -> CompileM (LBox.Term t)
+compileFunctionBody :: [QName] -> Definition -> CompileM (LBox.Term Typed)
 compileFunctionBody ms Defn{defName, theDef} = do
   Just t <- liftTCM $ treeless defName
 
@@ -59,9 +59,9 @@ shouldCompileFunction def@Defn{theDef} | Function{..} <- theDef
     && hasQuantityω def       -- non-erased
 
 -- | Convert a function definition to a λ□ declaration.
-compileFunction :: Target t -> Definition -> CompileM (Maybe (LBox.GlobalDecl t))
-compileFunction t defn | not (shouldCompileFunction defn) = pure Nothing
-compileFunction (t :: Target t) defn@Defn{defType} = do
+compileFunction :: Definition -> CompileM (Maybe (LBox.GlobalTermDecl Typed))
+compileFunction defn | not (shouldCompileFunction defn) = pure Nothing
+compileFunction defn@Defn{defType} = do
   let fundef@Function{funMutual = Just mutuals} = theDef defn
 
   reportSDoc "agda2lambox.compile.function" 5 $
@@ -78,7 +78,7 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
   let mnames = map defName mdefs
 
   -- (conditionally) compile type of function
-  typ <- whenTyped t $ case isRecordProjection fundef of
+  typ <- case isRecordProjection fundef of
     Nothing -> compileTopLevelType defType
 
     -- if it is a (real) projection, drop the parameters from the type
@@ -94,8 +94,8 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
     --                they should be eta-expanded somehow,
     --                OR treated like projections
 
-  let builder :: LBox.Term t -> Maybe (LBox.GlobalDecl t)
-      builder = Just . ConstantDecl . ConstantBody typ . Just
+  let builder :: LBox.Term Typed -> Maybe (LBox.GlobalTermDecl Typed)
+      builder = Just . ConstantDecl . ConstantBody (Some typ) . Just
 
   -- if the function is not recursive, just compile the body
   if null mdefs then builder <$> compileFunctionBody [] defn
diff --git a/src/Agda2Lambox/Compile/Inductive.hs b/src/Agda2Lambox/Compile/Inductive.hs
index ed2d33a..93de3da 100644
--- a/src/Agda2Lambox/Compile/Inductive.hs
+++ b/src/Agda2Lambox/Compile/Inductive.hs
@@ -35,8 +35,8 @@ import Agda2Lambox.Compile.Type
 import LambdaBox qualified as LBox
 
 -- | Toplevel conversion from a datatype/record definition to a Lambdabox declaration.
-compileInductive :: Target t -> Definition -> CompileM (Maybe (LBox.GlobalDecl t))
-compileInductive t defn@Defn{defName} = do
+compileInductive :: Definition -> CompileM (Maybe (LBox.GlobalTermDecl Typed))
+compileInductive defn@Defn{defName} = do
   mutuals <- liftTCM $ dataOrRecDefMutuals defn
 
   reportSDoc "agda2lambox.compile.inductive" 5 $
@@ -70,7 +70,7 @@ compileInductive t defn@Defn{defName} = do
     unless (all (isDataOrRecDef . theDef) defs) $
       genericError "Mutually-defined datatypes/records *and* functions not supported."
 
-    bodies <- forM defs $ actuallyConvertInductive t
+    bodies <- forM defs $ actuallyConvertInductive
 
     return $ Just $ LBox.InductiveDecl $ LBox.MutualInductive
       { indFinite = LBox.Finite -- TODO(flupe)
@@ -106,8 +106,8 @@ getBundle defn@Defn{defName, defType, theDef} =
         }
 
 
-actuallyConvertInductive :: ∀ t. Target t -> Definition -> CompileM (LBox.OneInductiveBody t)
-actuallyConvertInductive t defn = do
+actuallyConvertInductive :: Definition -> CompileM (LBox.OneInductiveBody Typed)
+actuallyConvertInductive defn = do
   let Bundle{..} = getBundle defn
 
   params <- theTel <$> telViewUpTo indPars indType
@@ -119,7 +119,7 @@ actuallyConvertInductive t defn = do
 
   addContext params do
 
-    tyvars <- whenTyped t $ forM (flattenTel params) \pdom -> do
+    tyvars <- forM (flattenTel params) \pdom -> do
       let domType = unDom pdom
       isParamLogical <- liftTCM $ isLogical pdom
       isParamArity   <- liftTCM $ isArity domType
@@ -137,15 +137,15 @@ actuallyConvertInductive t defn = do
           DataCon arity         -> arity
           RecordCon _ _ arity _ -> arity
 
-        conTypeInfo <- whenTyped t do
-          conType <- liftTCM $ (`piApplyM` pvars) . defType =<< getConstInfo cname
+        conTypeInfo <- do
+          conType <- liftTCM $ (`piApplyM` pvars) =<< defType =<< getConstInfo cname
           conTel  <- toList . theTel <$> telView conType
           compileArgs indPars conTel
 
         pure LBox.Constructor
           { cstrName  = qnameToIdent cname
           , cstrArgs  = arity
-          , cstrTypes = conTypeInfo
+          , cstrTypes = Some conTypeInfo
           }
 
     pure LBox.OneInductive
@@ -154,5 +154,5 @@ actuallyConvertInductive t defn = do
       , indKElim         = LBox.IntoAny -- TODO(flupe)
       , indCtors         = ctors
       , indProjs         = []
-      , indTypeVars      = tyvars
+      , indTypeVars      = Some tyvars
       }
diff --git a/src/Agda2Lambox/Compile/Target.hs b/src/Agda2Lambox/Compile/Target.hs
index 804b240..b90d6ef 100644
--- a/src/Agda2Lambox/Compile/Target.hs
+++ b/src/Agda2Lambox/Compile/Target.hs
@@ -9,6 +9,7 @@ module Agda2Lambox.Compile.Target
   , getUntyped
   , whenTyped
   , whenUntyped
+  , TypeErasure(..)
   ) where
 
 import Data.Foldable (Foldable(foldMap))
@@ -43,7 +44,6 @@ instance Foldable (WhenTyped t) where
   foldMap f None     = mempty
   foldMap f (Some x) = f x
 
--- | Type wrapper that contains a value iff we're in the untyped setting.
 data WhenUntyped (t :: Typing) (a :: Type) :: Type where
   NoneU ::      WhenUntyped Typed a
   SomeU :: a -> WhenUntyped Untyped   a
@@ -85,3 +85,6 @@ whenUntyped ToUntyped x = SomeU <$> x
 instance NFData (Target t) where
   rnf ToTyped   = ()
   rnf ToUntyped = ()
+
+class TypeErasure t where
+  erase :: t Typed -> t Untyped
diff --git a/src/Agda2Lambox/Compile/Term.hs b/src/Agda2Lambox/Compile/Term.hs
index 7d51950..e521241 100644
--- a/src/Agda2Lambox/Compile/Term.hs
+++ b/src/Agda2Lambox/Compile/Term.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns, DerivingVia, OverloadedStrings #-}
+{-# LANGUAGE NamedFieldPuns, DerivingVia, OverloadedStrings, DataKinds #-}
 module Agda2Lambox.Compile.Term
   ( compileTerm
   ) where
@@ -30,6 +30,7 @@ import LambdaBox ( Term(..), emptyName )
 import LambdaBox qualified as LBox
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
+import Agda2Lambox.Compile.Target
 
 
 -- * Term compilation monad
@@ -78,11 +79,11 @@ compileTerm
   :: [QName]
      -- ^ Local fixpoints.
   -> TTerm
-  -> CompileM (LBox.Term t)
+  -> CompileM (LBox.Term Typed)
 compileTerm ms = runC . withMutuals ms . compileTermC
 
 -- | Convert a treeless term to its λ□ equivalent.
-compileTermC :: TTerm -> C (LBox.Term t)
+compileTermC :: TTerm -> C (LBox.Term Typed)
 compileTermC = \case
 
   TVar  n -> do
@@ -126,7 +127,7 @@ compileTermC = \case
     ces <- traverse compileTermC es
     pure $ foldl' LApp cu ces
 
-  TLam t -> underBinder $ LLambda Anon undefined <$> compileTermC t
+  TLam t -> underBinder $ LLambda Anon (Some LBox.TBox) <$> compileTermC t
 
   TLit l -> compileLit l
 
@@ -191,7 +192,7 @@ compileCaseType = \case
 --   perhaps there's already a treeless translation to prevent this
 --   to inverstigate...
 
-compileAlt :: TAlt -> C ([LBox.Name], (LBox.Term t))
+compileAlt :: TAlt -> C ([LBox.Name], (LBox.Term Typed))
 compileAlt = \case
   TACon{..}   -> let names = take aArity $ repeat LBox.Anon
                  in (names,) <$> underBinders aArity (compileTermC aBody)
diff --git a/src/Agda2Lambox/Compile/TypeScheme.hs b/src/Agda2Lambox/Compile/TypeScheme.hs
index c712bb8..ab95927 100644
--- a/src/Agda2Lambox/Compile/TypeScheme.hs
+++ b/src/Agda2Lambox/Compile/TypeScheme.hs
@@ -13,7 +13,7 @@ import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Type
 import LambdaBox.Env
 
-compileTypeScheme :: Definition -> CompileM (GlobalDecl Typed)
+compileTypeScheme :: Definition -> CompileM (GlobalTypeDecl Typed)
 compileTypeScheme Defn{..} = do
   TelV tyargs _ <- telView defType
   liftIO $ putStrLn "compiling type scheme"
diff --git a/src/CoqGen.hs b/src/CoqGen.hs
index 29f5880..d39132c 100644
--- a/src/CoqGen.hs
+++ b/src/CoqGen.hs
@@ -180,15 +180,25 @@ instance ToCoq t (ConstantBody t) where
         ToUntyped -> []
         ToTyped   -> [("cst_type", pcoq t $ getTyped cstType)]
 
-instance ToCoq t (GlobalDecl t) where
+instance ToCoq t (GlobalTermDecl t) where
   pcoqP p t decl = case decl of
     ConstantDecl  body  -> ctorP p "ConstantDecl"  [pcoqP 10 t body]
     InductiveDecl minds -> ctorP p "InductiveDecl" [pcoqP 10 t minds]
+
+instance ToCoq t (GlobalTypeDecl t) where
+  pcoqP p t decl = case decl of
     TypeAliasDecl typ   -> ctorP p "TypeAliasDecl" [pcoqP 10 t typ]
 
+instance ToCoq t (GlobalDecl t) where
+  pcoq ToTyped decl = case decl of
+    GlobalTermDecl (kn, d) -> tpcoq ((kn, True), d)
+    GlobalTypeDecl (Some (kn, d)) -> tpcoq ((kn, True), d)
+  pcoq ToUntyped decl = case decl of
+    GlobalTermDecl (kn, d) -> upcoq ((kn, True), d)
+    GlobalTypeDecl _ -> mempty
+
 instance ToCoq t (GlobalEnv t) where
-  pcoq ToUntyped (GlobalEnv env) = upcoq env
-  pcoq ToTyped   (GlobalEnv env) = tpcoq $ flip map env \(kn, decl) -> ((kn, True), decl)
+  pcoq p (GlobalEnv env) = pcoq p $ map (pcoq p) env
 
 instance ToCoq t (LBoxModule t) where
   pcoq ToUntyped LBoxModule{..} = vsep
diff --git a/src/LambdaBox/Env.hs b/src/LambdaBox/Env.hs
index 7b98a06..a702144 100644
--- a/src/LambdaBox/Env.hs
+++ b/src/LambdaBox/Env.hs
@@ -19,6 +19,8 @@ module LambdaBox.Env where
 
 import Data.Kind ( Type )
 import Data.List.NonEmpty ( NonEmpty )
+import Data.Bifunctor ( first, second, bimap)
+import Data.Either
 
 import Agda.Syntax.Common.Pretty
 
@@ -113,13 +115,19 @@ data ConstantBody t = ConstantBody
   }
 
 -- | Global declarations.
+data GlobalTermDecl (t :: Typing) :: Type where
+  ConstantDecl  :: ConstantBody t        -> GlobalTermDecl t
+  InductiveDecl :: MutualInductiveBody t -> GlobalTermDecl t
+
+data GlobalTypeDecl (t :: Typing) :: Type where
+  TypeAliasDecl :: Maybe ([TypeVarInfo], LBox.Type) -> GlobalTypeDecl Typed
+
 data GlobalDecl (t :: Typing) :: Type where
-  ConstantDecl  :: ConstantBody t                   -> GlobalDecl t
-  InductiveDecl :: MutualInductiveBody t            -> GlobalDecl t
-  TypeAliasDecl :: Maybe ([TypeVarInfo], LBox.Type) -> GlobalDecl Typed
+  GlobalTypeDecl :: WhenTyped t (KerName, GlobalTypeDecl t) -> GlobalDecl t
+  GlobalTermDecl :: (KerName, GlobalTermDecl t) -> GlobalDecl t
 
 -- | Global environment.
-newtype GlobalEnv t = GlobalEnv [(KerName, GlobalDecl t)]
+newtype GlobalEnv t = GlobalEnv [GlobalDecl t]
 
 -- | Generated module
 data LBoxModule t = LBoxModule
@@ -127,6 +135,44 @@ data LBoxModule t = LBoxModule
   , lboxMain :: WhenUntyped t (NonEmpty KerName)
   }
 
+mkCoqMod :: Target t -> GlobalEnv Typed -> [KerName] -> CoqModule t
+mkCoqMod ToTyped env knames   = CoqModule env knames
+mkCoqMod ToUntyped env knames = erase (CoqModule env knames)
+
+-- Type Erasure
+----------------------------
+
+instance TypeErasure ConstructorBody where
+  erase Constructor {..} = Constructor cstrName cstrArgs None
+
+instance TypeErasure ProjectionBody where
+  erase Projection {..} = Projection projName None
+
+instance TypeErasure OneInductiveBody where
+  erase OneInductive {..} = OneInductive indName indPropositional indKElim None (map erase indCtors) (map erase indProjs)
+
+instance TypeErasure MutualInductiveBody where
+  erase MutualInductive {..} = MutualInductive indFinite indPars (map erase indBodies)
+
+instance TypeErasure ConstantBody where
+  erase ConstantBody {..} = ConstantBody None (erase <$> cstBody)
+
+instance TypeErasure GlobalTermDecl where
+  erase = \case
+    ConstantDecl  cbody -> ConstantDecl (erase cbody)
+    InductiveDecl mibody -> InductiveDecl (erase mibody)
+
+instance TypeErasure GlobalDecl where
+  erase = \case
+    GlobalTermDecl (kn , d) -> GlobalTermDecl (kn , erase d)
+    GlobalTypeDecl _  -> GlobalTypeDecl None
+
+instance TypeErasure GlobalEnv where
+  erase (GlobalEnv env) =
+    GlobalEnv (map erase env)
+
+instance TypeErasure CoqModule where
+  erase CoqModule {..} = CoqModule (erase coqEnv) coqPrograms
 
 -- pretty-printing
 ----------------------------
@@ -150,11 +196,11 @@ instance Pretty (OneInductiveBody t) where
     , nest 2 $ hang "constructors:" 2 $ vcat $ map pretty indCtors
     ]
 
-instance Pretty (GlobalDecl t) where
+instance Pretty (GlobalTermDecl t) where
   pretty = \case
     ConstantDecl ConstantBody{..} ->
       hang "constant declaration:" 2 $ vcat
-        [ flip foldMap cstType \(tvs, typ) -> 
+        [ flip foldMap cstType \(tvs, typ) ->
             vcat [ "type variables:" <+> pretty tvs
                  ,  "type:" <+> pretty typ
                   ]
@@ -165,12 +211,22 @@ instance Pretty (GlobalDecl t) where
       hang "mutual inductive(s):" 2 $
         vsep $ map pretty indBodies
 
+instance Pretty (GlobalTypeDecl t) where
+  pretty = \case
     TypeAliasDecl _ -> "type alias:"
 
+instance Pretty (GlobalDecl t) where
+  pretty = \case
+    GlobalTermDecl (kn , d) ->
+      hang (pretty kn <> ":") 2 (pretty d)
+    GlobalTypeDecl (Some (kn , d)) ->
+      hang (pretty kn <> ":") 2 (pretty d)
+    GlobalTypeDecl None ->
+      mempty
+
 instance Pretty (GlobalEnv t) where
   pretty (GlobalEnv env) =
-    vsep $ flip map (reverse env) \(kn, d) ->
-      hang (pretty kn <> ":") 2 (pretty d)
+    vsep $ map pretty (reverse env)
 
 instance Pretty (LBoxModule t) where
   pretty LBoxModule{..} = vcat
diff --git a/src/LambdaBox/Term.hs b/src/LambdaBox/Term.hs
index be0ea87..5aaff69 100644
--- a/src/LambdaBox/Term.hs
+++ b/src/LambdaBox/Term.hs
@@ -1,16 +1,16 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
 -- | Definition of λ□ terms.
 module LambdaBox.Term where
 
-import Data.Bifunctor (first)
+import Data.Bifunctor (first, second)
 import Agda.Syntax.Common.Pretty
 import Agda2Lambox.Compile.Target
 import LambdaBox.Names
 import LambdaBox.Type
 
-
 -- | Definition component in a mutual fixpoint.
 data Def (t :: Typing) where
   Def :: { dName :: Name , dBody :: Term t , dArgs :: Int } -> Def t
@@ -45,6 +45,21 @@ data Term (t :: Typing) where
     -> Int       -- ^ Index of the fixpoint we keep.
     -> Term t
 
+instance TypeErasure Term where
+  erase = \case
+    LBox -> LBox
+    LRel n -> LRel n
+    LLambda n _ t -> LLambda n None (erase t)
+    LLetIn n t t' -> LLetIn n (erase t) (erase t')
+    LApp t t' -> LApp (erase t) (erase t')
+    LConst n -> LConst n
+    LConstruct ind i ts -> LConstruct ind i (map erase ts)
+    LCase ind i t bs -> LCase ind i (erase t) (map (second erase) bs)
+    LFix ds i -> LFix (map erase ds) i
+
+instance TypeErasure Def where
+  erase (Def {..}) = Def dName (erase dBody) dArgs
+
 instance Pretty (Def t) where
   -- prettyPrec _ (Def s _ _) = pretty s
   prettyPrec _ (Def _ t _) = pretty t
@@ -56,15 +71,19 @@ instance Pretty (Term t) where
 
       LRel k -> "@" <> pretty k
 
-      LLambda n _ t ->
-        let getLams :: Term t -> ([Name], Term t)
-            getLams (LLambda n _ t) = first (n:) $ getLams t
+      LLambda n ty t ->
+        let getLams :: Term t -> ([(Name , WhenTyped t Type)], Term t)
+            getLams (LLambda n ty t) = first ((n,ty):) $ getLams t
             getLams t = ([], t)
 
             (ns, t') = getLams t
+
+            prettyWhenTyped :: Name -> WhenTyped t Type -> Doc
+            prettyWhenTyped n None     = pretty n
+            prettyWhenTyped n (Some t) = parens $ pretty n <+> ":" <+> pretty t
         in
         mparens (p > 0) $
-        hang ("λ" <+> sep (map pretty (n:ns)) <+> "→") 2 $ pretty t'
+        hang ("λ" <+> sep (map (uncurry prettyWhenTyped) ((n,ty):ns)) <+> "→") 2 $ pretty t'
 
 
       LLetIn n e t ->
diff --git a/src/Main.hs b/src/Main.hs
index fde2e12..fdaaff5 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -132,7 +132,7 @@ writeModule Options{..} menv IsMain m defs = do
   -- get defs annotated with a COMPILE pragma
   -- throw an error if none, when targetting untyped lbox
   mains    <- getMain optTarget programs
-  env      <- runCompile (CompileEnv optNoBlocks) $ compile optTarget defs
+  env      <- runCompile (CompileEnv optNoBlocks) $ compile defs
 
   liftIO $ createDirectoryIfMissing True outDir
 
diff --git a/src/SExpr.hs b/src/SExpr.hs
index ba317ae..4f1aa8c 100644
--- a/src/SExpr.hs
+++ b/src/SExpr.hs
@@ -6,6 +6,7 @@ module SExpr (ToSexp, prettySexp) where
 import Data.Bifunctor(bimap)
 import Data.List(intercalate)
 import Data.List.NonEmpty qualified as NEL (head)
+import Data.Maybe
 
 import Agda.Syntax.Common.Pretty
 import LambdaBox
@@ -175,15 +176,23 @@ instance ToSexp t (ConstantBody t) where
         ToTyped   -> [S $ getTyped cstType]
       ++ [S cstBody]
 
-instance ToSexp t (GlobalDecl t) where
+instance ToSexp t (GlobalTermDecl t) where
   toSexp t = \case
     ConstantDecl  body  -> ctor t "ConstantDecl"  [S body]
     InductiveDecl minds -> ctor t "InductiveDecl" [S minds]
+
+instance ToSexp t (GlobalTypeDecl t) where
+  toSexp t = \case
     TypeAliasDecl typ   -> ctor t "TypeAliasDecl" [S typ]
 
 instance ToSexp t (GlobalEnv t) where
-  toSexp t@ToUntyped (GlobalEnv env) = toSexp t env
-  toSexp t@ToTyped   (GlobalEnv env) = toSexp t $ flip map env \(kn, decl) -> ((kn, True), decl)
+  toSexp t@ToUntyped (GlobalEnv env) =
+    toSexp t . catMaybes . flip map env $ \case
+      GlobalTermDecl (kn , d) -> Just (kn , d)
+      GlobalTypeDecl _ -> Nothing
+  toSexp t@ToTyped (GlobalEnv env) = toSexp t . flip map env $ \case
+    GlobalTermDecl (kn, d) -> toSexp t ((kn, True), d)
+    GlobalTypeDecl (Some (kn, d)) -> toSexp t ((kn, True), d)
 
 instance ToSexp t (LBoxModule t) where
   toSexp t@ToUntyped LBoxModule{..} =

From f99ec77cb6043c3fe2dda07d747ef2aeff60560b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Thu, 27 Nov 2025 12:25:01 +0100
Subject: [PATCH 5/7] fix build issues

---
 src/Agda2Lambox/Compile.hs           |  5 ++---
 src/Agda2Lambox/Compile/Function.hs  |  2 +-
 src/Agda2Lambox/Compile/Inductive.hs |  2 +-
 src/LambdaBox.hs                     | 11 +++++++----
 src/LambdaBox/Env.hs                 |  9 +++------
 src/Main.hs                          |  2 +-
 6 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/Agda2Lambox/Compile.hs b/src/Agda2Lambox/Compile.hs
index b0da518..8615a8d 100644
--- a/src/Agda2Lambox/Compile.hs
+++ b/src/Agda2Lambox/Compile.hs
@@ -29,7 +29,7 @@ import Agda2Lambox.Compile.Inductive  ( compileInductive )
 import Agda2Lambox.Compile.TypeScheme ( compileTypeScheme )
 import Agda2Lambox.Compile.Type       ( compileTopLevelType )
 
-import LambdaBox ( emptyName, emptyDecl )
+import LambdaBox ( emptyGlobalDecl )
 import LambdaBox.Names
 import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), GlobalTermDecl(..), GlobalTypeDecl(..), ConstantBody(..))
 import LambdaBox.Term (Term(LBox))
@@ -40,7 +40,7 @@ import LambdaBox.Term (Term(LBox))
 compile :: [QName] -> CompileM (GlobalEnv Typed)
 compile qs = do
   items <- compileLoop compileDefinition qs
-  pure $ GlobalEnv $ map itemToEntry items ++ [(emptyName, emptyDecl t)]
+  pure $ GlobalEnv $ map itemToEntry items ++ [emptyGlobalDecl]
   where
     itemToEntry :: CompiledItem (Either (GlobalTermDecl Typed) (GlobalTypeDecl Typed))
                     -> GlobalDecl Typed
@@ -118,7 +118,6 @@ compileDefinition defn@Defn{..} = setCurrentRange defName do
         -- otherwise, compiling it as an axiom
         _ -> do
           reportSDoc "agda2lambox.compile" 5 $ "Compiling it to an axiom."
-            "Compiling it to an axiom."
           typ <- Some <$> compileTopLevelType defType
           pure $ Just . Left $ ConstantDecl $ ConstantBody typ Nothing
 
diff --git a/src/Agda2Lambox/Compile/Function.hs b/src/Agda2Lambox/Compile/Function.hs
index b6062f0..74fd037 100644
--- a/src/Agda2Lambox/Compile/Function.hs
+++ b/src/Agda2Lambox/Compile/Function.hs
@@ -108,7 +108,7 @@ compileFunction defn@Defn{defType} = do
       forM mdefs \def@Defn{defName} -> do
         body <- compileFunctionBody mnames def >>= \case
           l@LBox.LLambda{} -> pure l
-          LBox.LBox        -> pure $ LBox.LLambda LBox.Anon LBox.LBox
+          LBox.LBox        -> pure $ LBox.LLambda LBox.Anon (Some LBox.TBox) LBox.LBox
           _                -> genericError "Fixpoint body must be Lambda."
         return LBox.Def
           { dName = qnameToName defName
diff --git a/src/Agda2Lambox/Compile/Inductive.hs b/src/Agda2Lambox/Compile/Inductive.hs
index 93de3da..6d8d44c 100644
--- a/src/Agda2Lambox/Compile/Inductive.hs
+++ b/src/Agda2Lambox/Compile/Inductive.hs
@@ -138,7 +138,7 @@ actuallyConvertInductive defn = do
           RecordCon _ _ arity _ -> arity
 
         conTypeInfo <- do
-          conType <- liftTCM $ (`piApplyM` pvars) =<< defType =<< getConstInfo cname
+          conType <- liftTCM $ (`piApplyM` pvars) =<< defType <$> (getConstInfo cname)
           conTel  <- toList . theTel <$> telView conType
           compileArgs indPars conTel
 
diff --git a/src/LambdaBox.hs b/src/LambdaBox.hs
index 715b851..42ac1be 100644
--- a/src/LambdaBox.hs
+++ b/src/LambdaBox.hs
@@ -6,7 +6,7 @@ module LambdaBox
   , module LambdaBox.Type
   , module LambdaBox.Env
   , emptyName
-  , emptyDecl
+  , emptyGlobalDecl
   ) where
 
 import Control.Monad.Identity
@@ -22,8 +22,8 @@ emptyName = KerName (MPFile ["LamBox"]) "Empty"
 
 -- | Backed-in definition for the empty type.
 --   Used to discard unreachable branches in typed targets.
-emptyDecl :: Target t -> GlobalDecl t
-emptyDecl t = InductiveDecl MutualInductive
+emptyDecl :: GlobalTermDecl Typed
+emptyDecl = InductiveDecl MutualInductive
   { indFinite = Finite
   , indPars   = 0
   , indBodies = [
@@ -31,9 +31,12 @@ emptyDecl t = InductiveDecl MutualInductive
         { indName          = "Empty"
         , indPropositional = False
         , indKElim         = IntoAny
-        , indTypeVars      = runIdentity $ whenTyped t $ pure []
+        , indTypeVars      = Some []
         , indCtors         = []
         , indProjs         = []
         }
     ]
   }
+
+emptyGlobalDecl :: GlobalDecl Typed
+emptyGlobalDecl = GlobalTermDecl (emptyName, emptyDecl)
diff --git a/src/LambdaBox/Env.hs b/src/LambdaBox/Env.hs
index a702144..4f2d6cb 100644
--- a/src/LambdaBox/Env.hs
+++ b/src/LambdaBox/Env.hs
@@ -135,9 +135,9 @@ data LBoxModule t = LBoxModule
   , lboxMain :: WhenUntyped t (NonEmpty KerName)
   }
 
-mkCoqMod :: Target t -> GlobalEnv Typed -> [KerName] -> CoqModule t
-mkCoqMod ToTyped env knames   = CoqModule env knames
-mkCoqMod ToUntyped env knames = erase (CoqModule env knames)
+mkLBoxModule :: Target t -> GlobalEnv Typed -> WhenUntyped t (NonEmpty KerName) -> LBoxModule t
+mkLBoxModule ToTyped env _ = LBoxModule env NoneU
+mkLBoxModule ToUntyped env knames = LBoxModule (erase env) knames
 
 -- Type Erasure
 ----------------------------
@@ -171,9 +171,6 @@ instance TypeErasure GlobalEnv where
   erase (GlobalEnv env) =
     GlobalEnv (map erase env)
 
-instance TypeErasure CoqModule where
-  erase CoqModule {..} = CoqModule (erase coqEnv) coqPrograms
-
 -- pretty-printing
 ----------------------------
 
diff --git a/src/Main.hs b/src/Main.hs
index fdaaff5..48f965a 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -137,7 +137,7 @@ writeModule Options{..} menv IsMain m defs = do
   liftIO $ createDirectoryIfMissing True outDir
 
   let fileName = outDir </> prettyShow m
-  let lboxMod  = LBoxModule env mains
+  let lboxMod  = mkLBoxModule optTarget env mains
 
   liftIO do
     putStrLn $ "Writing " <> fileName -<.> ".txt"

From d25a767ba0dff958914f82492833e9a9b3ef5999 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Thu, 27 Nov 2025 12:26:03 +0100
Subject: [PATCH 6/7] Update flake.lock

---
 flake.lock | 74 +-----------------------------------------------------
 1 file changed, 1 insertion(+), 73 deletions(-)

diff --git a/flake.lock b/flake.lock
index d458c63..0459467 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,42 +1,5 @@
 {
   "nodes": {
-    "agda": {
-      "inputs": {
-        "flake-parts": "flake-parts",
-        "nixpkgs": "nixpkgs"
-      },
-      "locked": {
-        "lastModified": 1737271545,
-        "narHash": "sha256-qiV/tk+/b3xYPJcWVVd7x9jrQjBzl1TXHPNEQbKV2rA=",
-        "owner": "agda",
-        "repo": "agda",
-        "rev": "5c29109f8212ef61b0091d62ef9c8bfdfa16cf36",
-        "type": "github"
-      },
-      "original": {
-        "owner": "agda",
-        "repo": "agda",
-        "type": "github"
-      }
-    },
-    "flake-parts": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib"
-      },
-      "locked": {
-        "lastModified": 1701473968,
-        "narHash": "sha256-YcVE5emp1qQ8ieHUnxt1wCZCC3ZfAS+SRRWZ2TMda7E=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "34fed993f1674c8d06d58b37ce1e0fe5eebcb9f5",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
@@ -56,40 +19,6 @@
       }
     },
     "nixpkgs": {
-      "locked": {
-        "lastModified": 1735563628,
-        "narHash": "sha256-OnSAY7XDSx7CtDoqNh8jwVwh4xNL/2HaJxGjryLWzX8=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "b134951a4c9f3c995fd7be05f3243f8ecd65d798",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-24.05",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs-lib": {
-      "locked": {
-        "dir": "lib",
-        "lastModified": 1701253981,
-        "narHash": "sha256-ztaDIyZ7HrTAfEEUt9AtTDNoCYxUdSd6NrRHaYOIxtk=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "e92039b55bcd58469325ded85d4f58dd5a4eaf58",
-        "type": "github"
-      },
-      "original": {
-        "dir": "lib",
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs_2": {
       "locked": {
         "lastModified": 1763999649,
         "narHash": "sha256-TBLzlyxB8pgEXCfSjKLkNgaR4FOf3HyIa/o8yIjeMvI=",
@@ -106,9 +35,8 @@
     },
     "root": {
       "inputs": {
-        "agda": "agda",
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs"
       }
     },
     "systems": {

From 9c57a53daea0afbd7584ded1de79a642592a6286 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Thu, 27 Nov 2025 17:13:31 +0100
Subject: [PATCH 7/7] Add (bare) typechecker

---
 agda2lambox.cabal          |  1 +
 src/LambdaBox/Names.hs     |  3 ++
 src/LambdaBox/Type.hs      |  1 +
 src/LambdaBox/Typecheck.hs | 56 ++++++++++++++++++++++++++++++++++++++
 src/Main.hs                | 15 +++++++++-
 5 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 src/LambdaBox/Typecheck.hs

diff --git a/agda2lambox.cabal b/agda2lambox.cabal
index 01e8812..f30859c 100644
--- a/agda2lambox.cabal
+++ b/agda2lambox.cabal
@@ -36,6 +36,7 @@ executable agda2lambox
                        LambdaBox.Type,
                        LambdaBox.Env,
                        LambdaBox,
+                       LambdaBox.Typecheck,
                        CoqGen,
                        SExpr,
                        Paths_agda2lambox
diff --git a/src/LambdaBox/Names.hs b/src/LambdaBox/Names.hs
index aec00af..aec6e18 100644
--- a/src/LambdaBox/Names.hs
+++ b/src/LambdaBox/Names.hs
@@ -19,12 +19,14 @@ data ModPath
     -- ^ parameters of functors
   | MPDot ModPath Ident
     -- ^ submodules
+  deriving (Eq)
 
 -- | Absolute name of objects in the Rocq kernel.
 data KerName = KerName
   { kerModPath :: ModPath
   , kerName    :: Ident
   }
+  deriving (Eq)
 
 -- | Reference to an inductive datatype.
 data Inductive = Inductive
@@ -33,6 +35,7 @@ data Inductive = Inductive
   , indInd  :: Int
     -- ^ Which of those is the inductive we care about.
   }
+  deriving (Eq)
 
 -- | Names used in binders
 data Name = Anon | Named Ident
diff --git a/src/LambdaBox/Type.hs b/src/LambdaBox/Type.hs
index 153e5d1..c1cd8fd 100644
--- a/src/LambdaBox/Type.hs
+++ b/src/LambdaBox/Type.hs
@@ -15,6 +15,7 @@ data Type
       --   Uses De Bruijn *levels* and NOT indices.
   | TInd Inductive
   | TConst KerName
+  deriving (Eq)
 
 instance Pretty Type where
   prettyPrec p = \case
diff --git a/src/LambdaBox/Typecheck.hs b/src/LambdaBox/Typecheck.hs
new file mode 100644
index 0000000..b17b4c5
--- /dev/null
+++ b/src/LambdaBox/Typecheck.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE DataKinds #-}
+module LambdaBox.Typecheck where
+
+import Agda2Lambox.Compile.Target
+import LambdaBox
+import Agda.Utils.Monad
+
+type Env = Int -> Type
+
+extend :: Env -> Type -> Env
+extend env ty 0 = ty
+extend env ty i = env (i - 1)
+
+-- | Infer the type of a term
+infer :: MonadFail m => Term Typed -> Env -> m Type
+infer term env =
+  case term of
+    LBox -> return TBox
+    LRel n -> return $ env n
+    LLambda n (Some ty) b ->
+      infer b (extend env ty)
+    LLetIn n t b -> do
+      ty <- infer t env
+      ty' <- infer b (extend env ty)
+      return (TArr ty ty')
+    LApp t t' -> do
+      TArr t1 t2 <- infer t env
+      ifM (check t' t1 env)
+        (return t2)
+        (fail "Failure")
+    LConst kn -> fail "Not implemented" -- FIXME
+    LConstruct ind i ts -> fail "Not implemented" -- FIXME
+    LCase ind n t bs -> fail "Not implemented" -- FIXME
+    LFix mfix i -> fail "Not implemented" -- FIXME
+
+-- | Check a term against a type
+check :: MonadFail m => Term Typed -> Type -> Env -> m Bool
+check term ty env = case term of
+  LBox -> return $ TBox == ty
+  LRel n -> return $ env n == ty
+  LLambda n (Some ty) b -> case ty of
+    TArr t1 t2 -> check b t2 (extend env t1)
+    _ -> return False
+  LLetIn n t b -> do
+    ty' <- infer t env
+    check b ty (extend env ty')
+  LApp t t' -> do
+    TArr t1 t2 <- infer t env
+    check t' t1 env
+  LConst c -> return False
+  LConstruct ind n ts -> return False
+  LCase ind i t bs -> return False
+  LFix mfix i -> return False
+
+typecheck :: GlobalEnv Typed -> Bool
+typecheck _ = False
diff --git a/src/Main.hs b/src/Main.hs
index 48f965a..a65f9a2 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -35,6 +35,7 @@ import CoqGen    ( prettyCoq  )
 import SExpr     ( prettySexp )
 import LambdaBox.Env
 import LambdaBox.Names (KerName)
+import LambdaBox.Typecheck (typecheck)
 import Agda2Lambox.Compile.Monad (runCompile, CompileEnv(..))
 
 
@@ -48,12 +49,13 @@ data Output = RocqOutput | AstOutput
 data Options = forall t. Options
   { optOutDir   :: Maybe FilePath
   , optTarget   :: Target t
+  , optWithTC   :: Bool
   , optOutput   :: Output
   , optNoBlocks :: Bool
   }
 
 instance NFData Options where
-  rnf (Options m t o nb) = rnf m `seq` rnf t `seq` rnf o `seq` rnf nb
+  rnf (Options m t tc o nb) = rnf m `seq` rnf t `seq` rnf tc `seq` rnf o `seq` rnf nb
 
 -- | Setter for output directory option.
 outdirOpt :: Monad m => FilePath -> Options -> m Options
@@ -68,11 +70,15 @@ rocqOpt opts = return opts { optOutput = RocqOutput }
 noBlocksOpt :: Monad m => Options -> m Options
 noBlocksOpt opts = return opts { optNoBlocks = True }
 
+withTC :: Monad m => Options -> m Options
+withTC opts = return opts { optWithTC = True }
+
 -- | Default backend options.
 defaultOptions :: Options
 defaultOptions  = Options
   { optOutDir   = Nothing
   , optTarget   = ToUntyped
+  , optWithTC   = False
   , optOutput   = AstOutput
   , optNoBlocks = False
   }
@@ -97,6 +103,8 @@ agda2lambox = Backend backend
             "Write output files to DIR. (default: project root)"
           , Option ['t'] ["typed"] (NoArg typedOpt)
             "Compile to typed λ□ environments."
+          , Option "tc" ["typecheck"] (NoArg typedOpt)
+            "Typecheck output λ□."
           , Option ['c'] ["rocq"] (NoArg rocqOpt)
             "Output a Rocq file."
           , Option [] ["no-blocks"] (NoArg noBlocksOpt)
@@ -134,6 +142,11 @@ writeModule Options{..} menv IsMain m defs = do
   mains    <- getMain optTarget programs
   env      <- runCompile (CompileEnv optNoBlocks) $ compile defs
 
+  liftIO $ putStrLn $ "Typechecking generated λ□."
+  if (typecheck env)
+    then genericError "Failure"
+    else liftIO $ putStrLn "Success"
+
   liftIO $ createDirectoryIfMissing True outDir
 
   let fileName = outDir </> prettyShow m