diff --git a/Makefile b/Makefile
index 1b12bea..53c677e 100644
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,8 @@ LIBRARIES =
 
 .PHONY: app alllib clean clean-lib clean-agdai
 
-alllib: lib lib/Agda/Core/Syntax.hs lib/Agda/Core/Reduce.hs
+alllib: lib lib/Agda/Core/Syntax.hs lib/Agda/Core/Reduce.hs lib/Agda/Core/Typechecker.hs \
+  lib/Agda/Core/TCM.hs
 
 # alllib: lib lib/*.hs
 
diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda
index 11da2a0..39b818b 100644
--- a/src/Agda/Core/Context.agda
+++ b/src/Agda/Core/Context.agda
@@ -38,15 +38,15 @@ private variable
 
 lookupVar : (Γ : Context α) (@0 x : name) (p : x ∈ α) → Type α
 lookupVar CtxEmpty x p = inEmptyCase p
-lookupVar (CtxExtend Γ y s) x p = raise (rezz _) (inBindCase p
+lookupVar (CtxExtend g y s) x p = raise (rezz _) (inBindCase p
   (λ _ → s)
-  (λ q → lookupVar Γ x q))
+  (λ q → lookupVar g x q))
 
 {-# COMPILE AGDA2HS lookupVar #-}
 
-rezz-scope : (Γ : Context α) → Rezz (Scope name) α
-rezz-scope CtxEmpty = rezz _
-rezz-scope (CtxExtend Γ x _) =
-  rezzCong (λ t → (singleton x) <> t) (rezz-scope Γ)
+rezzScope : (Γ : Context α) → Rezz (Scope name) α
+rezzScope CtxEmpty = rezz _
+rezzScope (CtxExtend g x _) =
+  rezzCong (λ t → (singleton x) <> t) (rezzScope g)
 
-{-# COMPILE AGDA2HS rezz-scope #-}
+{-# COMPILE AGDA2HS rezzScope #-}
diff --git a/src/Agda/Core/Reduce.agda b/src/Agda/Core/Reduce.agda
index 29ea7ac..20842f1 100644
--- a/src/Agda/Core/Reduce.agda
+++ b/src/Agda/Core/Reduce.agda
@@ -6,7 +6,7 @@ module Agda.Core.Reduce
   (@0 globals : Globals name)
   where
 
-open import Haskell.Prelude hiding (All; coerce)
+open import Haskell.Prelude hiding (All; coerce; _,_,_) renaming (_,_ to infixr 5 _,_)
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 open import Haskell.Extra.Erase
@@ -14,6 +14,7 @@ open import Utils.Either
 
 open import Agda.Core.Syntax globals
 open import Agda.Core.Substitute globals
+open import Agda.Core.Utils
 
 private open module @0 G = Globals globals
 
@@ -148,12 +149,6 @@ opaque
 
 {-# COMPILE AGDA2HS step #-}
 
-data Fuel : Set where
-  None : Fuel
-  More : Fuel → Fuel
-
-{-# COMPILE AGDA2HS Fuel #-}
-
 -- TODO: make this into a `where` function once 
 -- https://github.com/agda/agda2hs/issues/264 is fixed
 reduceState : Rezz _ α
@@ -174,8 +169,16 @@ reduceClosed = reduce (rezz _)
 
 {-# COMPILE AGDA2HS reduceClosed #-}
 
-_reducesTo_ : (v w : Term α) → Set
-_reducesTo_ {α = α} v w = 
-  ∃ (Rezz _ α) λ r    → 
-  ∃ Fuel       λ fuel → 
-  reduce r v fuel ≡ Just w
+@0 _reducesTo_ : (v w : Term α) → Set
+_reducesTo_ {α = α} v w = Σ[ r ∈ Rezz _ α ] Σ[ f ∈ Fuel ] reduce r v f ≡ Just w
+
+reduceTo : Rezz _ α
+       → (v : Term α)
+       → Fuel
+       → Maybe (∃[ u ∈ Term α ] v reducesTo u)
+reduceTo r v f =
+  case reduce r v f of λ where
+    Nothing        → Nothing
+    (Just u) ⦃ p ⦄ → Just (u ⟨ r , f , p ⟩)
+
+{-# COMPILE AGDA2HS reduceTo #-}
diff --git a/src/Agda/Core/TCM.agda b/src/Agda/Core/TCM.agda
index a367b11..b80e0c7 100644
--- a/src/Agda/Core/TCM.agda
+++ b/src/Agda/Core/TCM.agda
@@ -1,100 +1,80 @@
+module Agda.Core.TCM where
+
+
 open import Haskell.Prelude hiding ( All; m )
 open import Scope
 open import Agda.Core.GlobalScope
+open import Agda.Core.Utils
 
-import Agda.Core.Syntax as Syntax
-
-module Agda.Core.TCM
-    {@0 name    : Set}
-    (@0 globals : Globals name)
-  where
 
-open import Agda.Core.Reduce globals
+TCError = String
+{-# COMPILE AGDA2HS TCError #-}
 
-module Pair where
-  open import Agda.Primitive
-  private variable
-    ℓ ℓ′ : Level
-  
-  record Pair (a : Set ℓ) (p : (@0 _ : a) → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
-    constructor MkPair
-    field
-      pfst : a
-      psnd : p pfst
-  open Pair public
-  {-# COMPILE AGDA2HS Pair #-}
+record TCM (a : Set) : Set where
+  constructor MkTCM
+  field runTCM : Fuel → Either TCError a
+open TCM public
+{-# COMPILE AGDA2HS TCM #-}
 
-open Pair
+tcmFuel : TCM Fuel
+tcmFuel = MkTCM Right
+{-# COMPILE AGDA2HS tcmFuel #-}
 
-pattern _⟨_⟩ a b = MkPair a b
+tcError : TCError -> TCM a
+tcError = MkTCM ∘ const ∘ Left
+{-# COMPILE AGDA2HS tcError #-}
 
-infix 4 ∃
-∃ : (a : Set) (p : @0 a → Set) → Set
-∃ a p = Pair a p
-{-# COMPILE AGDA2HS ∃ inline #-}
+private
+  fmapTCM : (a → b) → TCM a → TCM b
+  fmapTCM f = MkTCM ∘ fmap (fmap f) ∘ runTCM
+  {-# COMPILE AGDA2HS fmapTCM #-}
 
-TCError = String
-
-record TCM (a : Set) : Set where
-  constructor mkTCM
-  field
-    runTCM : Fuel → Either TCError a
+  pureTCM : a → TCM a
+  pureTCM = MkTCM ∘ const ∘ Right
+  {-# COMPILE AGDA2HS pureTCM #-}
+  
+  liftA2TCM : (a → b → c) → TCM a → TCM b → TCM c
+  liftA2TCM g ta tb = MkTCM λ f → g <$> runTCM ta f <*> runTCM tb f
+  {-# COMPILE AGDA2HS liftA2TCM #-}
 
-tcmFuel : TCM Fuel
-tcmFuel = mkTCM (λ f → Right f)
-
-fmapTCM : (a → b) → TCM a → TCM b
-fmapTCM f (mkTCM runTCM) = mkTCM (fmap (fmap f) runTCM)
-
-pureTCM : a → TCM a
-pureTCM a = mkTCM (pure (pure a))
-
-liftA2TCM : (a → b → c) → TCM a → TCM b → TCM c
-liftA2TCM f (mkTCM ta) (mkTCM tb) = mkTCM (liftA2Fuel (liftA2Either f) ta tb)
-  where
-    liftA2Fuel : {a b c f : Set} → (a → b → c) → (f → a) → (f → b) → (f → c)
-    liftA2Fuel f a b = f <$> a <*> b
-    liftA2Either : {a b c e : Set} → (a → b → c) → Either e a → Either e b → Either e c
-    liftA2Either f a b = f <$> a <*> b
-
-bindTCM : TCM a → (a → TCM b) → TCM b
-bindTCM ma mf = mkTCM (bindTCM' ma mf)
-  where
-  bindTCM' : TCM a → (a → TCM b) → Fuel → Either TCError b
-  bindTCM' (mkTCM ma) mf f with (ma f)
-  ... | Left e = Left e
-  ... | Right v = TCM.runTCM (mf v) f
+  bindTCM : TCM a → (a → TCM b) → TCM b
+  bindTCM ma mf = MkTCM λ f → do v ← runTCM ma f ; runTCM (mf v) f
+  {-# COMPILE AGDA2HS bindTCM #-}
 
 instance
   iFunctorTCM : Functor TCM
-  Functor.fmap iFunctorTCM = fmapTCM
-  Functor._<$>_ iFunctorTCM = fmapTCM
-  Functor._<&>_ iFunctorTCM = λ x f → fmapTCM f x
-  Functor._<$_ iFunctorTCM = λ x m → fmapTCM (λ b → x {{b}}) m
-  Functor._$>_ iFunctorTCM = λ m x → fmapTCM (λ b → x {{b}}) m
-  Functor.void iFunctorTCM = fmapTCM (const tt)
+  iFunctorTCM .fmap  = fmapTCM
+  iFunctorTCM ._<$>_ = fmapTCM
+  iFunctorTCM ._<&>_ = λ x f → fmapTCM f x
+  iFunctorTCM ._<$_  = λ x m → fmapTCM (λ b → x {{b}}) m
+  iFunctorTCM ._$>_  = λ m x → fmapTCM (λ b → x {{b}}) m
+  iFunctorTCM .void  = fmapTCM (const tt)
+  {-# COMPILE AGDA2HS iFunctorTCM #-}
 
+instance
   iApplicativeTCM : Applicative TCM
-  Applicative.pure iApplicativeTCM = pureTCM
-  Applicative._<*>_ iApplicativeTCM = liftA2TCM id
-  Applicative.super iApplicativeTCM = iFunctorTCM
-  Applicative._<*_ iApplicativeTCM = liftA2TCM (λ z _ → z)
-  Applicative._*>_ iApplicativeTCM = liftA2TCM (λ _ z → z)
+  iApplicativeTCM .pure  = pureTCM
+  iApplicativeTCM ._<*>_ = liftA2TCM id
+  iApplicativeTCM ._<*_  = liftA2TCM (λ z _ → z)
+  iApplicativeTCM ._*>_  = liftA2TCM (λ _ z → z)
+  {-# COMPILE AGDA2HS iApplicativeTCM #-}
 
+instance
   iMonadTCM : Monad TCM
-  Monad._>>=_ iMonadTCM = bindTCM
-  Monad.super iMonadTCM = iApplicativeTCM
-  Monad.return iMonadTCM = pureTCM
-  Monad._>>_ iMonadTCM = λ m m₁ → bindTCM m (λ x → m₁ {{x}})
-  Monad._=<<_ iMonadTCM = flip bindTCM
+  iMonadTCM ._>>=_  = bindTCM
+  iMonadTCM .return = pureTCM
+  iMonadTCM ._>>_   = λ x y → bindTCM x (λ z → y {{z}})
+  iMonadTCM ._=<<_  = flip bindTCM
+  {-# COMPILE AGDA2HS iMonadTCM #-}
 
 liftEither : Either TCError a → TCM a
-liftEither (Left e) = mkTCM λ f → Left e
-liftEither (Right v) = mkTCM λ f → Right v
+liftEither (Left e) = MkTCM λ f → Left e
+liftEither (Right v) = MkTCM λ f → Right v
+
+{-# COMPILE AGDA2HS liftEither #-}
 
 liftMaybe : Maybe a → TCError → TCM a
-liftMaybe Nothing e = mkTCM λ f → Left e
-liftMaybe (Just x) e = mkTCM λ f → Right x
+liftMaybe Nothing e = MkTCM λ f → Left e
+liftMaybe (Just x) e = MkTCM λ f → Right x
 
-tcError : TCError -> TCM a
-tcError e = mkTCM λ f → Left e
+{-# COMPILE AGDA2HS liftMaybe #-}
diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda
index dc70cca..cc85d4d 100644
--- a/src/Agda/Core/Typechecker.agda
+++ b/src/Agda/Core/Typechecker.agda
@@ -1,5 +1,8 @@
 {-# OPTIONS --allow-unsolved-metas #-}
-open import Haskell.Prelude hiding ( All; m )
+open import Haskell.Prelude
+  hiding ( All; m; _,_,_)
+  renaming (_,_ to infixr 5 _,_)
+
 open import Scope
 
 open import Agda.Core.GlobalScope using (Globals)
@@ -19,53 +22,42 @@ open import Agda.Core.Conversion globals defType
 open import Agda.Core.Typing globals defType
 open import Agda.Core.Reduce globals
 open import Agda.Core.Substitute globals
-open import Agda.Core.TCM globals
+open import Agda.Core.TCM
+open import Agda.Core.Utils
 
 open import Haskell.Law.Equality
-open import Haskell.Extra.Erase
-open import Haskell.Extra.Refinement using (value; proof) renaming (_⟨_⟩ to ⟨_,_⟩)
 
 private variable
   @0 α : Scope name
   Γ    : Context α
            
-private
-  -- TODO: move this to some utils file
-  subst' : (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
-  subst' p refl z = z
-  {-# COMPILE AGDA2HS subst' transparent #-}
-
 postulate
-  inferSort : (t : Type α) → TCM (∃ (Sort α) (λ s → Γ ⊢ t ∶ TSort s))
-  convert : (@0 ty : Type α) (@0 a b : Term α) → Conv {α = α} Γ ty a b
+  inferSort : (t : Type α) → TCM (Σ[ s ∈ Sort α ] Γ ⊢ t ∶ TSort s)
+  convert : (@0 ty : Type α) (@0 a b : Term α) → Γ ⊢ a ≅ b ∶ ty
 
-inferType : (te : Term α)
-          → TCM (∃ (Type α) (λ ty → Γ ⊢ te ∶ ty))
+inferType : ∀ u   → TCM (Σ[ t ∈ Type α ] Γ ⊢ u ∶ t)
+{-# COMPILE AGDA2HS inferType #-}
 
-checkType : (te : Term α) (ty : Type α)
-          → TCM (Γ ⊢ te ∶ ty)
+checkType : ∀ u t → TCM (Γ ⊢ u ∶ t)
+{-# COMPILE AGDA2HS checkType #-}
 
-inferVar : (@0 x : name)
-           (p : x ∈ α)
-         → TCM (∃ (Type α) (λ t → Γ ⊢ TVar x p ∶ t))
-inferVar {Γ = Γ} x p = return ( (lookupVar Γ x p) ⟨ TyTVar p ⟩)
+inferVar : ∀ (@0 x) (p : x ∈ α) → TCM (Σ[ t ∈ Type α ] Γ ⊢ TVar x p ∶ t)
+inferVar {Γ = g} x p = return (lookupVar g x p , TyTVar p)
 
-inferApp : (u : Term α)
-           (e : Elim α)
-           → TCM (∃ (Type α) (λ ty → Γ ⊢ TApp u e ∶ ty))
+inferApp : ∀ u e → TCM (Σ[ t ∈ Type α ] Γ ⊢ TApp u e ∶ t)
 inferApp {Γ = Γ} u (Syntax.EArg v) = do
-  let r = rezz-scope Γ
+  let r = rezzScope Γ
   fuel ← tcmFuel
 
-  tu  ⟨ gtu ⟩ ← inferType {Γ = Γ} u
-  stu ⟨ _   ⟩ ← inferSort {Γ = Γ} tu
+  tu  , gtu ← inferType {Γ = Γ} u
+  stu , _   ← inferSort {Γ = Γ} tu
 
   case reduce r tu fuel of λ where
     Nothing → tcError "not enough fuel to reduce term"
     (Just (TPi x sa sr at rt)) ⦃ p ⦄ → do
       gtv ← checkType {Γ = Γ} v at
-      let gc = CRedL ⟨ r , ⟨ fuel , p ⟩ ⟩ CRefl
-      pure $ substTop r v rt ⟨ TyAppE gtu (TyArg {k = funSort sa sr} gc gtv) ⟩
+      let gc = CRedL (r , fuel , p ) CRefl
+      pure $ substTop r v rt , TyAppE gtu (TyArg {k = funSort sa sr} gc gtv)
     (Just _) → tcError "couldn't reduce term to pi type"
 
 inferApp {Γ = Γ} u (Syntax.EProj x x₁) = tcError "not implemented"
@@ -75,27 +67,24 @@ inferPi : (@0 x : name)
           (su sv : Sort α)
           (u : Term α)
           (v : Term (x ◃ α))
-          → TCM (∃ (Type α) (λ ty → Γ ⊢ TPi x su sv u v ∶ ty))
+          → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TPi x su sv u v ∶ ty)
 inferPi {Γ = Γ} x su sv u v = do
   tu <- checkType {Γ = Γ} u (TSort su)
   tv <- checkType {Γ = Γ , x ∶ u} v (TSort (weakenSort (subWeaken subRefl) sv))
-  return ( (TSort (funSort su sv)) ⟨ TyPi tu tv ⟩ )
+  pure $ TSort (funSort su sv) , TyPi tu tv
 
-inferTySort : (s : Sort α)
-            → TCM (∃ (Type α) (λ ty → Γ ⊢ TSort s ∶ ty))
-inferTySort (STyp x) = return (TSort (STyp (suc x)) ⟨ TyType ⟩)
+inferTySort : (s : Sort α) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TSort s ∶ ty)
+inferTySort (STyp x) = pure $ TSort (STyp (suc x)) , TyType
 
-inferDef : (@0 f : name)
-           (p : f ∈ defScope )
-         → TCM (∃ (Type α) (λ ty → Γ ⊢ TDef f p ∶ ty))
-inferDef f p = return (((weaken subEmpty (defType ! f))) ⟨ TyDef p ⟩)
+inferDef : (@0 f : name) (p : f ∈ defScope ) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TDef f p ∶ ty)
+inferDef f p = pure $ weaken subEmpty (defType ! f) , TyDef p
 
 checkLambda : (@0 x : name)
               (u : Term (x ◃ α))
               (ty : Type α)
               → TCM (Γ ⊢ TLam x u ∶ ty)
 checkLambda {Γ = Γ} x u (TPi y su sv tu tv) = do
-  d ← checkType {Γ = Γ , x ∶ tu} u (renameTop (rezz-scope Γ) tv)
+  d ← checkType {Γ = Γ , x ∶ tu} u (renameTop (rezzScope Γ) tv)
   return (TyLam d)
 --FIXME: reduce ty and see if it's a Pi
 checkLambda x u _ = tcError "can't check lambda against a type that isn't a Pi"
@@ -106,12 +95,12 @@ checkLet : (@0 x : name)
            (ty : Type α)
            → TCM (Γ ⊢ TLet x u v ∶ ty)
 checkLet {Γ = Γ} x u v ty = do
-  tu ⟨ dtu ⟩  ← inferType {Γ = Γ} u
+  tu , dtu  ← inferType {Γ = Γ} u
   dtv ← checkType {Γ = Γ , x ∶ tu} v (weaken (subWeaken subRefl) ty)
-  return (TyLet {r = rezz-scope Γ} dtu dtv)
+  return (TyLet {r = rezzScope Γ} dtu dtv)
 
 checkCoerce : (t : Term α)
-            → ∃ (Type α) (λ ty → Γ ⊢ t ∶ ty)
+            → Σ[ ty ∈ Type α ] Γ ⊢ t ∶ ty
             → (cty : Type α) -- the type we want to have
             → (tty : Type α) -- the type of types
             → TCM (Γ ⊢ t ∶ cty)
@@ -125,31 +114,31 @@ checkCoerce : (t : Term α)
 --for pi
 --for sort
 --the rest should be reduced away
-checkCoerce t (s ⟨ d ⟩) cty tty = return (TyConv d (convert tty s cty))
+checkCoerce t (s , d) cty tty = return (TyConv d (convert tty s cty))
 
 
 
 checkType {Γ = Γ} t@(TVar x p) ty = do
-  tvar ← inferVar {Γ = Γ} x p
-  (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
+  tvar     ← inferVar {Γ = Γ} x p
+  tsor , _ ← inferSort {Γ = Γ} ty
   checkCoerce {Γ = Γ} t tvar ty (TSort tsor)
 checkType {Γ = Γ} (TDef d p) ty =  do
-  tdef ← inferDef d p
-  (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
+  tdef     ← inferDef d p
+  tsor , _ ← inferSort {Γ = Γ} ty
   checkCoerce {Γ = Γ} (TDef d p) tdef ty (TSort tsor)
 checkType (TCon c p x) ty = tcError "not implemented yet"
 checkType (TLam x te) ty =  checkLambda x te ty
 checkType {Γ = Γ} t@(TApp u e) ty = do
-  tapp ← inferApp {Γ = Γ} u e
-  (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
+  tapp     ← inferApp {Γ = Γ} u e
+  tsor , _ ← inferSort {Γ = Γ} ty
   checkCoerce {Γ = Γ} t tapp ty (TSort tsor)
 checkType {Γ = Γ} t@(TPi x su sv u v) ty = do
-  tpi ← inferPi {Γ = Γ} x su sv u v
-  (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
+  tpi      ← inferPi {Γ = Γ} x su sv u v
+  tsor , _ ← inferSort {Γ = Γ} ty
   checkCoerce {Γ = Γ} t tpi ty (TSort tsor)
 checkType {Γ = Γ} t@(TSort s) ty = do
-  tts ← inferTySort {Γ = Γ} s
-  (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
+  tts      ← inferTySort {Γ = Γ} s
+  tsor , _ ← inferSort {Γ = Γ} ty
   checkCoerce {Γ = Γ} t tts ty (TSort tsor)
 checkType (TLet x u v) ty = checkLet x u v ty
 checkType (TAnn u t) ty = tcError "not implemented yet"
diff --git a/src/Agda/Core/Typing.agda b/src/Agda/Core/Typing.agda
index 7f1a9d7..cf5419a 100644
--- a/src/Agda/Core/Typing.agda
+++ b/src/Agda/Core/Typing.agda
@@ -77,7 +77,7 @@ data TyTerm {α} Γ where
     : Γ ⊢ TSort (STyp n) ∶ TSort (STyp (suc n))
 
   TyLet
-    : {r : Rezz _ α}
+    : {@0 r : Rezz _ α}
     → Γ ⊢ u ∶ s
     → Γ , x ∶ s ⊢ v ∶ weaken (subWeaken subRefl) t
     ----------------------------------------------
diff --git a/src/Agda/Core/Utils.agda b/src/Agda/Core/Utils.agda
new file mode 100644
index 0000000..0711374
--- /dev/null
+++ b/src/Agda/Core/Utils.agda
@@ -0,0 +1,58 @@
+module Agda.Core.Utils where
+
+open import Haskell.Prelude hiding (_,_)
+open import Haskell.Extra.Refinement using (∃; _⟨_⟩)  public
+open import Haskell.Extra.Erase      using (Σ0; ⟨_⟩_) public
+
+-- we have 3 kinds of dependent pairs available,
+-- encoding (x : a) (y : p x)
+
+-- ∃  from Haskell.Extra.Refinement, which erases the snd component
+-- Σ0 from Haskell.Extra.Refinement, which erases the fst component
+-- Σ  from this module,              which keeps both components
+
+private module SigmaDef where
+  
+  record Sigma (a : Set) (b : @0 a → Set) : Set where
+    constructor Pair
+    field
+      fst : a
+      snd : b fst
+  open Sigma public
+  {-# COMPILE AGDA2HS Sigma #-}
+
+-- this is done so as to have a valid Haskell constructor name
+-- but be able to overload _,_ on the Agda side
+open SigmaDef public renaming (Pair to infixr 5 _,_)
+
+Σ = Sigma
+{-# COMPILE AGDA2HS Σ inline #-}
+
+
+-- we provide a shorthand syntax for all 3
+------------------------------------------
+
+infixr 2 ∃-syntax Σ Σ0-syntax
+
+∃-syntax  = ∃
+{-# COMPILE AGDA2HS ∃-syntax inline #-}
+
+Σ0-syntax = Σ0
+{-# COMPILE AGDA2HS Σ0-syntax inline #-}
+
+syntax ∃-syntax  a (λ x → b) =  ∃[ x ∈ a ] b
+syntax Σ0-syntax a (λ x → b) = Σ0[ x ∈ a ] b
+syntax Σ         a (λ x → b) =  Σ[ x ∈ a ] b
+
+pattern ∃⟨_⟩  x = x ⟨ _ ⟩
+pattern Σ0⟨_⟩ x = ⟨ _ ⟩ x
+
+-- TODO: move this upstream
+subst' : (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
+subst' p refl z = z
+{-# COMPILE AGDA2HS subst' transparent #-}
+
+data Fuel : Set where
+  None : Fuel
+  More : Fuel → Fuel
+{-# COMPILE AGDA2HS Fuel #-}