diff --git a/HoTTLean/ForMathlib.lean b/HoTTLean/ForMathlib.lean
index 0d1cd8c9..af5a7bd2 100644
--- a/HoTTLean/ForMathlib.lean
+++ b/HoTTLean/ForMathlib.lean
@@ -1,10 +1,11 @@
+import Mathlib.Tactic.DepRewrite
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
 import Mathlib.CategoryTheory.Groupoid.Discrete
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.Logic.Function.ULift
 import Mathlib.CategoryTheory.Category.Cat
-import Mathlib.CategoryTheory.Category.Grpd
+import Mathlib.CategoryTheory.Groupoid.Grpd.Basic
 import Mathlib.Data.Part
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 import Mathlib.CategoryTheory.Core
@@ -101,29 +102,29 @@ namespace CategoryTheory.Cat
 
 /-- This is the proof of equality used in the eqToHom in `Cat.eqToHom_hom` -/
 theorem eqToHom_hom_aux {C1 C2 : Cat.{v,u}} (x y: C1) (eq : C1 = C2) :
-    (x ⟶ y) = ((eqToHom eq).obj x ⟶ (eqToHom eq).obj y) := by
+    (x ⟶ y) = ((eqToHom eq).toFunctor.obj x ⟶ (eqToHom eq).toFunctor.obj y) := by
   cases eq
   simp[CategoryStruct.id]
 
 /-- This is the turns the hom part of eqToHom functors into a cast-/
 theorem eqToHom_hom {C1 C2 : Cat.{v,u}} {x y: C1} (f : x ⟶ y) (eq : C1 = C2) :
-    (eqToHom eq).map f = (cast (Cat.eqToHom_hom_aux x y eq) f) := by
+    (eqToHom eq).toFunctor.map f = (cast (Cat.eqToHom_hom_aux x y eq) f) := by
   cases eq
   simp[CategoryStruct.id]
 
 /-- This turns the object part of eqToHom functors into casts -/
 theorem eqToHom_obj {C1 C2 : Cat.{v,u}} (x : C1) (eq : C1 = C2) :
-    (eqToHom eq).obj x = cast (congrArg Bundled.α eq) x := by
+    (eqToHom eq).toFunctor.obj x = cast (congrArg Bundled.α eq) x := by
   cases eq
   simp[CategoryStruct.id]
 
 abbrev homOf {C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) :
-    Cat.of C ⟶ Cat.of D := F
+    Cat.of C ⟶ Cat.of D := ⟨F⟩
 
 @[simps] def ULift_lte_iso_self {C : Type (max u u₁)} [Category.{v} C] :
     Cat.of (ULift.{u} C) ≅ Cat.of C where
-  hom := ULift.downFunctor
-  inv := ULift.upFunctor
+  hom := homOf ULift.downFunctor
+  inv := homOf ULift.upFunctor
 
 @[simp] def ULift_succ_iso_self {C : Type (u + 1)} [Category.{v} C] :
     of (ULift.{u, u + 1} C) ≅ of C := ULift_lte_iso_self.{v,u,u+1}
@@ -135,8 +136,8 @@ def ofULift (C : Type u) [Category.{v} C] : Cat.{v, max u w} :=
   of $ ULift.{w} C
 
 def uLiftFunctor : Cat.{v,u} ⥤ Cat.{v, max u w} where
-  obj X := Cat.ofULift.{w} X
-  map F := Cat.homOf $ ULift.downFunctor ⋙ F ⋙ ULift.upFunctor
+  obj X := ofULift.{w} X
+  map F := homOf $ ULift.downFunctor ⋙ F.toFunctor ⋙ ULift.upFunctor
 
 end CategoryTheory.Cat
 
@@ -401,16 +402,15 @@ variable {Γ : Type u₂} [Category.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
 
 @[simp] theorem Cat.map_id_obj {A : Γ ⥤ Cat.{v₁,u₁}}
     {x : Γ} {a : A.obj x} :
-    (A.map (𝟙 x)).obj a = a := by
-  have : A.map (𝟙 x) = 𝟙 (A.obj x) := by simp
-  exact Functor.congr_obj this a
+    (A.map (𝟙 x)).toFunctor.obj a = a := by
+  simp
 
 theorem Cat.map_id_map {A : Γ ⥤ Cat.{v₁,u₁}}
     {x : Γ} {a b : A.obj x} {f : a ⟶ b} :
-    (A.map (𝟙 x)).map f = eqToHom Cat.map_id_obj
+    (A.map (𝟙 x)).toFunctor.map f = eqToHom Cat.map_id_obj
       ≫ f ≫ eqToHom Cat.map_id_obj.symm := by
-  have : A.map (𝟙 x) = 𝟙 (A.obj x) := by simp
-  exact Functor.congr_hom this f
+  rw! [show A.map (𝟙 x) = 𝟙 (A.obj x) by simp]
+  simp
 
 end
 
@@ -624,14 +624,6 @@ lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} :
     cases h
     simp
 
-lemma Discrete.functor_ext {X C : Type*} [Category C] (F G : Discrete X ⥤ C)
-    (h : ∀ x : X, F.obj ⟨x⟩ = G.obj ⟨x⟩) :
-    F = G :=
-  calc F
-    _ = Discrete.functor (fun x => F.obj ⟨x⟩) := Discrete.functor_eq
-    _ = Discrete.functor (fun x => G.obj ⟨x⟩) := Discrete.functor_ext' h
-    _ = G := Discrete.functor_eq.symm
-
 lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y)
     (hab : a.1 ≍ b.1) : a ≍ b := by
   aesop_cat
diff --git a/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean b/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean
index 3f256088..05b5a28d 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean
+++ b/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean
@@ -60,8 +60,6 @@ variable (F : Pseudofunctor B Cat) {a b : B}
     (X Y : LocallyDiscrete C) (e : X ≅ Y) : e.hom.toLoc ≫ e.inv.toLoc = 𝟙 _ :=
   LocallyDiscrete.eq_of_hom ⟨⟨by simp⟩⟩
 
-attribute [reassoc] StrongTrans.naturality_comp_inv_app
-
 end
 
 lemma _root_.CategoryTheory.Functor.toPseudofunctor'_map₂ {C : Type u₁} [Category.{v₁} C] (F : C ⥤ Cat)
diff --git a/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean b/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean
index e853e0c4..8c6c9147 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean
+++ b/HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean
@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Hua
 -/
 import Mathlib.CategoryTheory.Groupoid.FreeGroupoid
-import Mathlib.CategoryTheory.Category.Grpd
+import Mathlib.CategoryTheory.Groupoid.Grpd.Basic
 import Mathlib.CategoryTheory.Adjunction.Reflective
 import Mathlib.CategoryTheory.Localization.Predicate
 import Mathlib.CategoryTheory.Monad.Limits
 import Mathlib.CategoryTheory.Category.Cat.Limit
 
-import HoTTLean.ForMathlib.CategoryTheory.Localization.Predicate
-
 /-!
 # Free groupoid on a category
 
@@ -190,15 +188,15 @@ open Category.FreeGroupoid
 @[simps]
 def free : Cat.{u,u} ⥤ Grpd.{u,u} where
   obj C := Grpd.of <| Category.FreeGroupoid C
-  map {C D} F := map F
-  map_id C := by simp [Grpd.id_eq_id, ← map_id]; rfl
-  map_comp F G := by simp [Grpd.comp_eq_comp, ← map_comp]; rfl
+  map {C D} F := map F.toFunctor
+  map_id C := by simp [Grpd.id_eq_id, ← map_id]
+  map_comp F G := by simp [Grpd.comp_eq_comp, ← map_comp]
 
 /-- The unit of the free-forgetful adjunction between `Grpd` and `Cat`. -/
 @[simps]
 def freeForgetAdjunction.unit : 𝟭 Cat ⟶ free ⋙ forgetToCat where
-  app C := Category.FreeGroupoid.of C
-  naturality C D F := by simp [forgetToCat, Cat.comp_eq_comp, map, lift_spec]
+  app C := ⟨Category.FreeGroupoid.of C⟩
+  naturality C D F := by ext; simp [forgetToCat, map, lift_spec]
 
 /-- The counit of the free-forgetful adjunction between `Grpd` and `Cat`. -/
 @[simps]
@@ -218,7 +216,7 @@ def freeForgetAdjunction : free ⊣ Grpd.forgetToCat where
     apply lift_unique
     simp [Functor.assoc, lift_spec, Grpd.id_eq_id]
   right_triangle_components G := by
-    simp [forgetToCat, Cat.comp_eq_comp, lift_spec, Cat.id_eq_id]
+    ext; simp [forgetToCat, lift_spec]
 
 instance : Reflective Grpd.forgetToCat where
   L := free
diff --git a/HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean b/HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean
deleted file mode 100644
index 0f73aff6..00000000
--- a/HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathlib.CategoryTheory.Groupoid
-import Mathlib.CategoryTheory.MorphismProperty.Basic
-
-namespace CategoryTheory
-
-open MorphismProperty in
-lemma isGroupoid_iff_isomorphisms_eq_top (C : Type*) [Category C] :
-    IsGroupoid C ↔ isomorphisms C = ⊤ := by
-  constructor
-  · rw [eq_top_iff]
-    intro _ _
-    simp only [isomorphisms.iff, top_apply]
-    infer_instance
-  · intro h
-    exact ⟨of_eq_top h⟩
-
-end CategoryTheory
diff --git a/HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean b/HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean
deleted file mode 100644
index 70dc3771..00000000
--- a/HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-import Mathlib.CategoryTheory.Localization.Predicate
-
-import HoTTLean.ForMathlib.CategoryTheory.Groupoid
-import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.Basic
-
-noncomputable section
-
-namespace CategoryTheory.Localization
-open Category Functor
-
-variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D) (W : MorphismProperty C) (E : Type*)
-  [Category E]
-
-variable {D₁ D₂ : Type _} [Category D₁] [Category D₂] (L₁ : C ⥤ D₁) (L₂ : C ⥤ D₂)
-  (W' : MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W']
-
-lemma morphismProperty_eq_top [L.IsLocalization W] (P : MorphismProperty D) [P.RespectsIso]
-    [P.IsMultiplicative] (h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f))
-    (h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv) :
-    P = ⊤ := by
-  let P' : MorphismProperty W.Localization :=
-    P.inverseImage (Construction.lift L Functor.IsLocalization.inverts)
-  have hP' : P' = ⊤ := by
-    apply Construction.morphismProperty_is_top
-    · intros
-      simp only [MorphismProperty.inverseImage_iff, Construction.lift_obj, ← Functor.comp_map,
-        Functor.congr_hom (Construction.fac L Functor.IsLocalization.inverts), Functor.comp_obj,
-        eqToHom_refl, Category.comp_id, Category.id_comp, h₁, P']
-    · intro X Y w hw
-      simp only [P', MorphismProperty.inverseImage_iff]
-      convert h₂ w hw
-      convert Functor.map_inv (Construction.lift L Functor.IsLocalization.inverts)
-        (Construction.wIso w hw).hom
-      · simp
-      · have : (Construction.wIso w hw).hom = W.Q.map w := rfl
-        simp only [this, ← Functor.comp_map,
-          Functor.congr_hom (Construction.fac L Functor.IsLocalization.inverts)]
-        simp [isoOfHom]
-  have : P'.map _ = P := MorphismProperty.map_inverseImage_eq_of_isEquivalence ..
-  simp [← this, hP']
-
-lemma isGroupoid [L.IsLocalization ⊤] :
-    IsGroupoid D := by
-  rw [isGroupoid_iff_isomorphisms_eq_top]
-  exact morphismProperty_eq_top L ⊤ _
-    (fun _ _ f ↦ inverts L ⊤ _ (by simp))
-    (fun _ _ f hf ↦ Iso.isIso_inv _)
-
-instance : IsGroupoid (⊤ : MorphismProperty C).Localization :=
-  isGroupoid <| MorphismProperty.Q ⊤
-
-/-- Localization of a category with respect to all morphisms results in a groupoid. -/
-def groupoid : Groupoid (⊤ : MorphismProperty C).Localization :=
-  Groupoid.ofIsGroupoid
-
-end CategoryTheory.Localization
diff --git a/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean b/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean
deleted file mode 100644
index 8773745c..00000000
--- a/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import Mathlib.CategoryTheory.MorphismProperty.Basic
-
-universe u v
-
-namespace CategoryTheory.MorphismProperty
-
-variable {C : Type u} [Category.{v} C] {D : Type*} [Category D]
-
-@[simp]
-lemma map_top_eq_top_of_essSurj_of_full (F : C ⥤ D) [F.EssSurj] [F.Full] :
-    (⊤ : MorphismProperty C).map F = ⊤ := by
-  rw [eq_top_iff]
-  intro X Y f _
-  refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
-  · exact (Functor.objObjPreimageIso F X).hom ≫ f ≫ (Functor.objObjPreimageIso F Y).inv
-  · exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
-      (by simp)
-
-end CategoryTheory.MorphismProperty
diff --git a/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean b/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean
index aee6e9a4..d8697466 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean
+++ b/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean
@@ -1,6 +1,5 @@
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Functor.TwoSquare
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 import HoTTLean.ForMathlib
 
 universe w v u v₁ u₁ v₂ u₂ v₃ u₃
diff --git a/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean b/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean
index acffbd24..49174775 100644
--- a/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean
+++ b/HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean
@@ -1,7 +1,7 @@
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 import HoTTLean.ForMathlib.CategoryTheory.WeakPullback
 
 /-!
diff --git a/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean b/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean
index d03c7c5b..2c4b7d1b 100644
--- a/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean
+++ b/HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean
@@ -56,24 +56,24 @@ def functorMapExpr (e : Expr) (lvl_params : Bool) : MetaM (Expr × List Level) :
     let some (hom, _, _) := eTp.eq? | throwError "expected an equality, got{indentD eTp}"
     if !hom.isAppOf ``Quiver.Hom then
       throwError "expected an equality of morphisms, got{indentD eTp}"
-    let [.succ v₁, u₁] := hom.getAppFn.constLevels! |
+    let [v₁, u₁] := hom.getAppFn.constLevels! |
       throwError "unexpected universe levels in{indentD hom.getAppFn}"
     let e' ← mkAppM' (.const ``eq_functor_map [v₁, u₁, v₂, u₂]) #[e]
     simpType categorySimp' e'
   return (e, [v₂, u₂])
 
-syntax (name := functor_map) "functor_map" (" (" &"attr" ":=" Parser.Term.attrInstance,* ")")? : attr
+syntax (name := functor_map) "functor_map" optAttrArg : attr
 
 initialize registerBuiltinAttribute {
   name := `functor_map
   descr := ""
   applicationTime := .afterCompilation
   add := fun src ref kind => match ref with
-  | `(attr| functor_map $[(attr := $stx?,*)]?) => MetaM.run' do
+  | `(attr| functor_map $stx?) => MetaM.run' do
     if (kind != AttributeKind.global) then
       throwError "`functor_map` can only be used as a global attribute"
-    addRelatedDecl src "_functor_map" ref stx? fun type value levels => do
-      let (e, levels') ← functorMapExpr (← mkExpectedTypeHint value type) true
+    addRelatedDecl src (src.appendAfter "_functor_map") ref stx? fun value levels => do
+      let (e, levels') ← functorMapExpr value true
       pure (e, levels ++ levels'.map fun | .param n => n | _ => panic! "")
   | _ => throwUnsupportedSyntax }
 
diff --git a/HoTTLean/ForPoly.lean b/HoTTLean/ForPoly.lean
index b9a44a91..72f1fdb6 100644
--- a/HoTTLean/ForPoly.lean
+++ b/HoTTLean/ForPoly.lean
@@ -256,8 +256,8 @@ theorem fan_snd_map' {E B E' B' : C} {P : UvPoly E B} {P' : UvPoly E' B'}
   slice_lhs 1 2 => rw [← this]
   slice_lhs 2 3 => apply Category.comp_id
   simp [α, Over.starPullbackIsoStar]
-  slice_lhs 5 6 => apply pullback.lift_fst
-  simp [Over.mapForget]
+  slice_lhs 4 5 => apply pullback.lift_fst
+  simp
 
 open ExponentiableMorphism in
 theorem fan_snd_map {E B A E' B' A' : C} {P : UvPoly E B} {P' : UvPoly E' B'}
diff --git a/HoTTLean/Frontend/Checked.lean b/HoTTLean/Frontend/Checked.lean
deleted file mode 100644
index 6c05d190..00000000
--- a/HoTTLean/Frontend/Checked.lean
+++ /dev/null
@@ -1,62 +0,0 @@
-import HoTTLean.Syntax.Axioms
-import HoTTLean.Typechecker.Value
-
-/-! Structures that store deeply embedded axioms and definitions. -/
-
-namespace SynthLean
-
-variable {χ : Type*} {E : Axioms χ}
-
-/-- An axiom checked with respect to the axioms in `E`. -/
-structure CheckedAx (E : Axioms χ) where
-  name : χ
-  get_name : E name = none
-  l : Nat
-  tp : Expr χ
-  nfTp : Val χ
-  wf_nfTp : ValEqTp E [] l nfTp tp
-
-namespace CheckedAx
-
-theorem wf_tp (a : CheckedAx E) : E ∣ [] ⊢[a.l] a.tp :=
-  a.wf_nfTp.wf_tp
-
-/-- The set of axioms extended by this one. -/
-noncomputable def snocAxioms (a : CheckedAx E) : Axioms χ :=
-  E.snoc a.l a.name a.tp a.wf_tp.le_univMax a.wf_tp.isClosed
-
-theorem le_snocAxioms (a : CheckedAx E) : E ≤ a.snocAxioms :=
-  E.le_snoc_self _ _ _ _ _ a.get_name
-
-theorem wf_snocAxioms (a : CheckedAx E) (Ewf : E.Wf) : a.snocAxioms.Wf :=
-  Ewf.snoc a.name a.wf_tp a.get_name
-
-/-- The axiom as a term. -/
-def val (a : CheckedAx E) : Expr χ :=
-  .ax a.name a.tp
-
-theorem wf_val (a : CheckedAx E) : a.snocAxioms ∣ [] ⊢[a.l] a.val : a.tp := by
-  unfold val
-  have := E.snoc_get a.l a.name a.tp a.wf_tp.le_univMax a.wf_tp.isClosed
-  apply WfTm.ax .nil this
-  apply a.wf_nfTp.wf_tp.of_axioms_le a.le_snocAxioms
-
-end CheckedAx
-
-/-- A definition checked with respect to the axioms in `E`. -/
-structure CheckedDef (E : Axioms χ) where
-  l : Nat
-  tp : Expr χ
-  nfTp : Val χ
-  wf_nfTp : ValEqTp E [] l nfTp tp
-  val : Expr χ
-  -- nfVal?
-  wf_val : E ∣ [] ⊢[l] val : tp
-
-namespace CheckedDef
-
-theorem wf_tp (d : CheckedDef E) : E ∣ [] ⊢[d.l] d.tp :=
-  d.wf_val.wf_tp
-
-end CheckedDef
-end SynthLean
diff --git a/HoTTLean/Frontend/ExternalCtxWidget.lean b/HoTTLean/Frontend/ExternalCtxWidget.lean
new file mode 100644
index 00000000..d5f099c2
--- /dev/null
+++ b/HoTTLean/Frontend/ExternalCtxWidget.lean
@@ -0,0 +1,33 @@
+import Qq
+import HoTTLean.Frontend.Macros
+import ProofWidgets.Component.OfRpcMethod
+import ProofWidgets.Component.Panel.Basic
+
+namespace SynthLean
+
+open Qq
+open Lean Server Meta
+open ProofWidgets Jsx
+
+@[server_rpc_method]
+def ExternalCtxWidget.rpc (p : PanelWidgetProps) : RequestM (RequestTask Html) :=
+  RequestM.asTask do
+    let some g := p.termGoal? | return .text ""
+    g.ctx.val.runMetaM {} do
+      let some elabData := elabExt.getState (← getEnv) | return .text ""
+      withLCtx elabData.lctx elabData.linsts do
+        let g ← mkFreshExprMVar (some q(SynthLean.Expr $elabData.χ))
+        let ctx := { env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := ← getOptions }
+        let msg := .withContext ctx <| .ofGoal g.mvarId!
+        return <details «open»={true}>
+          <summary>External expected type</summary>
+          <InteractiveMessage msg={← WithRpcRef.mk msg} />
+        </details>
+
+@[widget_module]
+def ExternalCtxWidget : Component PanelWidgetProps :=
+  mk_rpc_widget% ExternalCtxWidget.rpc
+
+show_panel_widgets [ExternalCtxWidget]
+
+end SynthLean
diff --git a/HoTTLean/Frontend/Instances.lean b/HoTTLean/Frontend/Instances.lean
new file mode 100644
index 00000000..a65e5684
--- /dev/null
+++ b/HoTTLean/Frontend/Instances.lean
@@ -0,0 +1,78 @@
+import HoTTLean.Model.Unstructured.InternalTheory
+import HoTTLean.Frontend.Reflected
+
+/-! Classes used by the typechecker to combine expressions from different theories. -/
+
+namespace SynthLean
+
+variable {χ : Type*}
+
+/-! ## Theory inclusions -/
+
+namespace Axioms
+
+variable (𝕋 𝕋' : Axioms χ)
+
+-- High priority to prove `𝕋.snoc 𝕋c Awf ≤ 𝕋.snoc 𝕋c Awf` without going through `snoc_le_snoc`.
+instance (priority := high) : Fact (𝕋 ≤ 𝕋) := ⟨Std.Refl.refl _⟩
+
+/-! The rules below prove `Fact (𝕋 ≤ 𝕋')` whenever both are theories are `.empty`/`.snoc` lists,
+and `𝕋` is a sublist of `𝕋'` (without reordering). -/
+
+instance : Fact (.empty χ ≤ 𝕋) := ⟨empty_le _⟩
+
+instance [DecidableEq χ] [Fact (𝕋 ≤ 𝕋')]
+    {c A l} (𝕋'c : 𝕋' c = none) (Awf : 𝕋' ∣ [] ⊢[l] A) :
+    Fact (𝕋 ≤ 𝕋'.snoc 𝕋'c Awf) :=
+  ⟨le_snoc Fact.out ..⟩
+
+instance [DecidableEq χ] [Fact (𝕋 ≤ 𝕋')]
+    {c A l} (𝕋c : 𝕋 c = none) (𝕋'c : 𝕋' c = none)
+    (Awf : 𝕋 ∣ [] ⊢[l] A) (Awf' : 𝕋' ∣ [] ⊢[l] A) :
+    Fact (𝕋.snoc 𝕋c Awf ≤ 𝕋'.snoc 𝕋'c Awf') :=
+  ⟨snoc_le_snoc Fact.out ..⟩
+
+end Axioms
+
+/-! ## Theory maps -/
+
+variable {χ' : Type*}
+
+/-- Provides a well-formed translation from theory `𝕋` to theory `𝕋'`.
+
+This is a class because when such a translation exists,
+it is convenient to directly use `𝕋`-expressions in `𝕋'`-expressions.
+We automatically insert the instance in such cases. -/
+class HasTheoryMap (𝕋 : Axioms χ) (𝕋' : Axioms χ') where
+  map : χ → χ'
+  map_wf (𝕋 𝕋') : WfTheoryMap 𝕋 map 𝕋'
+
+instance [Inhabited χ'] (𝕋' : Axioms χ') : HasTheoryMap (.empty χ) 𝕋' where
+  map := fun _ => default
+  map_wf := ⟨nofun⟩
+
+instance (𝕋 𝕋' : Axioms χ) [Fact (𝕋 ≤ 𝕋')] : HasTheoryMap 𝕋 𝕋' where
+  map := id
+  map_wf := WfTheoryMap.of_le Fact.out
+
+/-! ## Well-formed theories -/
+
+instance (χ) : Fact (Axioms.empty χ).Wf :=
+  ⟨Axioms.empty_wf χ⟩
+
+instance [DecidableEq χ] (𝕋 : Axioms χ) [Fact 𝕋.Wf] (a : ReflectedAx 𝕋) : Fact a.snocAxioms.Wf :=
+  ⟨a.wf_snocAxioms Fact.out⟩
+
+instance [DecidableEq χ] (𝕋 : Axioms χ) [Fact 𝕋.Wf]
+    {c A l} (𝕋c : 𝕋 c = none) (Awf : 𝕋 ∣ [] ⊢[l] A) :
+    Fact (𝕋.snoc 𝕋c Awf).Wf :=
+  ⟨(Fact.out : 𝕋.Wf).snoc 𝕋c Awf⟩
+
+open CategoryTheory
+open Model UnstructuredUniverse
+universe v u
+
+instance {𝒞 : Type u} [Category.{v,u} 𝒞] [ChosenTerminal 𝒞] (s : UHomSeq 𝒞) : Fact s.thyInt.Wf :=
+  ⟨s.thyInt_wf⟩
+
+end SynthLean
diff --git a/HoTTLean/Frontend/Macros.lean b/HoTTLean/Frontend/Macros.lean
new file mode 100644
index 00000000..c507818d
--- /dev/null
+++ b/HoTTLean/Frontend/Macros.lean
@@ -0,0 +1,167 @@
+import HoTTLean.Model.Unstructured.InternalTheory
+import HoTTLean.Frontend.Shallow
+import HoTTLean.Frontend.Translation
+
+/-! Elaborators for `tp%{..}`, `tm%{..}`, and `⸨..⸩`. -/
+
+namespace SynthLean
+
+open Qq
+open Lean Meta Elab Term
+open CategoryTheory ChosenTerminal
+open Model UnstructuredUniverse
+
+inductive ExpectedTheory : {u : Level} → Q(Type u) → Type
+  | internal {u : Level} (𝒞 : Q(Type u))
+    {v : Level} (cat : Q(Category.{v, u} $𝒞)) (ct : Q(ChosenTerminal.{v,u} $𝒞))
+    (s : Q(UHomSeq $𝒞)) : ExpectedTheory q(($s).SigInt)
+  | other {u : Level} {χ : Q(Type u)} (E : Q(Axioms $χ)) : ExpectedTheory q($χ)
+
+def ExpectedTheory.theory {u : Level} : {χ : Q(Type u)} → ExpectedTheory q($χ) → Q(Axioms $χ)
+  | _, .internal _ _ _ s => q(($s).thyInt)
+  | _, .other E => q($E)
+
+structure ElabData where
+  lctx : LocalContext
+  linsts : LocalInstances
+  u : Level
+  χ : Q(Type u)
+  E : ExpectedTheory q($χ)
+
+private abbrev ElabExt := EnvExtension (Option ElabData)
+
+/-- When elaborating terms such as `tm%{t ⸨u⸩}`,
+we must communicate some information (e.g. which theory is in use)
+from the outer `tm%{..}` elaborator to the inner `⸨..⸩` elaborator
+(the term `t ⸨u⸩` is processed using Lean's default `elabTerm`,
+so we can't just call something with the right argument).
+`CoreM` is only extensible through environment extensions,
+so we use one to communicate this data.
+
+It would alternatively be possible for `tm%{..}` to traverse its argument
+and preprocess occurrences of `⸨..⸩`
+(this is what `quote4` does with antiquotations like `q(t $(u))`),
+but the present implementation strategy appears more straightforward.
+
+For those who know Fitch-style modal type theory:
+this is basically a janky implementation of context locking. -/
+initialize elabExt : ElabExt ← registerEnvExtension (pure none)
+
+/-- Identify the signature and theory that a `tp%/tm% (theory := thy)` expression should target. -/
+-- TODO: Infer `computeAxioms` when `eT = SynthLean.Expr Lean.Name`?
+def elabExpectedTheory (thy : Option Term) (expectedType : Lean.Expr) :
+    TermElabM ((u : Level) × (χ : Q(Type u)) × ExpectedTheory q($χ)) := do
+  let v ← mkFreshLevelMVar
+  let χ ← mkFreshExprMVarQ q(Type v)
+  if let some thy := thy then
+    let E ← elabTermEnsuringTypeQ thy q(Axioms $χ)
+    let u ← mkFreshLevelMVar
+    let 𝒞 : Q(Type u) ← mkFreshExprMVarQ q(Type u)
+    let _cat : Q(Category.{v,u} $𝒞) ← mkFreshExprMVarQ q(Category.{v,u} $𝒞)
+    let _ct : Q(ChosenTerminal.{v,u} $𝒞) ← mkFreshExprMVarQ q(ChosenTerminal.{v,u} $𝒞)
+    let s : Q(UHomSeq $𝒞) ← mkFreshExprMVarQ q(UHomSeq $𝒞)
+    if ← isDefEq E q(($s).thyInt) then
+      return ⟨v, q(($s).SigInt), .internal q($𝒞) q($_cat) q($_ct) q($s)⟩
+    else
+      return ⟨v, q($χ), .other q($E)⟩
+  -- This may assign the expected type.
+  if !(← isDefEq expectedType q(SynthLean.Expr $χ)) then
+    throwError "This macro produces a SynthLean expression. \
+      The expected type must be of the form{indentExpr q(SynthLean.Expr $χ)}"
+  let u ← mkFreshLevelMVar
+  let 𝒞 ← mkFreshExprMVarQ q(Type u)
+  let _cat ← mkFreshExprMVarQ q(Category.{v,u} $𝒞)
+  let _ct ← mkFreshExprMVarQ q(ChosenTerminal.{v,u} $𝒞)
+  let s ← mkFreshExprMVarQ q(UHomSeq $𝒞)
+  if ← isDefEq χ q(($s).SigInt) then
+    if !(← instantiateMVars s).hasMVar then
+      return ⟨v, q(($s).SigInt), .internal q($𝒞) q($_cat) q($_ct) q($s)⟩
+  throwError "Could not infer the theory from the expected type. \
+  Please provide (theory := ..) explicitly."
+
+elab_rules : term <= expectedType | `(tp% $[$thy:theorySpec]? {$t}) => do
+  let thy := thy.map (⟨·.raw[3]⟩)
+  let ⟨u, χ, E⟩ ← elabExpectedTheory thy expectedType
+  let env ← getEnv
+  let lctx ← getLCtx
+  let linsts ← getLocalInstances
+  let t ←
+    withEnv (elabExt.modifyState env fun _ => some ⟨lctx, linsts, u, χ, E⟩) <|
+    -- FIXME: Would be really cool to also display the locked,
+    -- external context in the tactic state.
+    withLCtx {} {} <|
+    -- Ensure that infotrees store the `elabExt`.
+    withSaveInfoContext do
+      -- TODO: Need to also deal with mctx?
+      let w ← mkFreshLevelMVar
+      elabTermEnsuringType t (some <| .sort (.succ w))
+  let (_, T) ←
+    try translateAsTp (u := u) χ t |>.run E.theory
+    catch e =>
+      throwError "Failed to translate type{Lean.indentExpr t}\nError: {e.toMessageData}"
+  return T
+
+-- TODO: term expressions
+
+elab_rules : term <= expectedType | `(⸨$t_stx⸩) => do
+  let w ← mkFreshLevelMVar
+  if !(← isDefEq expectedType (.sort (.succ w))) then
+    throwError "Expected a term of type{indentExpr expectedType}\n\
+    but got{indentD ""}⸨..⸩ : {Expr.sort (.succ w)}"
+
+  let some elabData := elabExt.getState (← getEnv)
+    | throwError "The `⸨..⸩` macro can only appear inside `tp%` or `tm%` macros."
+  let { lctx, linsts, E := .internal (u := u) (v := v) _ _ _ s, .. } := elabData
+    | throwError "The `⸨..⸩` macro can only be used in the internal theory of a model."
+
+  -- expected Type is one of P : Sort 0 : Type 0 : Type 1
+  -- h : P : Sort 0 : Type 0 : Type 1
+  withEnv (elabExt.modifyState (← getEnv) fun _ => none) do
+  -- Reinstate the external local context and instances.
+  withLCtx lctx linsts do
+  -- Ensure that infotrees store the `elabExt`.
+  withSaveInfoContext do
+    let l ← mkFreshExprMVarQ q(ℕ)
+    let _lt ← mkFreshExprMVarQ q($l < ($s).length + 1)
+    let t ← elabTermEnsuringTypeQ t_stx q(𝟭_ _ ⟶ $s[$l].Ty)
+
+    -- FIXME: how should we external/internal mvars, in particular in `l`/`w`?
+    -- Can we postpone here, wait until `l`/`w` are concrete,
+    -- and then unify them?
+    -- For now we only handle closed `t` and `l`.
+    if t.hasMVar then
+      throwErrorAt t_stx "Term contains metavariables{indentExpr t}"
+    let l ← instantiateMVars l
+    let some nl ← (evalNat l).run
+      | throwErrorAt t_stx "Semantic type has unknown universe level{indentExpr l}"
+    if !(← isLevelDefEq nl.toLevel w) then
+      throwErrorAt t_stx "Got semantic type at level{indentExpr l}\n\
+      but expected{indentExpr <| expectedType}"
+
+    -- Ensure `l < univMax`
+    let lt ← ltNat q($l) q(univMax)
+
+    -- `semTy` is well-formed in the external local context.
+    let semTy : Q(($s).SigInt) := q(UHomSeq.SigInt.ty.{v,u} $lt $t)
+    -- `qst` is a closed expression, well-formed in any local context
+    -- (in particular in the internal one).
+    let qst : Q(Lean.Expr) := @toExpr Lean.Expr _ semTy
+    let expectedType : Q(Type w) := expectedType
+
+    return q(SemAx $expectedType $qst)
+
+open PrettyPrinter Delaborator SubExpr
+
+@[delab app.SynthLean.SemAx]
+def delabSemAx : Delab := do
+  let e ← getExpr
+  guard <| e.getAppNumArgs == 2
+  let some elabData := elabExt.getState (← getEnv) | failure
+  let qst ← evalExprExpr (e.getArg! 1)
+  let pos := (← getPos).pushNaryArg 2 1
+  let st ← withLCtx elabData.lctx elabData.linsts <|
+    withTheReader SubExpr (fun _ => { expr := qst, pos }) <|
+      delab
+  `(⸨$st⸩)
+
+end SynthLean
diff --git a/HoTTLean/Frontend/Reflect.lean b/HoTTLean/Frontend/Reflect.lean
new file mode 100644
index 00000000..cf708a7c
--- /dev/null
+++ b/HoTTLean/Frontend/Reflect.lean
@@ -0,0 +1,178 @@
+import Lean
+import Qq
+import HoTTLean.Prelude
+import HoTTLean.Typechecker.Synth
+import HoTTLean.Frontend.Translation
+
+/-! We define the `@[reflect]` attribute. -/
+
+namespace SynthLean
+
+open Lean Meta
+open Qq
+
+/-- Find axioms used by the given constant,
+and return them as an axiom environment.
+Fails if any axiom has not yet been reflected
+as a definition of type `CheckedAx _`. -/
+def computeAxioms (constNm : Name) : MetaM ((E : Q(Axioms Name)) × Q(($E).Wf)) := do
+  let env ← getEnv
+  let (_, st) ← (CollectAxioms.collect constNm).run env |>.run {}
+  let axioms := st.axioms
+  -- The output includes `constNm` if it is itself an axiom.
+  let axioms := axioms.filter (· != constNm)
+  -- Order the axioms by '(`a` uses `b`) or (`a`'s name is lex below `b`'s name)'.
+  let mut axiomAxioms : Std.HashMap Name (Array Name) := {}
+  for axNm in axioms do
+    let (_, st) ← (CollectAxioms.collect axNm).run env |>.run {}
+    let axioms := st.axioms.filter (· != axNm)
+    axiomAxioms := axiomAxioms.insert axNm axioms
+  let mut axioms := axioms.qsort fun a b => axiomAxioms[b]!.contains a || a.lt b
+  -- HACK: replace `sorryAx` with our universe-monomorphic versions.
+  if let some i := axioms.findIdx? (· == ``sorryAx) then
+    axioms := axioms.set! i `sorryAx₀
+    for i in [1:univMax] do
+      axioms := axioms.push (Name.anonymous.str s!"sorryAx{Nat.subDigitChar i}")
+  let mut E : Q(Axioms Name) := q(.empty _)
+  let mut Ewf : Q(($E).Wf) := q(Axioms.empty_wf _)
+  for axNm in axioms do
+    let checkedAxNm := axNm ++ reflectPostfix
+    if !(← hasConst checkedAxNm) then
+      throwError "Axiom '{Expr.const axNm []}' has not been reflected. \
+        Try marking it with `@[reflect]`."
+    let axCi ← getConstInfo checkedAxNm
+    if !axCi.type.isAppOfArity' ``ReflectedAx 2 then
+      throwError "checked axiom '{axNm}' has unexpected type{indentExpr axCi.type}"
+    let #[_, axE] := axCi.type.getAppArgs | throwError "internal error"
+    have axE : Q(Axioms Name) := axE
+    have ax : Q(ReflectedAx $axE) := .const checkedAxNm []
+    -- (Aux `have`s work around bugs in Qq elaboration.)
+    have E' : Q(Axioms Name) := E
+    have Ewf' : Q(($E').Wf) := Ewf
+    let .inr get_name ← lookupAxiom q($E') q(($ax).name) | continue
+    let le ← synthInstanceQ q(Fact ($axE ≤ $E'))
+    let E'' : Q(Axioms Name) := q(($E').snoc $get_name (($ax).wf_tp.of_axioms_le ($le).out))
+    let Ewf'' : Q(($E'').Wf) := q(($Ewf').snoc $get_name (($ax).wf_tp.of_axioms_le ($le).out))
+    E := E''
+    Ewf := Ewf''
+  return ⟨E, Ewf⟩
+
+/-- Reflect the axiom `ci` as a `CheckedAx`,
+adding that to the Lean environment. -/
+def addCheckedAx (ci : AxiomVal) : MetaM Unit := do
+  let ⟨axioms, wf_axioms⟩ ← computeAxioms ci.name
+  let (l, T) ←
+    try translateAsTp q(Name) ci.type |>.run axioms
+    catch e =>
+      throwError "failed to translate type{indentExpr ci.type}\nerror: {e.toMessageData}"
+
+  have name : Q(Name) := toExpr ci.name
+  let .inr get_eq_none ← lookupAxiom q($axioms) q($name)
+    | throwError "internal error: axiom '{ci.name}' depends on itself"
+  TypecheckerM.run do
+  let Twf ← checkTp q($axioms) q([]) q($l) q($T)
+  let ⟨vT, vTeq⟩ ← evalTpId q(show TpEnv Name from []) q($T)
+  let value : Q(ReflectedAx $axioms) := q(
+    { name := $name
+      get_name := $get_eq_none
+      l := $l
+      tp := $T
+      nfTp := $vT
+      wf_nfTp := $vTeq .nil <| $Twf $wf_axioms .nil
+    }
+  )
+
+  -- FIXME: `addDeclQ`
+  addDecl <| .defnDecl {
+    name := ci.name ++ reflectPostfix
+    levelParams := []
+    type := q(ReflectedAx $axioms)
+    value := ShareCommon.shareCommon' value
+    hints := .regular 0 -- TODO: what height?
+    safety := .safe
+  }
+
+/-- Reflect the definition `ci` as a `CheckedDef`,
+adding that to the Lean environment. -/
+def addCheckedDef (ci : DefinitionVal) : MetaM Unit := do
+  let ⟨axioms, wf_axioms⟩ ← computeAxioms ci.name
+  let (l, T) ←
+    try translateAsTp q(Name) ci.type |>.run axioms
+    catch e =>
+      throwError "failed to translate type{indentExpr ci.type}\nerror: {e.toMessageData}"
+  let (k, t) ←
+    try translateAsTm q(Name) ci.value |>.run axioms
+    catch e =>
+      throwError "failed to translate term{indentExpr ci.value}\nerror: {e.toMessageData}"
+  if l != k then throwError "internal error: inferred level mismatch"
+
+  TypecheckerM.run do
+  let Twf ← checkTp q($axioms) q([]) q($l) q($T)
+  let ⟨vT, vTeq⟩ ← evalTpId q(show TpEnv Name from []) q($T)
+  let twf ← checkTm q($axioms) q([]) q($l) q($vT) q($t)
+  let value : Q(ReflectedDef $axioms) := q(
+    { l := $l
+      tp := $T
+      nfTp := $vT
+      wf_nfTp := $vTeq .nil <| $Twf $wf_axioms .nil
+      val := $t
+      wf_val := $twf $wf_axioms .nil <| $vTeq .nil <| $Twf $wf_axioms .nil
+    }
+  )
+
+  addDecl <| .defnDecl {
+    name := ci.name ++ reflectPostfix
+    levelParams := []
+    type := q(ReflectedDef $axioms)
+    /- The kernel does not max-share terms before checking them,
+    and our tactics are currently bad at producing highly shared terms.
+    Maximal sharing improves checking time asymptotically on some benchmarks (`bench.samplers.id`)
+    and by a constant factor on others (`bench.samplers.fn`). -/
+    value := ShareCommon.shareCommon' value
+    hints := .regular 0 -- TODO: what height?
+    safety := .safe
+  }
+
+/--
+When applied to a definition or axiom,
+this attribute reflects its type and value
+as deeply embedded `SynthLean.Expr` syntax
+together with a proof that the syntax is well-typed
+in SynthLean's minimal version of Martin-Löf type theory (MLTT).
+All this is stored in a new definition of type `CheckedDef` or `CheckedAx`,
+called `thisDef.reflection`.
+
+Note that SynthLean's MLTT does not support `Prop`
+and many features of Lean such as inductive types.
+The attribute will fail if these occur in the definition.
+-/
+initialize registerBuiltinAttribute {
+  name := `reflect
+  descr := "" -- Is `descr` even used for anything?
+  applicationTime := .afterCompilation
+  add := fun declName _stx _attrKind => do
+    match ← getConstInfo declName with
+    | .axiomInfo i => discard <| MetaM.run (addCheckedAx i)
+    | .defnInfo i => discard <| MetaM.run (addCheckedDef i)
+    | _ => throwError "Unsupported command."
+}
+
+-- Reflect definitions from our prelude as `Checked*`.
+run_meta do
+  let addAx (nm : Name) := do
+    let .axiomInfo i ← getConstInfo nm | throwError "internal error"
+    addCheckedAx i
+  let addDef (nm : Name) := do
+    let .defnInfo i ← getConstInfo nm | throwError "internal error"
+    addCheckedDef i
+  addDef ``Identity.rfl₀
+  addDef ``Identity.rfl₁
+  addDef ``Identity.symm₀
+  addDef ``Identity.symm₁
+  addDef ``Identity.trans₀
+  addDef ``Identity.trans₁
+  addAx ``sorryAx₀
+  addAx ``sorryAx₁
+  addAx ``sorryAx₂
+
+end SynthLean
diff --git a/HoTTLean/Frontend/Reflected.lean b/HoTTLean/Frontend/Reflected.lean
new file mode 100644
index 00000000..199e03fa
--- /dev/null
+++ b/HoTTLean/Frontend/Reflected.lean
@@ -0,0 +1,64 @@
+import HoTTLean.Syntax.Axioms
+import HoTTLean.Typechecker.Value
+
+/-! Structures that store deeply embedded axioms and definitions. -/
+
+namespace SynthLean
+
+variable {χ : Type*} {𝕋 : Axioms χ}
+
+/-- An axiom checked with respect to the theory `𝕋`. -/
+structure ReflectedAx (𝕋 : Axioms χ) where
+  name : χ
+  get_name : 𝕋 name = none
+  l : Nat
+  tp : Expr χ
+  nfTp : Val χ
+  wf_nfTp : ValEqTp 𝕋 [] l nfTp tp
+
+namespace ReflectedAx
+
+theorem wf_tp (a : ReflectedAx 𝕋) : 𝕋 ∣ [] ⊢[a.l] a.tp :=
+  a.wf_nfTp.wf_tp
+
+variable [DecidableEq χ]
+
+/-- The theory that `a` depends on, extended by `a`. -/
+noncomputable abbrev snocAxioms (a : ReflectedAx 𝕋) : Axioms χ :=
+  𝕋.snoc a.get_name a.wf_tp
+
+theorem le_snocAxioms (a : ReflectedAx 𝕋) : 𝕋 ≤ a.snocAxioms :=
+  𝕋.le_snoc_self ..
+
+theorem wf_snocAxioms (a : ReflectedAx 𝕋) (𝕋wf : 𝕋.Wf) : a.snocAxioms.Wf :=
+  𝕋wf.snoc a.get_name a.wf_tp
+
+/-- The axiom as a term. -/
+def val (a : ReflectedAx 𝕋) : Expr χ :=
+  .ax a.name a.tp
+
+theorem wf_val (a : ReflectedAx 𝕋) : a.snocAxioms ∣ [] ⊢[a.l] a.val : a.tp := by
+  unfold val
+  apply WfTm.ax .nil (𝕋.snoc_get ..)
+  apply a.wf_nfTp.wf_tp.of_axioms_le a.le_snocAxioms
+
+end ReflectedAx
+
+/-- A definition checked with respect to the theory `𝕋`. -/
+structure ReflectedDef (𝕋 : Axioms χ) where
+  l : Nat
+  tp : Expr χ
+  nfTp : Val χ
+  wf_nfTp : ValEqTp 𝕋 [] l nfTp tp
+  val : Expr χ
+  -- nfVal?
+  wf_val : 𝕋 ∣ [] ⊢[l] val : tp
+
+namespace ReflectedDef
+
+theorem wf_tp (d : ReflectedDef 𝕋) : 𝕋 ∣ [] ⊢[d.l] d.tp :=
+  d.wf_val.wf_tp
+
+end ReflectedDef
+
+end SynthLean
diff --git a/HoTTLean/Frontend/Shallow.lean b/HoTTLean/Frontend/Shallow.lean
new file mode 100644
index 00000000..a8966e3d
--- /dev/null
+++ b/HoTTLean/Frontend/Shallow.lean
@@ -0,0 +1,59 @@
+import Qq
+
+/-! Utilities for shallowly embedded representations of SynthLean expressions
+(i.e., for pretending that a `SynthLean.Expr` is a `Lean.Expr`). -/
+
+namespace SynthLean
+open Qq
+
+/-- An optional specification of the expected theory.
+
+Copied from `Lean.Parser.Tactic.valConfigItem`. -/
+syntax theorySpec := atomic(" (" &"theory" " := ") withoutPosition(term) ") "
+
+/-- A SynthLean type expression.
+
+#### Expected theory
+
+This macro needs to know the *expected theory* `𝕋`
+w.r.t. which the type `A` should be typechecked,
+so that we'll have `𝕋 ∣ [] ⊢[?l] A`.
+When the optional `(theory := thy)` argument is provided,
+the expected theory is `thy`.
+Otherwise the expected theory is inferred from the expected type `eT`:
+- When `eT = SynthLean.Expr s.SigInt` for `s : UHomSeq 𝒞`,
+  the expected theory is `s.thyInt`.
+- Otherwise inference fails. -/
+syntax "tp%" (theorySpec)? "{" term "}" : term
+/-- A SynthLean term expression. See `tp%{..}` for more info. -/
+syntax "tm%" (theorySpec)? "{" term "}" : term
+
+/-- *Deinterpretation* `⸨..⸩` (the *Scott unbracket*) works in any `tm%{..}/tp%{..}` context
+where the expected theory is `s.thyInt`.
+It allows us to name a semantic type in the syntax
+(so, in a sense, it is inverse to interpretation).
+
+It obeys the following rule,
+where `⊢[..]` is the internal typing judgment,
+and `⊢` is Lean's usual typing.
+```
+Γ ⊢ t : 𝟭_ _ ⟶ s[l].Ty
+---------------------------------
+s.thyInt ∣ · ⊢[l+1] ⸨t⸩ : .univ l
+```
+where `Γ` is the external local context
+in which `tm%{..}/tp%{..}` is being elaborated.
+
+TODO: Also support semantic term deinterpretation. -/
+syntax "⸨" term "⸩" : term
+
+/-- A representation of `⸨t⸩` in the shallow embedding.
+It can have whatever type is necessary.
+The external arrow `t` is stored in quoted form in `e`.
+It must be a closed expression and not refer to any global constants. -/
+/- FIXME: Double-quoting `e` may become a performance issue.
+One alternative would be to store an auxiliary definition in the environment,
+and use its name here. -/
+axiom SemAx.{u} (α : Type u) (e : Lean.Expr) : α
+
+end SynthLean
diff --git a/HoTTLean/Frontend/Translation.lean b/HoTTLean/Frontend/Translation.lean
index b9771a3e..4419735d 100644
--- a/HoTTLean/Frontend/Translation.lean
+++ b/HoTTLean/Frontend/Translation.lean
@@ -1,41 +1,59 @@
 import Qq
 import HoTTLean.Syntax.Axioms
-import HoTTLean.Frontend.Checked
+import HoTTLean.Typechecker.Util
+import HoTTLean.Frontend.Reflected
+import HoTTLean.Frontend.Instances
+import HoTTLean.Frontend.Shallow
 
 namespace SynthLean
 
 open Qq Lean Meta
 
-def traceClsTranslation : Name := `SynthLean.Translation
+namespace TraceCls
+def Translation := `SynthLean.Translation
+def translateAsTp := Translation ++ `asTp
+def translateAsTm := Translation ++ `asTm
 
 initialize
-  registerTraceClass traceClsTranslation
-  registerTraceClass (traceClsTranslation ++ `tp) (inherited := true)
-  registerTraceClass (traceClsTranslation ++ `tm) (inherited := true)
+  registerTraceClass Translation
+  registerTraceClass translateAsTp (inherited := true)
+  registerTraceClass translateAsTm (inherited := true)
+end TraceCls
 
-structure Context where
-  /-- The position of an `FVarId` is its de Bruijn index. -/
+def reflectPostfix : Name := `reflection
+
+
+structure Context {u : Level} (χ : Q(Type u)) where
+  /-- The `FVarId` of each active binder in the local context.
+  The position of an `FVarId` here is its de Bruijn index in the translated term. -/
   bvars : List FVarId := []
-  /-- The ordinary (external) Lean environment. -/
-  extEnv : Environment
+  /-- The theory that the translated term should be well-formed w.r.t. to.
+  We synthesize and insert theory maps to ensure this. -/
+  expectedTheory : Q(Axioms $χ)
 
-/-- `TranslateM` computations run in the internal environment
-(otherwise operations such as type inference on internal constants wouldn't work). -/
-abbrev TranslateM := ReaderT Context MetaM
+abbrev TranslateM {u : Level} (χ : Q(Type u)) := ReaderT (Context χ) MetaM
 
-def TranslateM.run {α : Type} (x : TranslateM α) (extEnv : Environment) : MetaM α :=
-  ReaderT.run x { extEnv }
+def TranslateM.run {α : Type} {u : Level} {χ : Q(Type u)} (x : TranslateM χ α)
+    (expectedTheory : Q(Axioms $χ)) : MetaM α :=
+  ReaderT.run x { expectedTheory }
 
-def withBinder {α : Type} (x : Lean.Expr) (k : TranslateM α) : TranslateM α := do
+def withBinder {α : Type} {u : Level} {χ : Q(Type u)} (x : Lean.Expr) (k : TranslateM χ α) :
+    TranslateM χ α := do
   withReader (fun s => { s with bvars := x.fvarId! :: s.bvars }) k
 
-/-- Extract the level `u` in `Sort u`.
-It must be monomorphic, i.e., may not contain universe variables. -/
-def getSortLevel (l : Level) : Lean.MetaM Nat := do
+/-- Extract the level `u` in `Sort l = Type u`.
+It must be monomorphic, i.e., may not contain universe variables.
+It may also not contain level metavariables. -/
+def getTypeLevel (l : Level) : Lean.MetaM Nat := do
+  let l ← instantiateLevelMVars l
+  if l.hasMVar then
+    throwError "unsupported universe (contains metavariables){indentExpr <| .sort l}"
+  if l.hasParam then
+    throwError "unsupported universe (contains level parameters){indentExpr <| .sort l}"
   match l.toNat with
   | .some (n+1) => return n
-  | .some 0 => throwError "unsupported universe{indentExpr <| .sort l}"
-  | .none => throwError "unsupported polymorphic universe level in{indentExpr <| .sort l}"
+  | .some 0 => throwError "unsupported proof-irrelevant universe{indentExpr <| .sort l}"
+  | _ => throwError "internal error"
 
 /-- Syntactically check if a Lean expression should be handled by the type translator.
 We use the term translator iff this returns `false`. -/
@@ -62,58 +80,72 @@ def mkId {u : Level} (χ : Q(Type u)) (l : Nat) : Q(Expr $χ) :=
       .lam $l ($l + 1) (.el <| .bvar 1) <|
         .code <| .Id $l (.el <| .bvar 2) (.bvar 1) (.bvar 0))
 
+/-- Get the theory w.r.t. which a checked entity is defined. -/
+def getTheoryOfChecked (e : Lean.Expr) : MetaM ((u : Level) × (χ : Q(Type u)) × Q(Axioms $χ)) := do
+  let ⟨u, α, e⟩ ← inferTypeQ' e
+  match α with
+  | ~q(@ReflectedAx $χ $E) =>
+    let _ ← synthInstanceQ q(DecidableEq $χ)
+    return ⟨u, q($χ), q(($e).snocAxioms)⟩
+  | ~q(@ReflectedDef $χ $E) => return ⟨u, q($χ), q($E)⟩
+  | _ => throwError "expected a `CheckedAx` or `CheckedDef`, got{indentExpr e}"
+
 mutual
 /-- Completeness: if the argument is well-formed in Lean,
 the output is well-typed in MLTT. -/
-partial def translateAsTp (e : Lean.Expr) : TranslateM (Nat × Q(Expr Lean.Name)) := do
-  Lean.withTraceNode (ε := Lean.Exception) (traceClsTranslation ++ `tp) (fun
+partial def translateAsTp {u : Level} (χ : Q(Type u)) (e : Lean.Expr) :
+    TranslateM χ (Nat × Q(Expr $χ)) := do
+  Lean.withTraceNode (ε := Lean.Exception) TraceCls.translateAsTp (fun
     | .ok ⟨l, A⟩ => do
-      let mA : MessageData ← withEnv (← read).extEnv <| addMessageContextPartial A
-      return m!"✅️ {e} [{l}]⇒ {mA}"
+      return m!"✅️ {e} [{l}]⇒ {A}"
     | .error _ => return m!"❌️ {e} ⇒ _") do
   if !isType e then
-    let ⟨l+1, a⟩ ← translateAsTm e
+    let ⟨l+1, a⟩ ← translateAsTm χ e
       | throwError "type code should have level > 0{indentExpr e}"
     return ⟨l, q(.el $a)⟩
   match e with
-  | .mdata _ e => translateAsTp e
+  | .mdata _ e => translateAsTp χ e
   | .sort l => do
-    let n : Nat ← getSortLevel l
+    let n : Nat ← getTypeLevel l
     return ⟨n+1, q(.univ $n)⟩
   | .forallE _ A .. =>
-    let ⟨l, A⟩ ← translateAsTp A
+    let ⟨l, A⟩ ← translateAsTp χ A
     let ⟨l', B⟩ ← forallBoundedTelescope e (some 1) fun xs B => do
       let #[x] := xs | throwError "internal error (forall tp)"
-      withBinder x <| translateAsTp B
+      withBinder x <| translateAsTp χ B
     return ⟨max l l', q(.pi $l $l' $A $B)⟩
   | _ => throwError "internal error: should fail `isType`{indentExpr e}"
 
-partial def translateAsTm (e : Lean.Expr) : TranslateM (Nat × Q(Expr Lean.Name)) := do
-  Lean.withTraceNode (ε := Lean.Exception) (traceClsTranslation ++ `tm) (fun
+partial def translateAsTm {u : Level} (χ : Q(Type u)) (e : Lean.Expr) :
+    TranslateM χ (Nat × Q(Expr $χ)) := do
+  Lean.withTraceNode (ε := Lean.Exception) TraceCls.translateAsTm (fun
     | .ok ⟨l, a⟩ => do
-      let ma : MessageData ← withEnv (← read).extEnv <| addMessageContextPartial a
-      return m!"✅️ {e} [{l}]⇒ {ma}"
+      return m!"✅️ {e} [{l}]⇒ {a}"
     | .error _ => return m!"❌️ {e} ⇒ _") do
   if isType e then
-    let ⟨l, A⟩ ← translateAsTp e
+    let ⟨l, A⟩ ← translateAsTp χ e
     return ⟨l+1, q(.code $A)⟩
   match e with
-  | .mdata _ e => translateAsTm e
+  | .mdata _ e => translateAsTm χ e
   | .fvar f => do
     let eTp ← inferType e
     let .sort l ← inferType eTp | throwError "internal error (sort)"
-    let n ← getSortLevel l
+    let n ← getTypeLevel l
     match (← read).bvars.findIdx? (· == f) with
     | some i => return ⟨n, q(.bvar $i)⟩
     | none => throwError "unexpected fvar{indentExpr e}"
   | .lam _ A .. =>
-    let ⟨l, A⟩ ← translateAsTp A
+    let ⟨l, A⟩ ← translateAsTp χ A
     let ⟨l', b⟩ ← lambdaBoundedTelescope e 1 fun xs b => do
       let #[x] := xs | throwError "internal error (lam tm)"
-      withBinder x <| translateAsTm b
+      withBinder x <| translateAsTm χ b
     return ⟨max l l', q(.lam $l $l' $A $b)⟩
   | .app fn arg => do
     if e.isAppOfArity' ``sorryAx 3 then
+      let .defEq _ ← isLevelDefEqQ u 0
+        | throwError "`sorry` can only be used with Lean.Name as the signature"
+      let .defEq _ ← isDefEqQ q($χ) q(Lean.Name)
+        | throwError "`sorry` can only be used with Lean.Name as the signature"
       let #[A, _, _] := e.getAppArgs | throwError "internalError"
       -- Recent versions of Lean generate ``sorryAx (Name → ActualType) `«sourceLocation»``.
       -- In `Frontend.Prelude` we have defined `sorryAxₗ` for `l < univMax`.
@@ -123,7 +155,7 @@ partial def translateAsTm (e : Lean.Expr) : TranslateM (Nat × Q(Expr Lean.Name)
         let tp ← inferType x
         if !(← isDefEq tp q(Lean.Name)) then
           throwError "unexpected type of sorryAx{Lean.indentExpr A}"
-        translateAsTp A'
+        translateAsTp χ A'
       let sl : Nat := l + 1
       let name : Q(Lean.Name) := toExpr <|
         Lean.Name.anonymous.str s!"sorryAx{Nat.subDigitChar l}"
@@ -131,51 +163,56 @@ partial def translateAsTm (e : Lean.Expr) : TranslateM (Nat × Q(Expr Lean.Name)
         q(.app $sl $l (.el <| .bvar 0)
           (.ax $name (.pi $sl $l (.univ $l) (.el <| .bvar 0)))
           (.code $A))⟩
+    if e.isAppOfArity' ``SemAx 2 then
+      let #[T, a] := e.getAppArgs | throwError "internal error"
+      let ⟨l, T⟩ ← translateAsTp χ T
+      let a : Q($χ) ← evalExprExpr a
+      return ⟨l, q(.ax $a $T)⟩
     if e.isAppOfArity' ``Sigma.mk 4 then
       let #[_, B, f, s] := e.getAppArgs | throwError "internal error"
       let ⟨l', B⟩ ← lambdaBoundedTelescope B 1 fun xs B => do
         let #[x] := xs | throwError "internal error (Sigma.mk)"
-        withBinder x <| translateAsTp B
-      let ⟨l, f⟩ ← translateAsTm f
-      let ⟨_, s⟩ ← translateAsTm s
+        withBinder x <| translateAsTp χ B
+      let ⟨l, f⟩ ← translateAsTm χ f
+      let ⟨_, s⟩ ← translateAsTm χ s
       return ⟨max l l', q(.pair $l $l' $B $f $s)⟩
     if e.isAppOfArity' ``Sigma.fst 3 then
       let #[A, B, p] := e.getAppArgs | throwError "internal error"
-      let ⟨l, A⟩ ← translateAsTp A
+      let ⟨l, A⟩ ← translateAsTp χ A
       let ⟨l', B⟩ ← lambdaBoundedTelescope B 1 fun xs B => do
         let #[x] := xs | throwError "internal error (Sigma.fst)"
-        withBinder x <| translateAsTp B
-      let ⟨_, p⟩ ← translateAsTm p
+        withBinder x <| translateAsTp χ B
+      let ⟨_, p⟩ ← translateAsTm χ p
       return ⟨l, q(.fst $l $l' $A $B $p)⟩
     if e.isAppOfArity' ``Sigma.snd 3 then
       let #[A, B, p] := e.getAppArgs | throwError "internal error"
-      let ⟨l, A⟩ ← translateAsTp A
+      let ⟨l, A⟩ ← translateAsTp χ A
       let ⟨l', B⟩ ← lambdaBoundedTelescope B 1 fun xs B => do
         let #[x] := xs | throwError "internal error (Sigma.snd)"
-        withBinder x <| translateAsTp B
-      let ⟨_, p⟩ ← translateAsTm p
+        withBinder x <| translateAsTp χ B
+      let ⟨_, p⟩ ← translateAsTm χ p
       return ⟨l', q(.snd $l $l' $A $B $p)⟩
     -- Defined in `Syntax.Frontend.Prelude`.
     if e.isAppOfArity' `Identity.refl 2 then
       let #[_, a] := e.getAppArgs | throwError "internal error (Id.refl)"
-      let ⟨l, a⟩ ← translateAsTm a
+      let ⟨l, a⟩ ← translateAsTm χ a
       return ⟨l, q(.refl $l $a)⟩
     if e.isAppOfArity' `Identity.rec 6 then
       let #[_, a, M, r, b, h] := e.getAppArgs | throwError "internal error (Id.rec)"
-      let ⟨l, a⟩ ← translateAsTm a
+      let ⟨l, a⟩ ← translateAsTm χ a
       let ⟨l', M⟩ ← lambdaBoundedTelescope M 2 fun xs M => do
         let #[x, h] := xs | throwError "internal error (Id.rec motive)"
-        withBinder x <| withBinder h <| translateAsTp M
-      let ⟨_, r⟩ ← translateAsTm r
-      let ⟨_, b⟩ ← translateAsTm b
-      let ⟨_, h⟩ ← translateAsTm h
+        withBinder x <| withBinder h <| translateAsTp χ M
+      let ⟨_, r⟩ ← translateAsTm χ r
+      let ⟨_, b⟩ ← translateAsTm χ b
+      let ⟨_, h⟩ ← translateAsTm χ h
       return ⟨l', q(.idRec $l $l' $a $M $r $b $h)⟩
     let fnTp ← inferType fn
-    let ⟨_, fn⟩ ← translateAsTm fn
-    let ⟨l, arg⟩ ← translateAsTm arg
+    let ⟨_, fn⟩ ← translateAsTm χ fn
+    let ⟨l, arg⟩ ← translateAsTm χ arg
     let ⟨l', B⟩ ← forallBoundedTelescope fnTp (some 1) fun xs B => do
       let #[x] := xs | throwError "internal error (app tm)"
-      withBinder x <| translateAsTp B
+      withBinder x <| translateAsTp χ B
     return ⟨l', q(.app $l $l' $B $fn $arg)⟩
   | .const ``Sigma [l, l'] =>
     /- FIXME: To simplify the translation,
@@ -185,23 +222,34 @@ partial def translateAsTm (e : Lean.Expr) : TranslateM (Nat × Q(Expr Lean.Name)
     But the max universe is deficient anyway -
     it can't have axiomatic function extensionality -
     so maybe this is fine. -/
-    let l ← getSortLevel l.succ
-    let l' ← getSortLevel l'.succ
+    let l ← getTypeLevel l.succ
+    let l' ← getTypeLevel l'.succ
     return ⟨max l l' + 1, mkSigma _ l l'⟩
   | .const `Identity [l] =>
-    let l ← getSortLevel l.succ
+    let l ← getTypeLevel l.succ
     return ⟨l + 1, mkId _ l⟩
   | .const nm [] =>
     let eTp ← inferType e
     let .sort l ← inferType eTp | throwError "internal error (sort)"
-    let n ← getSortLevel l
-    -- We translate internal constants to projections from external constants.
+    let n ← getTypeLevel l
+    -- We translate constants to projections of reflected constants.
     let ci ← getConstInfo nm
-    withEnv (← read).extEnv do
-      match ci with
-      | .defnInfo i => return ⟨n, ← mkAppM ``CheckedDef.val #[.const i.name []]⟩
-      | .axiomInfo i => return ⟨n, ← mkAppM ``CheckedAx.val #[.const i.name []]⟩
-      | _ => throwError "unsupported constant (not a `def` or an `axiom`){indentExpr e}"
+    let nm := ci.name ++ reflectPostfix
+    if !(← hasConst nm) then
+      throwError "Constant '{Expr.const ci.name []}' has not been reflected. \
+        Try marking it with `@[reflect]`."
+    let ⟨_, χ₀, E⟩ ← getTheoryOfChecked (.const nm [])
+    let val : Q(Expr $χ₀) := ← match ci with
+      | .defnInfo _ => mkAppM ``ReflectedDef.val #[.const nm []]
+      | .axiomInfo _ => mkAppM ``ReflectedAx.val #[.const nm []]
+      | _ => throwError "unsupported kind of constant (not a `def` or an `axiom`){indentExpr e}"
+    let E' := (← read).expectedTheory
+    if !(← isDefEq E E') then
+      let thyMap ← synthInstanceQ q(HasTheoryMap $E $E')
+      trace[SynthLean.Translation.asTm]
+        m!"inserting translation from{indentExpr E}\nto{indentExpr E'}"
+      return ⟨n, q(($val).map ($thyMap).map)⟩
+    return ⟨n, val⟩
   | .const .. => throwError "unsupported constant (universe-polymorphic){indentExpr e}"
   | e => throwError "unsupported term{indentExpr e}"
 
diff --git a/HoTTLean/Groupoids/UHom.lean b/HoTTLean/Groupoids/UHom.lean
index 9c7e29fa..7dcd08df 100644
--- a/HoTTLean/Groupoids/UHom.lean
+++ b/HoTTLean/Groupoids/UHom.lean
@@ -32,6 +32,7 @@ def uHomSeqHomSucc' (i : Nat) (h : i < 3) :
 -/
 def uHomSeq : UHomSeq Ctx.{4} where
   length := 3
+  univMax_le := by unfold SynthLean.univMax; omega
   objs := uHomSeqObjs
   homSucc' := uHomSeqHomSucc'
 
diff --git a/HoTTLean/HoTT0/Semantics.lean b/HoTTLean/HoTT0/Semantics.lean
new file mode 100644
index 00000000..5c09c970
--- /dev/null
+++ b/HoTTLean/HoTT0/Semantics.lean
@@ -0,0 +1,43 @@
+import HoTTLean.HoTT0.Theory
+import HoTTLean.Model.Unstructured.Interpretation
+import HoTTLean.Groupoids.UHom
+
+noncomputable section
+
+namespace GroupoidModel
+
+open SynthLean
+open Model UnstructuredUniverse Interpretation
+open CategoryTheory ChosenTerminal
+
+def emptyInterp : Interpretation Lean.Name uHomSeq where
+  ax _ _ _ := none
+
+instance : Fact (emptyInterp.Wf (.empty _)) := by
+  constructor; constructor; simp [emptyInterp, Axioms.empty]
+
+abbrev isGrpd₀_all_tp : 𝟭_ Ctx.{4} ⟶ uHomSeq[1].Ty :=
+  emptyInterp.interpTy HoTT0.isGrpd₀_all.wf_tp
+
+def isGrpd₀_all_witness : 𝟭_ Ctx.{4} ⟶ uHomSeq[1].Tm :=
+  sorry
+
+theorem isGrpd₀_all_witness_tp : isGrpd₀_all_witness ⋙ uHomSeq[1].tp = isGrpd₀_all_tp :=
+  sorry
+
+def hott₀Interp : Interpretation Lean.Name uHomSeq where
+  ax := fun
+    | ``HoTT0.isGrpd₀_all, 1, _ => isGrpd₀_all_witness
+    | _, _, _ => none
+
+instance : Fact (hott₀Interp.Wf HoTT0.isGrpd₀_all.snocAxioms) := by
+  constructor; constructor
+  intro c _ eq
+  simp [HoTT0.isGrpd₀_all, CheckedAx.snocAxioms, Axioms.snoc] at eq
+  split_ifs at eq
+  . cases eq
+    subst_vars
+    use isGrpd₀_all_witness
+    simp [hott₀Interp, isGrpd₀_all_witness_tp]
+    apply emptyInterp.interpTy_mem HoTT0.isGrpd₀_all.wf_tp
+  . cases eq
diff --git a/test/hott0.lean b/HoTTLean/HoTT0/Theory.lean
similarity index 54%
rename from test/hott0.lean
rename to HoTTLean/HoTT0/Theory.lean
index 2fb3f7a0..8fbd06a4 100644
--- a/test/hott0.lean
+++ b/HoTTLean/HoTT0/Theory.lean
@@ -1,54 +1,54 @@
 import HoTTLean.Frontend.Commands
 
+/-! Axioms of HoTT0 and basic constructions. -/
+
 noncomputable section
 
 declare_theory hott0
 
 namespace HoTT0
 
+/-! ## Sections and equivalences -/
+
 hott0 def isSection₀₀ {A B : Type} (f : A → B) (g : B → A) : Type :=
   ∀ (a : A), Identity (g (f a)) a
 
-hott0 def isEquiv₀₀ {A B : Type} (f : A → B) : Type :=
-  Σ (g : B → A),
-    Σ (h : B → A),
-      Σ (_ : isSection₀₀ f g),
-        isSection₀₀ h f
-
-hott0 def happly {A : Type} {B : A → Type} {f g : (a : A) → B a} :
-    Identity f g → (a : A) → Identity (f a) (g a) :=
-  fun h _ => h.rec .rfl₀
-
-hott0
-  /-- HoTT book, Axiom 2.9.3. -/
-  axiom funext₀₀ {A : Type} {B : A → Type} (f g : (a : A) → B a) :
-    isEquiv₀₀ (@happly _ _ f g)
-
 hott0 def isSection₁₀ {A : Type 1} {B : Type} (f : A → B) (g : B → A) : Type 1 :=
   ∀ (a : A), Identity (g (f a)) a
 
 hott0 def isSection₀₁ {A : Type} {B : Type 1} (f : A → B) (g : B → A) : Type :=
   ∀ (a : A), Identity (g (f a)) a
 
+hott0 def isEquiv₀₀ {A B : Type} (f : A → B) : Type :=
+  Σ (g : B → A),
+    Σ (h : B → A),
+      Σ (_ : isSection₀₀ f g),
+        isSection₀₀ h f
+
 hott0 def isEquiv₁₀ {A : Type 1} {B : Type} (f : A → B) : Type 1 :=
   Σ (g : B → A),
     Σ (h : B → A),
       Σ (_ : isSection₁₀ f g),
         isSection₀₁ h f
 
-hott0 def isEquiv₁₀_grpd {A : Type 1} {B : Type} (f : A → B) : Type 1 :=
-  Σ (g : B → A),
-    Σ (_ : isSection₁₀ f g),
-      isSection₀₁ g f
+/-! ## Function extensionality -/
 
-hott0 def transport₀ {A B : Type} (h : Identity A B) (a : A) : B :=
-  h.rec a
+hott0 def happly₀₀ {A : Type} {B : A → Type} {f g : (a : A) → B a} :
+    Identity f g → (a : A) → Identity (f a) (g a) :=
+  fun h _ => h.rec .rfl₀
 
-hott0 def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv₀₀ (transport₀ h) :=
-  h.rec ⟨fun a => a, fun a => a, fun _ => .rfl₀, fun _ => .rfl₀⟩
+hott0
+  /-- HoTT book, Axiom 2.9.3. -/
+  axiom isEquiv₀₀_happly₀₀ {A : Type} {B : A → Type} (f g : (a : A) → B a) :
+    isEquiv₀₀ (@happly₀₀ _ _ f g)
 
-hott0 def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
-  fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
+hott0 def funext₀₀ {A : Type} {B : A → Type} {f g : (a : A) → B a} :
+    (∀ a : A, Identity (f a) (g a)) → Identity f g :=
+  -- TODO: frontend rejects auxiliary match-defintion
+  -- let ⟨F, _⟩ := isEquiv₀₀_happly₀₀ f g
+  fun h => (isEquiv₀₀_happly₀₀ f g).fst h
+
+/-! ## H-level -/
 
 hott0
   /-- The type `A` is (-1)-truncated. -/
@@ -60,7 +60,48 @@ hott0
   def isSet₀ (A : Type) : Type :=
     ∀ (a b : A), isProp₀ (Identity a b)
 
+hott0
+  /-- The type `A` is 1-truncated. -/
+  def isGrpd₀ (A : Type) : Type :=
+    ∀ (a b : A), isSet₀ (Identity a b)
+
+/-! ## Set univalence -/
+
+hott0 def transport₀ {A B : Type} (h : Identity A B) (a : A) : B :=
+  h.rec a
+
+hott0 def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv₀₀ (transport₀ h) :=
+  h.rec ⟨fun a => a, fun a => a, fun _ => .rfl₀, fun _ => .rfl₀⟩
+
+hott0 def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
+  fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
+
 hott0
   /-- The univalence axiom for sets. See HoTT book, Axiom 2.10.3. -/
   axiom setUv₀₀ {A B : Type} (A_set : isSet₀ A) (B_set : isSet₀ B) :
     isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
+
+/-! ## Groupoids -/
+
+hott0
+  /-- Every type is a groupoid. -/
+  axiom isGrpd₀_all (A : Type) : isGrpd₀ A
+
+hott0 def grpdIsEquiv₀₀ {A B : Type} (f : A → B) : Type :=
+  Σ (g : B → A),
+    Σ (_ : isSection₀₀ f g),
+      isSection₀₀ g f
+
+hott0 def ofGrpdIsEquiv₀₀ {A B : Type} {f : A → B} :
+    grpdIsEquiv₀₀ f → isEquiv₀₀ f :=
+  fun e => ⟨e.1, e.1, e.2.1, e.2.2⟩
+
+hott0 def grpdIsEquiv₀₀_ofGrpdIsEquiv₀₀ {A B : Type} (f : A → B) :
+    grpdIsEquiv₀₀ (ofGrpdIsEquiv₀₀ (f := f)) :=
+  sorry
+
+hott0 def isEquiv₀₀_ofGrpdIsEquiv₀₀ {A B : Type} (f : A → B) :
+    isEquiv₀₀ (ofGrpdIsEquiv₀₀ (f := f)) :=
+  -- TODO: frontend timeout
+  -- ofGrpdIsEquiv₀₀ (grpdIsEquiv₀₀_ofGrpdIsEquiv₀₀ f)
+  sorry
diff --git a/HoTTLean/Model/Natural/NaturalModel.lean b/HoTTLean/Model/Natural/NaturalModel.lean
index 3671be69..57659ea2 100644
--- a/HoTTLean/Model/Natural/NaturalModel.lean
+++ b/HoTTLean/Model/Natural/NaturalModel.lean
@@ -267,6 +267,7 @@ lemma snd_mk (A : y(Γ) ⟶ M.Ty) (B : y(M.ext A) ⟶ X) :
     snd M (mk M A B) _ (fst_mk ..) = B := by
   dsimp only [snd, mk]
   rw! [UvPoly.Equiv.snd'_mk']
+  rfl
 
 section
 variable {Δ : Ctx} {σ : Δ ⟶ Γ} {AB : y(Γ) ⟶ M.Ptp.obj X}
@@ -1152,7 +1153,7 @@ lemma comp_j : ym(ii.motiveSubst σ _) ≫ j i a C r r_tp =
     j i (ym(σ) ≫ a) (ym(ii.motiveSubst σ _) ≫ C) (ym(σ) ≫ r) (by
       simp [r_tp, IdIntro.comp_reflSubst'_assoc]) := by
   simp only [j]
-  conv => rhs; rw! [i.lift_comp_left a C r r_tp]
+  rw! [i.lift_comp_left a C r r_tp]
   rw [ie.equivSnd_comp_left]
   simp only [← Category.assoc]
   congr 1
diff --git a/HoTTLean/Model/Unstructured/InternalTheory.lean b/HoTTLean/Model/Unstructured/InternalTheory.lean
new file mode 100644
index 00000000..49162c46
--- /dev/null
+++ b/HoTTLean/Model/Unstructured/InternalTheory.lean
@@ -0,0 +1,69 @@
+import HoTTLean.Syntax.InversionLemmas
+import HoTTLean.Model.Unstructured.Interpretation
+
+/-! ## The internal theory of an unstructured model -/
+
+namespace Model.UnstructuredUniverse.UHomSeq
+
+open SynthLean
+open Interpretation
+open CategoryTheory ChosenTerminal
+
+universe v u
+variable {𝒞 : Type u} [Category.{v} 𝒞] [ChosenTerminal 𝒞]
+variable (s : UHomSeq 𝒞)
+
+/-- The signature of the internal theory of `s`.
+It includes a name for each semantic term and each semantic type
+at every universe level strictly below `univMax`. -/
+inductive SigInt
+  | tm {l} (llen : l < univMax) (t : 𝟭_ 𝒞 ⟶ s[l].Tm)
+  | ty {l} (llen : l < univMax) (A : 𝟭_ 𝒞 ⟶ s[l].Ty)
+
+/-- The internal theory of a model `s`.
+
+The syntactic type of a semantic type constant is the universe it lives in.
+The syntactic type of a semantic term constant is (`el` of) its semantic type as a constant. -/
+def thyInt : Axioms s.SigInt
+  | .tm (l := l) llen t =>
+    some ⟨
+      (.el (.ax (.ty llen (t ≫ s[l].tp)) (.univ l)), l),
+      by simp [Expr.isClosed]; omega⟩
+  | .ty (l := l) _ A =>
+    some ⟨
+      (.univ l, l+1),
+      by simp [Expr.isClosed]; omega⟩
+
+theorem thyInt_wf : s.thyInt.Wf :=
+  fun
+    | .tm (l := l) _ t, _, get => by
+      simp only [thyInt, Option.some.injEq] at get
+      rw [← get]
+      apply WfTp.el
+      apply WfTm.ax (Al := s.thyInt (.ty ‹_› (t ≫ s[l].tp)) |>.get rfl) .nil
+      . simp
+      . apply WfTp.univ .nil ‹_›
+    | .ty .., _, get => by
+      simp only [thyInt, Option.some.injEq] at get
+      subst_vars
+      apply WfTp.univ .nil ‹_›
+
+/-- Interpretation of the internal signature of `s`. -/
+def interpSigInt : Interpretation s.SigInt s where
+  ax := fun
+    | .tm (l := l) _ t, l', _ => if eq : l = l' then some (eq ▸ t) else none
+    | .ty (l := l) _ A, l', _ => if eq : l+1 = l' then some (eq ▸ s.code (by omega) A) else none
+
+variable [s.PiSeq] [s.SigSeq] [s.IdSeq]
+
+theorem interpSigInt_wf : s.interpSigInt.Wf s.thyInt where
+  ax := @fun
+    | .tm _ t, _, get => by
+      cases get
+      simp [interpSigInt, ofType, comp_code]
+      simp [nilCObj]; get_elem_tactic
+    | .ty _ t, _, get => by
+      cases get
+      simp [interpSigInt, ofType, nilCObj]
+
+end Model.UnstructuredUniverse.UHomSeq
diff --git a/HoTTLean/Model/Unstructured/Interpretation.lean b/HoTTLean/Model/Unstructured/Interpretation.lean
index 521e84d3..0eab8c00 100644
--- a/HoTTLean/Model/Unstructured/Interpretation.lean
+++ b/HoTTLean/Model/Unstructured/Interpretation.lean
@@ -20,7 +20,7 @@ namespace Model.UnstructuredUniverse
 
 open SynthLean
 
-variable {𝒞 : Type u} [Category 𝒞] (M : UnstructuredUniverse 𝒞)
+variable {𝒞 : Type u} [Category.{v} 𝒞] (M : UnstructuredUniverse 𝒞)
 variable [ChosenTerminal 𝒞]
 
 open ChosenTerminal
@@ -28,22 +28,21 @@ open ChosenTerminal
 /-! ## Universe level bound helpers -/
 
 section univBounds
-variable {s : UHomSeq 𝒞} (slen : univMax ≤ s.length)
+variable {s : UHomSeq 𝒞}
 variable {χ : Type*} {E : Axioms χ} {Γ : Ctx χ} {A B t u : Expr χ} {l : Nat}
-include slen
 
 theorem _root_.SynthLean.EqTp.lt_slen (H : E ∣ Γ ⊢[l] A ≡ B) : l < s.length + 1 := by
   have := H.le_univMax
-  omega
+  get_elem_tactic
 
 theorem _root_.SynthLean.WfTp.lt_slen (H : E ∣ Γ ⊢[l] A) : l < s.length + 1 :=
-  (EqTp.refl_tp H).lt_slen slen
+  (EqTp.refl_tp H).lt_slen
 
 theorem _root_.SynthLean.EqTm.lt_slen (H : E ∣ Γ ⊢[l] t ≡ u : A) : l < s.length + 1 :=
-  H.wf_tp.lt_slen slen
+  H.wf_tp.lt_slen
 
 theorem _root_.SynthLean.WfTm.lt_slen (H : E ∣ Γ ⊢[l] t : A) : l < s.length + 1 :=
-  H.wf_tp.lt_slen slen
+  H.wf_tp.lt_slen
 
 end univBounds
 
@@ -56,7 +55,7 @@ where `Γ` is a prefix of `Γ'`.
 It witnesses a sequence of context extension operations in `s`
 that built `Γ'` on top of `Γ`.
 We write `Γ ≤ Γ'`. -/
-inductive ExtSeq (s : UHomSeq 𝒞) (Γ : 𝒞) : 𝒞 → Type u where
+inductive ExtSeq (s : UHomSeq 𝒞) (Γ : 𝒞) : 𝒞 → Type (max u v) where
   | nil : s.ExtSeq Γ Γ
   | snoc {Γ'} {l : Nat} (d : s.ExtSeq Γ Γ') (llen : l < s.length + 1) (A : Γ' ⟶ s[l].Ty) :
     s.ExtSeq Γ (s[l].ext A)
@@ -209,7 +208,7 @@ i.e., one of the form `1.Aₙ₋₁.….A₀`,
 together with the extension sequence `[Aₙ₋₁ :: … :: A₀]`.
 
 This kind of object can be destructured. -/
-def CObj (s : UHomSeq 𝒞) : Type u := Σ Γ : 𝒞, s.ExtSeq (𝟭_ 𝒞) Γ
+def CObj (s : UHomSeq 𝒞) : Type (max u v) := Σ Γ : 𝒞, s.ExtSeq (𝟭_ 𝒞) Γ
 
 def nilCObj (s : UHomSeq 𝒞) : s.CObj :=
   ⟨𝟭_ 𝒞, .nil⟩
@@ -398,10 +397,11 @@ end
 
 def ofCtx : Ctx χ → Part s.CObj
   | [] => return s.nilCObj
-  | (A,l) :: Γ => do
-    Part.assert (l < s.length + 1) fun llen => do
-    let sΓ ← ofCtx Γ
-    let sA ← I.ofType sΓ l A
+  | (A,l) :: Γ =>
+    Part.assert (l < s.length + 1) fun llen =>
+    Part.bind (ofCtx Γ) fun sΓ =>
+    -- This universe-polymorphic bind breaks `do` notation.
+    Part.bind (I.ofType sΓ l A) fun sA =>
     return sΓ.snoc llen sA
 
 @[simp]
@@ -567,7 +567,7 @@ theorem mem_ofType_univ {Γ l i} {llen : l < s.length + 1} {x} :
 @[simp]
 theorem mem_ofCtx_snoc {Γ A l sΓ'} : sΓ' ∈ I.ofCtx ((A,l) :: Γ) ↔
     ∃ sΓ ∈ I.ofCtx Γ, ∃ llen, ∃ sA ∈ I.ofType sΓ l A llen, sΓ' = sΓ.snoc llen sA := by
-  simp only [ofCtx, Part.pure_eq_some, Part.bind_eq_bind, Part.mem_assert_iff, Part.mem_bind_iff,
+  simp only [ofCtx, Part.pure_eq_some, Part.mem_assert_iff, Part.mem_bind_iff,
     Part.mem_some_iff]
   tauto
 
@@ -656,7 +656,6 @@ end CSb
 /-! ## Admissibility of substitution -/
 
 open UHomSeq PolymorphicSigma PolymorphicPi PolymorphicIdIntro PolymorphicIdElim
-variable (slen : univMax ≤ s.length)
 
 theorem mem_ofType_ofTerm_subst' {full}
     (IH : full = true → ∀ {Δ Γ l} (llen : l < s.length + 1) {sσ} (σ : I.CSb Δ Γ sσ false) {se e},
@@ -887,9 +886,8 @@ theorem WfCtxIH.nil : I.WfCtxIH [] := by simp [WfCtxIH]
 theorem WfCtxIH.snoc {Γ A l} : I.WfTpIH Γ l A → I.WfCtxIH ((A, l) :: Γ)
   | ⟨_, hΓ, llen, _, hA⟩ => ⟨_, I.mem_ofCtx_snoc.2 ⟨_, hΓ, llen, _, hA, rfl⟩⟩
 
-include slen in
 theorem WfTpIH.univ {Γ l} (_ : l < univMax) : I.WfCtxIH Γ → I.WfTpIH Γ (l + 1) (Expr.univ l)
-  | ⟨_, hΓ⟩ => ⟨_, hΓ, by omega, _, I.mem_ofType_univ.2 ⟨rfl, rfl⟩⟩
+  | ⟨_, hΓ⟩ => ⟨_, hΓ, by get_elem_tactic, _, I.mem_ofType_univ.2 ⟨rfl, rfl⟩⟩
 
 theorem EqTpIH.pi {Γ A A' B B' l l'} :
     I.EqTpIH Γ l A A' → I.EqTpIH ((A, l) :: Γ) l' B B' →
@@ -935,11 +933,10 @@ theorem EqTpIH.el {Γ A A' l} : I.EqTmIH Γ (l + 1) (Expr.univ l) A A' → I.EqT
       I.mem_ofType_el.2 ⟨_, _, ht, ttp, rfl⟩,
       I.mem_ofType_el.2 ⟨_, _, ht', ttp, rfl⟩⟩
 
-include slen in
 theorem EqTpIH.el_code {Γ A l} (_ : l < univMax) : I.WfTpIH Γ l A → I.EqTpIH Γ l A.code.el A
   | ⟨_, hΓ', _, _, hA⟩ =>
     ⟨_, ‹_›, ‹_›, _,
-      I.mem_ofType_el.2 ⟨by omega, _,
+      I.mem_ofType_el.2 ⟨by get_elem_tactic, _,
         I.mem_ofTerm_code.2 ⟨_, rfl, _, hA, by simp; rfl⟩, s.code_tp .., rfl⟩,
       by rwa [s.el_code]⟩
 
@@ -1083,11 +1080,10 @@ theorem EqTmIH.idRec {Γ A M M' t t' r r' u u' h h' l l'} :
       simp [ttp]
     · simp
 
-include slen in
 theorem EqTmIH.code {Γ A A' l} (_ : l < univMax) :
     I.EqTpIH Γ l A A' → I.EqTmIH Γ (l + 1) (Expr.univ l) A.code A'.code
   | ⟨_, hΓ, _, _, hA, hA'⟩ =>
-    ⟨_, hΓ, by omega, _,
+    ⟨_, hΓ, by get_elem_tactic, _,
       I.mem_ofType_univ.2 ⟨rfl, by simp⟩, _,
       I.mem_ofTerm_code.2 ⟨_, rfl, _, hA, by simp; rfl⟩,
       I.mem_ofTerm_code.2 ⟨_, rfl, _, hA', by simp⟩,
@@ -1152,7 +1148,7 @@ theorem EqTmIH.idRec_refl {Γ A M t r l l'} :
     have sr := rtp ▸ Part.mem_unique hR sM
     have ir := I.mem_ofTerm_idRec.2 ⟨_, _, ht, _, ttp, B, by simp [Beq, sAeq],
       _, hM, _, hr, by simp [ttp, sr], _, ht, ttp, _, h1, by simp [ttp],
-        by rw! [ttp, PolymorphicIdElim.idRec_refl (I_eq := _)]⟩
+        by rw! [ttp, PolymorphicIdElim.idRec_refl (I_eq := _)]; rfl⟩
     ⟨_, hΓ, _, _, sM, _, ir, hr, sr⟩
   simp [Beq, ← Id_comp, sAeq, ttp]
 
@@ -1214,21 +1210,21 @@ theorem EqTmIH.trans {Γ A t t' t'' l} :
 
 /-- `I` is a well-formed interpretation of the axiom environment `E`. -/
 structure Wf (I : Interpretation χ s) (E : Axioms χ) : Prop where
-  ax {c Al} (Ec : E c = some Al) :
+  ax ⦃c Al⦄ (Ec : E c = some Al) :
     ∃ sc, I.ax c Al.1.2 = some sc ∧
-    ∃ sA : (𝟭_ 𝒞) ⟶ s[Al.1.2].Ty,
+    ∃ sA : 𝟭_ 𝒞 ⟶ s[Al.1.2].Ty,
       sA ∈ I.ofType s.nilCObj Al.1.2 Al.1.1 ∧
       sc ≫ s[Al.1.2].tp = sA
 
-variable {E : Axioms χ} {slen} [Iwf : Fact (I.Wf slen E)]
+variable {E : Axioms χ} [Iwf : Fact (I.Wf E)]
 include Iwf
 
 theorem WfTmIH.ax {Γ c Al} (Ec : E c = some Al) :
     I.WfCtxIH Γ → I.WfTmIH Γ Al.val.2 Al.val.1 (Expr.ax c Al.val.1)
   | ⟨Γ, hΓ⟩ => by
     have ⟨_, eq, _, sA, sA_tp⟩ := Iwf.out.ax Ec
-    have := I.mem_ofType_of_isClosed Al.2.1 Γ (by omega) sA
-    refine ⟨_, hΓ, by omega, _, this, ?_⟩
+    have := I.mem_ofType_of_isClosed Al.2.1 Γ (by get_elem_tactic) sA
+    refine ⟨_, hΓ, by get_elem_tactic, _, this, ?_⟩
     simp [ofTerm, eq, sA_tp]
 
 theorem ofType_ofTerm_sound :
@@ -1245,14 +1241,14 @@ theorem ofType_ofTerm_sound :
   case pi' => exact fun _ _ h1 h2 => (h1.refl.pi h2.refl).left
   case sigma' => exact fun _ _ h1 h2 => (h1.refl.sigma h2.refl).left
   case Id' => exact fun _ _ _ h1 h2 h3 => (h1.refl.Id h2.refl h3.refl).left
-  case univ => exact fun _ => .univ slen
+  case univ => exact fun _ => .univ
   case el => exact fun _ h1 => (EqTpIH.el h1.refl).left
 
   case cong_pi' => exact fun _ _ _ _ _ _ => .pi
   case cong_sigma' => exact fun _ _ _ _ _ _ => .sigma
   case cong_Id => exact fun _ _ _ => .Id
   case cong_el => exact fun _ => .el
-  case el_code => exact fun h _ => .el_code slen h
+  case el_code => exact fun h _ => .el_code h
   case refl_tp => exact fun _ h => h.refl
   case symm_tp => exact fun _ => .symm
   case trans_tp => exact fun _ _ => .trans
@@ -1267,7 +1263,7 @@ theorem ofType_ofTerm_sound :
   case refl' => exact fun _ _ _ h1 => h1.refl.refl_tm.left
   case idRec' => exact fun _ _ _ _ _ _ _ h1 h2 h3 h4 h5 =>
     (h1.refl.idRec h2.refl h3.refl h4.refl h5.refl).left
-  case code => exact fun h _ h1 => (EqTmIH.code slen h h1.refl).left
+  case code => exact fun h _ h1 => (EqTmIH.code h h1.refl).left
   case conv => exact fun _ _ h1 h2 => (h1.refl.conv h2).left
 
   case cong_lam' => exact fun _ _ _ _ _ _ => .lam
@@ -1277,7 +1273,7 @@ theorem ofType_ofTerm_sound :
   case cong_snd' => exact fun _ _ _ _ _ h1 h2 h3 => (h3.fst_snd h1 h2).2
   case cong_refl' => exact fun _ _ _ => .refl_tm
   case cong_idRec' => exact fun _ _ _ _ _ _ _ _ _ => .idRec
-  case cong_code => exact fun h _ => .code slen h
+  case cong_code => exact fun h _ => .code h
   case app_lam' => exact fun _ _ _ _ _ _ => .app_lam
   case fst_pair' => exact fun _ _ _ _ _ h1 h2 h3 => (EqTmIH.fst_snd_pair h1 h2 h3).1
   case snd_pair' => exact fun _ _ _ _ _ h1 h2 h3 => (EqTmIH.fst_snd_pair h1 h2 h3).2
@@ -1302,8 +1298,8 @@ def interpCtx (H : WfCtx E Γ) : s.CObj :=
   Part.get_mem ..
 
 /-- Given `Γ, l, A` s.t. `Γ ⊢[l] A`, return `⟦A⟧_⟦Γ⟧`. -/
-def interpTy (H : E ∣ Γ ⊢[l] A) : (I.interpCtx H.wf_ctx |>.1) ⟶ (s[l]'(H.lt_slen slen)).Ty :=
-  (I.ofType _ l A (H.lt_slen slen)).get <| by
+def interpTy (H : E ∣ Γ ⊢[l] A) : (I.interpCtx H.wf_ctx |>.1) ⟶ (s[l]'H.lt_slen).Ty :=
+  (I.ofType _ l A H.lt_slen).get <| by
     have ⟨_, h1, _, h2⟩ := I.ofType_ofTerm_sound.2.1 H
     cases Part.mem_unique (I.interpCtx_mem H.wf_ctx) h1
     apply Part.dom_iff_mem.mpr h2
@@ -1320,8 +1316,8 @@ theorem interpTy_eq (H : E ∣ Γ ⊢[l] A ≡ B) :
 
 /-- Given `Γ, l, t, A` s.t. `Γ ⊢[l] t : A`, return `⟦t⟧_⟦Γ⟧`. -/
 def interpTm (H : E ∣ Γ ⊢[l] t : A) :
-    (I.interpCtx H.wf_ctx |>.1) ⟶ (s[l]'(H.lt_slen slen)).Tm :=
-  (I.ofTerm _ l t (H.lt_slen slen)).get <| by
+    (I.interpCtx H.wf_ctx |>.1) ⟶ (s[l]'H.lt_slen).Tm :=
+  (I.ofTerm _ l t H.lt_slen).get <| by
     have ⟨_, h1, _, _, _, _, ⟨h2, rfl⟩, _⟩ := I.ofType_ofTerm_sound.2.2.2.1 H
     cases Part.mem_unique (I.interpCtx_mem H.wf_ctx) h1
     exact h2
@@ -1330,7 +1326,7 @@ def interpTm (H : E ∣ Γ ⊢[l] t : A) :
   Part.get_mem ..
 
 @[simp] theorem interpTm_tp (H : E ∣ Γ ⊢[l] t : A) :
-    I.interpTm H ≫ (s[l]'(H.lt_slen slen)).tp = I.interpTy H.wf_tp := by
+    I.interpTm H ≫ (s[l]'H.lt_slen).tp = I.interpTy H.wf_tp := by
   have ⟨_, h1, _, _, ⟨_, rfl⟩, _, ⟨_, rfl⟩, h2⟩ := I.ofType_ofTerm_sound.2.2.2.1 H
   cases Part.mem_unique (I.interpCtx_mem H.wf_ctx) h1
   exact h2
diff --git a/HoTTLean/Model/Unstructured/UHom.lean b/HoTTLean/Model/Unstructured/UHom.lean
index 3c05dc06..2f9e8d19 100644
--- a/HoTTLean/Model/Unstructured/UHom.lean
+++ b/HoTTLean/Model/Unstructured/UHom.lean
@@ -1,6 +1,7 @@
 import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
 import HoTTLean.ForMathlib
 import HoTTLean.Model.Unstructured.UnstructuredUniverse
+import HoTTLean.Syntax.Typing
 
 /-! Morphisms of unstructured models, and Russell-universe embeddings. -/
 
@@ -193,11 +194,22 @@ structure UHomSeq where
   /-- Number of embeddings in the sequence,
   or one less than the number of models in the sequence. -/
   length : Nat
+  univMax_le : SynthLean.univMax ≤ length
   objs (i : Nat) (h : i < length + 1) : UnstructuredUniverse Ctx
   homSucc' (i : Nat) (h : i < length) : UHom (objs i <| by omega) (objs (i + 1) <| by omega)
 
 namespace UHomSeq
 
+/-- Enable index notation `s[-]` to use the field `univMax_le`,
+as well as the concrete value of `univMax`. -/
+macro_rules
+  | `(tactic| get_elem_tactic_extensible) =>
+    `(tactic| (
+      have := Model.UnstructuredUniverse.UHomSeq.univMax_le ‹_›
+      have that := this
+      unfold SynthLean.univMax at that
+      omega))
+
 variable (s : UHomSeq Ctx)
 
 instance : GetElem (UHomSeq Ctx) Nat (UnstructuredUniverse Ctx) (fun s i => i < s.length + 1) where
diff --git a/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean b/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean
index 5e57936b..7304600a 100644
--- a/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean
+++ b/HoTTLean/Model/Unstructured/UnstructuredUniverse.lean
@@ -28,7 +28,7 @@ structure UnstructuredUniverse (Ctx : Type u) [Category Ctx] where
 
 namespace UnstructuredUniverse
 
-variable {Ctx : Type u} [Category Ctx] (M : UnstructuredUniverse Ctx)
+variable {Ctx : Type u} [Category.{v} Ctx] (M : UnstructuredUniverse Ctx)
 
 @[reassoc (attr := simp)]
 theorem var_tp {Γ : Ctx} (A : Γ ⟶ M.Ty) : M.var A ≫ M.tp = (M.disp A) ≫ A := by
@@ -320,12 +320,14 @@ lemma fst_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA} (eq) {B : U0.ex
     S.fst (U0.substWk σ A σA eq ≫ B) (σ ≫ s) (by simp [s_tp, S.Sig_comp]) =
     σ ≫ S.fst B s s_tp := by
   rw! [(S.pair_fst_snd B s (by simp [s_tp])).symm, ← S.pair_comp, S.fst_pair, S.fst_pair]
+  rfl
 
 lemma snd_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA} (eq) {B : U0.ext A ⟶ U1.Ty}
     (s : Γ ⟶ U2.Tm) (s_tp : s ≫ U2.tp = S.Sig B) :
     S.snd (U0.substWk σ A σA eq ≫ B) (σ ≫ s) (by simp [s_tp, S.Sig_comp]) =
     σ ≫ S.snd B s s_tp := by
   rw! [(S.pair_fst_snd B s (by simp [s_tp])).symm, ← S.pair_comp, S.snd_pair, S.snd_pair]
+  rfl
 
 end PolymorphicSigma
 
@@ -362,7 +364,7 @@ lemma unLam_comp {Γ Δ} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA} (eq) {B : U0.
     P.unLam (U0.substWk σ A σA eq ≫ B) (σ ≫ f) (by simp [f_tp, P.Pi_comp]) =
     U0.substWk σ A σA eq ≫ P.unLam B f f_tp := by
   rw [← P.unLam_lam (U0.substWk σ A σA eq ≫ B) (U0.substWk σ A σA eq ≫ P.unLam B f f_tp)]
-  . rw! [P.lam_comp σ eq B, P.lam_unLam]
+  . rw! [P.lam_comp σ eq B, P.lam_unLam]; rfl
   . rw [Category.assoc, P.unLam_tp]
 
 /--
diff --git a/HoTTLean/Syntax/Autosubst.lean b/HoTTLean/Syntax/Autosubst.lean
index 97def38e..7609b421 100644
--- a/HoTTLean/Syntax/Autosubst.lean
+++ b/HoTTLean/Syntax/Autosubst.lean
@@ -23,6 +23,10 @@ theorem snoc_zero {X} (σ : Nat → X) (x : X) : snoc σ x 0 = x := rfl
 @[simp]
 theorem snoc_succ {X} (σ : Nat → X) (x : X) (n) : snoc σ x (n + 1) = σ n := rfl
 
+theorem snoc_map_comp {χ χ'} (f : χ → χ') (σ : Nat → Expr χ) (e : Expr χ) :
+    snoc (map f ∘ σ) (e.map f) = map f ∘ snoc σ e := by
+  funext n; cases n <;> simp
+
 /-! ## Renaming -/
 
 variable {χ : Type*}
@@ -56,6 +60,10 @@ def rename (ξ : Nat → Nat) : Expr χ → Expr χ
   | .el a => .el (a.rename ξ)
   | .code A => .code (A.rename ξ)
 
+theorem rename_map {χ'} (f : χ → χ') (ξ : Nat → Nat) (e : Expr χ) :
+    (e.rename ξ).map f = (e.map f).rename ξ := by
+  induction e generalizing ξ <;> simp [rename, map] at * <;> grind
+
 /-! ## Substitution -/
 
 /-- Lift a substitution under a binder.
@@ -70,6 +78,11 @@ Warning: don't unfold this definition! Use `up_eq_snoc` instead. -/
 def up (σ : Nat → Expr χ) : Nat → Expr χ :=
   snoc (rename Nat.succ ∘ σ) (.bvar 0)
 
+theorem up_map_comp {χ'} (f : χ → χ') (σ : Nat → Expr χ) : up (map f ∘ σ) = map f ∘ up σ := by
+  funext n
+  cases n <;> simp [up, rename_map]
+  . simp [map]
+
 -- TODO: upN
 
 @[simp]
@@ -103,6 +116,10 @@ theorem subst_bvar (χ) : subst (χ := χ) Expr.bvar = id := by
 theorem subst_snoc_zero (σ : Nat → Expr χ) (t : Expr χ) : subst (snoc σ t) (.bvar 0) = t := by
   dsimp [subst, snoc]
 
+theorem subst_map {χ'} (f : χ → χ') (σ : Nat → Expr χ) (e : Expr χ) :
+    (subst σ e).map f = subst (map f ∘ σ) (e.map f) := by
+  induction e generalizing σ <;> simp [subst, map, up_map_comp] at * <;> grind
+
 /-- Turn a renaming into a substitution. -/
 def ofRen (χ) (ξ : Nat → Nat) : Nat → Expr χ :=
   fun i => Expr.bvar (ξ i)
@@ -204,6 +221,9 @@ theorem snoc_comp_wk_succ (σ : Nat → Expr χ) (n) :
     snoc (comp wk σ) (bvar (n + 1)) = comp wk (snoc σ (bvar n)) := by
   ext ⟨⟩ <;> dsimp [comp, snoc, wk, -ofRen_succ, subst, ofRen]
 
+@[simp]
+theorem map_comp_wk {χ'} (f : χ → χ') : map f ∘ wk = wk := rfl
+
 /-- A substitution that instantiates one binder.
 ```
 Γ ⊢ t : A
@@ -213,6 +233,12 @@ theorem snoc_comp_wk_succ (σ : Nat → Expr χ) (n) :
 def toSb (t : Expr χ) : Nat → Expr χ :=
   snoc Expr.bvar t
 
+@[simp]
+theorem map_comp_bvar {χ'} (f : χ → χ') : map f ∘ bvar = bvar := rfl
+
+theorem map_toSb {χ'} (f : χ → χ') (e : Expr χ) : (e.map f).toSb = map f ∘ e.toSb := by
+  simp [toSb, ← snoc_map_comp]
+
 /-! ## Decision procedure -/
 
 theorem snoc_comp_wk_zero_subst (σ : Nat → Expr χ) :
@@ -303,6 +329,14 @@ def isClosed (k : Nat := 0) : Expr χ → Bool
   | .idRec _ _ t M r u h =>
     t.isClosed k && M.isClosed (k + 2) && r.isClosed k && u.isClosed k && h.isClosed k
 
+theorem isClosed_of_isClosed_of_le {k k'} {e : Expr χ} (le : k ≤ k') :
+    e.isClosed k → e.isClosed k' := by
+  induction e generalizing k k' <;> grind [isClosed]
+
+@[simp]
+theorem map_isClosed {χ'} (f : χ → χ') (e : Expr χ) (k) : (e.map f).isClosed k = e.isClosed k := by
+  induction e generalizing k <;> simp_all [isClosed, map]
+
 /-- The substitution acts via identity on indices strictly below `n`. -/
 def SbIsBvar (σ : Nat → Expr χ) (n : Nat) :=
   ∀ ⦃i⦄, i < n → σ i = .bvar i
diff --git a/HoTTLean/Syntax/Axioms.lean b/HoTTLean/Syntax/Axioms.lean
index a7056c45..5b4845b4 100644
--- a/HoTTLean/Syntax/Axioms.lean
+++ b/HoTTLean/Syntax/Axioms.lean
@@ -2,19 +2,7 @@ import HoTTLean.Syntax.Synth
 
 namespace SynthLean
 
-variable {χ : Type*} {E : Axioms χ}
-
-theorem isClosed_all :
-    (∀ {Γ l A}, E ∣ Γ ⊢[l] A → A.isClosed Γ.length) ∧
-    (∀ {Γ l A t}, E ∣ Γ ⊢[l] t : A → t.isClosed Γ.length) := by
-  mutual_induction WfTp
-  case bvar =>
-    intros; rename_i lk _
-    simp [Expr.isClosed, lk.lt_length]
-  all_goals grind [Expr.isClosed]
-
-theorem WfTp.isClosed {l A} : E ∣ [] ⊢[l] A → A.isClosed := isClosed_all.1
-theorem WfTm.isClosed {l A t} : E ∣ [] ⊢[l] t : A → t.isClosed := isClosed_all.2
+variable {χ : Type*}
 
 /-! ## Axiom environments -/
 
@@ -24,12 +12,28 @@ def empty (χ) : Axioms χ := fun _ => none
 
 theorem empty_wf (χ) : (empty χ).Wf := nofun
 
-open Classical
+section
+variable [DecidableEq χ]
+
+/- Remark: we require `E c = none` and `E ∣ [] ⊢[l] A`
+so that `E.snoc` is automatically `Wf` if `E` is. -/
+def snoc (E : Axioms χ) {c : χ} {A : Expr χ} {l : Nat}
+    (_Ec : E c = none) (Awf : E ∣ [] ⊢[l] A) : Axioms χ :=
+  fun d => if d = c then some ⟨(A, l), ⟨Awf.isClosed, Awf.le_univMax⟩⟩ else E d
+
+@[simp]
+theorem snoc_get (E : Axioms χ) {c A l} (Ec : E c = none) (Awf) :
+    E.snoc Ec Awf c = some ⟨(A, l), ⟨Awf.isClosed, Awf.le_univMax⟩⟩ := by
+  simp [snoc]
+
+end
+
+/-! ## Theory inclusions -/
 
 instance : LE (Axioms χ) where
   le E E' := ∀ ⦃c p⦄, (E c) = some p → (E' c) = some p
 
-instance : IsRefl (Axioms χ) (· ≤ ·) where
+instance : @Std.Refl (Axioms χ) (· ≤ ·) where
   refl _ _ _ := id
 
 instance : IsTrans (Axioms χ) (· ≤ ·) where
@@ -37,77 +41,126 @@ instance : IsTrans (Axioms χ) (· ≤ ·) where
 
 theorem empty_le (E : Axioms χ) : empty χ ≤ E := nofun
 
-noncomputable def snoc (E : Axioms χ)
-    (l : Nat) (c : χ) (A : Expr χ)
-    (l_le : l ≤ univMax) (A_cl : A.isClosed) : Axioms χ :=
-  fun d => if d = c then some ⟨(A, l), ⟨A_cl, l_le⟩⟩ else E d
+theorem eq_none_of_le {E E' : Axioms χ} (le : E ≤ E') {c} (E'c : E' c = none) : E c = none := by
+  apply Option.eq_none_iff_forall_ne_some.mpr
+  intro _ h
+  simp [le h] at E'c
+
+section
+variable [DecidableEq χ] {𝕋 𝕋' : Axioms χ} (le : 𝕋 ≤ 𝕋')
+  {c : χ} {A : Expr χ} {l : Nat}
+  (𝕋c : 𝕋 c = none) (𝕋'c : 𝕋' c = none)
+  (Awf : 𝕋 ∣ [] ⊢[l] A) (Awf' : 𝕋' ∣ [] ⊢[l] A)
+
+include le in
+theorem le_snoc : 𝕋 ≤ 𝕋'.snoc 𝕋'c Awf' := by
+  intro d Al 𝕋d
+  have : d ≠ c := fun h => nomatch (h ▸ le 𝕋d) ▸ 𝕋'c
+  simpa [snoc, this, ↓reduceIte] using le 𝕋d
+
+include le in
+theorem snoc_le (𝕋'c : 𝕋' c = some ⟨(A, l), ⟨Awf.isClosed, Awf.le_univMax⟩⟩) :
+    𝕋.snoc 𝕋c Awf ≤ 𝕋' := by
+  intro d Al 𝕋d
+  by_cases eq : d = c
+  . cases eq; convert 𝕋'c using 2; simpa [snoc] using 𝕋d.symm
+  . simp only [snoc, eq, ↓reduceIte] at 𝕋d; exact le 𝕋d
 
-@[simp]
-theorem snoc_get (E : Axioms χ) (l c A l_le A_cl) :
-    E.snoc l c A l_le A_cl c = some ⟨(A, l), ⟨A_cl, l_le⟩⟩ := by
-  simp [snoc]
+variable (𝕋) in
+theorem le_snoc_self : 𝕋 ≤ 𝕋.snoc 𝕋c Awf :=
+  le_snoc (refl _) 𝕋c Awf
 
-theorem le_snoc {E E' : Axioms χ} (le : E ≤ E') (l c A l_le A_cl) (Ec : E c = none) :
-    E ≤ E'.snoc l c A l_le A_cl := by
-  intro d Al Ed
-  have : d ≠ c := by grind
-  simpa [snoc, this, ↓reduceIte] using le Ed
+include le in
+theorem snoc_le_snoc : 𝕋.snoc 𝕋c Awf ≤ 𝕋'.snoc 𝕋'c Awf' := by
+  simp [snoc_le (le_snoc le ..)]
 
-theorem le_snoc_self (E : Axioms χ) (l c A l_le A_cl) (Ec : E c = none) :
-    E ≤ E.snoc l c A l_le A_cl :=
-  le_snoc (refl _) l c A l_le A_cl Ec
+end
+end Axioms
 
-theorem snoc_le {E E' : Axioms χ} (le : E ≤ E') (l c A l_le A_cl)
-    (E'c : E' c = some ⟨(A, l), ⟨A_cl, l_le⟩⟩) :
-    E.snoc l c A l_le A_cl ≤ E' := by
-  intro d Al Ed
-  by_cases eq : d = c
-  . cases eq; convert E'c using 2; simpa [snoc] using Ed.symm
-  . simp only [snoc, eq, ↓reduceIte] at Ed; exact le Ed
-
-theorem of_le_all {E E' : Axioms χ} (le : E ≤ E') :
-    (∀ {Γ}, WfCtx E Γ → WfCtx E' Γ) ∧
-    (∀ {Γ l A}, E ∣ Γ ⊢[l] A → E' ∣ Γ ⊢[l] A) ∧
-    (∀ {Γ l A B}, E ∣ Γ ⊢[l] A ≡ B → E' ∣ Γ ⊢[l] A ≡ B) ∧
-    (∀ {Γ l A t}, E ∣ Γ ⊢[l] t : A → E' ∣ Γ ⊢[l] t : A) ∧
-    (∀ {Γ l A t u}, E ∣ Γ ⊢[l] t ≡ u : A → E' ∣ Γ ⊢[l] t ≡ u : A) := by
+/-! ## Theory maps (translations) -/
+
+variable {χ χ' : Type*} {𝕋 : Axioms χ} {f : χ → χ'} {𝕋' : Axioms χ'}
+
+/-- A map `f` of signatures is well-formed as a map of theories
+when it preserves the types of those base constants
+that are present in the domain. -/
+structure WfTheoryMap (𝕋 : Axioms χ) (f : χ → χ') (𝕋' : Axioms χ') : Prop where
+  get_eq (c : χ) (h : (𝕋 c).isSome) :
+    𝕋' (f c) = (𝕋 c).map fun ⟨(A, l), h⟩ => ⟨(A.map f, l), by simp [h]⟩
+
+theorem WfTheoryMap.of_le {𝕋 𝕋' : Axioms χ} (le : 𝕋 ≤ 𝕋') : WfTheoryMap 𝕋 id 𝕋' :=
+  ⟨by
+    intro _ 𝕋c
+    simp [le <| Option.eq_some_of_isSome 𝕋c]⟩
+
+section
+variable (H : WfTheoryMap 𝕋 f 𝕋') {Γ l A B t u}
+include H
+
+private theorem map_all :
+    (∀ {Γ}, WfCtx 𝕋 Γ → WfCtx 𝕋' (Γ.map f)) ∧
+    (∀ {Γ l A}, 𝕋 ∣ Γ ⊢[l] A → 𝕋' ∣ Γ.map f ⊢[l] A.map f) ∧
+    (∀ {Γ l A B}, 𝕋 ∣ Γ ⊢[l] A ≡ B → 𝕋' ∣ Γ.map f ⊢[l] A.map f ≡ B.map f) ∧
+    (∀ {Γ l A t}, 𝕋 ∣ Γ ⊢[l] t : A → 𝕋' ∣ Γ.map f ⊢[l] t.map f : A.map f) ∧
+    (∀ {Γ l A t u}, 𝕋 ∣ Γ ⊢[l] t ≡ u : A → 𝕋' ∣ Γ.map f ⊢[l] t.map f ≡ u.map f : A.map f) := by
   mutual_induction WfCtx
   case ax =>
-    intros; rename_i Ec _ Γ ihA
-    apply WfTm.ax Γ (le Ec) ihA
+    intro _ _ Al _ 𝕋c _ _
+    apply WfTm.ax (Al := ⟨(Al.1.1.map f, Al.1.2), by simp [Al.2]⟩)
+    . assumption
+    . apply 𝕋c ▸ H.get_eq _ (Option.isSome_iff_exists.mpr ⟨_, 𝕋c⟩)
+  case bvar =>
+    introv _ lk _
+    apply WfTm.bvar ‹_› (lk.map f)
+
+  all_goals (
+    dsimp [Expr.map]; intros
+    try simp only [Expr.subst_map, ← Expr.up_map_comp, ← Expr.snoc_map_comp, ← Expr.map_toSb] at *)
+  case lam_app' => apply EqTm.lam_app; assumption
+  case idRec_refl' => apply EqTm.idRec_refl <;> assumption
+  case cong_idRec' => apply EqTm.cong_idRec <;> assumption
+  case cong_snd' => apply EqTm.cong_snd <;> assumption
+  case idRec' => apply WfTm.idRec <;> assumption
+  case snd' => apply WfTm.snd; assumption
   grind_cases
 
-end Axioms
-
-theorem WfCtx.of_axioms_le {E E' : Axioms χ} {Γ} (le : E ≤ E') (Γwf : WfCtx E Γ) :
-    WfCtx E' Γ :=
-  Axioms.of_le_all le |>.1 Γwf
-
-theorem WfTp.of_axioms_le {E E' : Axioms χ} {Γ A l} (le : E ≤ E') (ΓA : E ∣ Γ ⊢[l] A) :
-    E' ∣ Γ ⊢[l] A :=
-  Axioms.of_le_all le |>.2.1 ΓA
-
-theorem EqTp.of_axioms_le {E E' : Axioms χ} {Γ A B l} (le : E ≤ E') (ΓAB : E ∣ Γ ⊢[l] A ≡ B) :
-    E' ∣ Γ ⊢[l] A ≡ B :=
-  Axioms.of_le_all le |>.2.2.1 ΓAB
-
-theorem WfTm.of_axioms_le {E E' : Axioms χ} {Γ A t l} (le : E ≤ E') (Γt : E ∣ Γ ⊢[l] t : A) :
-    E' ∣ Γ ⊢[l] t : A :=
-  Axioms.of_le_all le |>.2.2.2.1 Γt
-
-theorem EqTm.of_axioms_le {E E' : Axioms χ} {Γ A t u l} (le : E ≤ E') (Γtu : E ∣ Γ ⊢[l] t ≡ u : A) :
-    E' ∣ Γ ⊢[l] t ≡ u : A :=
-  Axioms.of_le_all le |>.2.2.2.2 Γtu
-
-theorem Axioms.Wf.snoc {E : Axioms χ} {A l}
-    (Ewf : E.Wf) (c : χ) (Awf : E ∣ [] ⊢[l] A) (Ec : E c = none) :
-    (E.snoc l c A Awf.le_univMax Awf.isClosed).Wf := by
-  intro d Al Ed
-  simp only [Axioms.snoc] at Ed
-  have le := E.le_snoc_self l c A Awf.le_univMax Awf.isClosed Ec
-  by_cases eq : d = c <;> simp only [eq, ↓reduceIte] at Ed
-  . cases Ed
+theorem WfCtx.map (W : WfCtx 𝕋 Γ) : WfCtx 𝕋' (Γ.map f) := (map_all H).1 W
+theorem WfTp.map (W : 𝕋 ∣ Γ ⊢[l] A) : 𝕋' ∣ Γ.map f ⊢[l] A.map f := (map_all H).2.1 W
+theorem EqTp.map (W : 𝕋 ∣ Γ ⊢[l] A ≡ B) : 𝕋' ∣ Γ.map f ⊢[l] A.map f ≡ B.map f :=
+  (map_all H).2.2.1 W
+theorem WfTm.map (W : 𝕋 ∣ Γ ⊢[l] t : A) : 𝕋' ∣ Γ.map f ⊢[l] t.map f : A.map f :=
+  (map_all H).2.2.2.1 W
+theorem EqTm.map (W : 𝕋 ∣ Γ ⊢[l] t ≡ u : A) : 𝕋' ∣ Γ.map f ⊢[l] t.map f ≡ u.map f : A.map f :=
+  (map_all H).2.2.2.2 W
+
+end
+
+section
+variable {𝕋 𝕋' : Axioms χ} (le : 𝕋 ≤ 𝕋') {Γ l A B t u}
+include le
+
+theorem WfCtx.of_axioms_le (Γwf : WfCtx 𝕋 Γ) : WfCtx 𝕋' Γ := by
+  simpa using Γwf.map (WfTheoryMap.of_le le)
+theorem WfTp.of_axioms_le (ΓA : 𝕋 ∣ Γ ⊢[l] A) : 𝕋' ∣ Γ ⊢[l] A := by
+  simpa using ΓA.map (WfTheoryMap.of_le le)
+theorem EqTp.of_axioms_le (ΓAB : 𝕋 ∣ Γ ⊢[l] A ≡ B) : 𝕋' ∣ Γ ⊢[l] A ≡ B := by
+  simpa using ΓAB.map (WfTheoryMap.of_le le)
+theorem WfTm.of_axioms_le (Γt : 𝕋 ∣ Γ ⊢[l] t : A) : 𝕋' ∣ Γ ⊢[l] t : A := by
+  simpa using Γt.map (WfTheoryMap.of_le le)
+theorem EqTm.of_axioms_le (Γtu : 𝕋 ∣ Γ ⊢[l] t ≡ u : A) : 𝕋' ∣ Γ ⊢[l] t ≡ u : A := by
+  simpa using Γtu.map (WfTheoryMap.of_le le)
+
+end
+
+theorem Axioms.Wf.snoc [DecidableEq χ] {𝕋 : Axioms χ} {c A l}
+    (𝕋wf : 𝕋.Wf) (𝕋c : 𝕋 c = none) (Awf : 𝕋 ∣ [] ⊢[l] A) :
+    (𝕋.snoc 𝕋c Awf).Wf := by
+  intro d Al 𝕋d
+  simp only [Axioms.snoc] at 𝕋d
+  have le := 𝕋.le_snoc_self 𝕋c Awf
+  by_cases eq : d = c <;> simp only [eq, ↓reduceIte] at 𝕋d
+  . cases 𝕋d
     exact Awf.of_axioms_le le
-  . exact (Ewf Ed).of_axioms_le le
+  . exact (𝕋wf 𝕋d).of_axioms_le le
 
 end SynthLean
diff --git a/HoTTLean/Syntax/Basic.lean b/HoTTLean/Syntax/Basic.lean
index d05dfe5a..72d8e86e 100644
--- a/HoTTLean/Syntax/Basic.lean
+++ b/HoTTLean/Syntax/Basic.lean
@@ -1,10 +1,9 @@
 import Lean.Meta.Tactic.Simp
-
-universe u
+import Mathlib.Tactic.TypeStar
 
 namespace SynthLean
 
-variable (χ : Type u) in
+variable (χ : Type*) in
 /-- A HoTT0 expression with axioms indexed by `χ`. -/
 inductive Expr where
   /-- An axiom (i.e., a closed term constant in the theory) of the given type. -/
@@ -40,10 +39,42 @@ inductive Expr where
   | code (A : Expr)
   deriving Inhabited, Repr, Lean.ToExpr
 
+namespace Expr
+
+variable {χ χ' : Type*} (f : χ → χ')
+
 @[simp]
-theorem Expr.sizeOf_pos {χ} (e : Expr χ) : 0 < sizeOf e := by
+theorem sizeOf_pos (e : Expr χ) : 0 < sizeOf e := by
   induction e <;> { dsimp; omega }
 
+-- `Expr.map` can be autogenerated using `derive Functor`,
+-- but the result is not sufficiently universe-polymorphic.
+-- See https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/inferred.20Type.20universe.20in.20functors/near/217072636
+def map : Expr χ → Expr χ'
+  | ax c A => ax (f c) (map A)
+  | bvar i => bvar i
+  | pi l l' A B => pi l l' (map A) (map B)
+  | lam l l' A b => lam l l' (map A) (map b)
+  | app l l' B fn arg => app l l' (map B) (map fn) (map arg)
+  | sigma l l' A B => sigma l l' (map A) (map B)
+  | pair l l' B t u => pair l l' (map B) (map t) (map u)
+  | fst l l' A B p => fst l l' (map A) (map B) (map p)
+  | snd l l' A B p => snd l l' (map A) (map B) (map p)
+  | Id l A t u => Id l (map A) (map t) (map u)
+  | refl l t => refl l (map t)
+  | idRec l l' t M r u h => idRec l l' (map t) (map M) (map r) (map u) (map h)
+  | univ l => univ l
+  | el a => el (map a)
+  | code A => code (map A)
+
+@[simp] theorem map_id_fun : map (id : χ → χ) = id := by
+  funext e
+  induction e <;> simp_all [map]
+
+@[simp] theorem map_id_fun' : map (fun (c : χ) => c) = id := map_id_fun
+
+end Expr
+
 /-- A convergent rewriting system for the HoTT0 σ-calculus. -/
 -- The attribute has to be initialized here for use in downstream modules.
 register_simp_attr autosubst
diff --git a/HoTTLean/Syntax/Synth.lean b/HoTTLean/Syntax/Synth.lean
index b168d9eb..0eadeb01 100644
--- a/HoTTLean/Syntax/Synth.lean
+++ b/HoTTLean/Syntax/Synth.lean
@@ -3,33 +3,7 @@ import HoTTLean.Syntax.GCongr
 
 namespace SynthLean
 
-variable {χ : Type*} {E E' : Axioms χ} {Γ : Ctx χ}
-  {A A' t t' : Expr χ} {i l l' : Nat}
-
-/-! ## Lookup well-formedness -/
-
-namespace Lookup
-
-theorem lt_length : Lookup Γ i A l → i < Γ.length := by
-  intro lk; induction lk <;> (dsimp; omega)
-
-theorem lvl_eq (lk : Lookup Γ i A l) : l = (Γ[i]'lk.lt_length).2 := by
-  induction lk <;> grind
-
-theorem tp_uniq (lk : Lookup Γ i A l) (lk' : Lookup Γ i A' l) : A = A' := by
-  induction lk generalizing A' <;> grind [cases Lookup]
-
-theorem of_lt_length : i < Γ.length → ∃ A l, Lookup Γ i A l := by
-  intro lt
-  induction Γ generalizing i
-  · cases lt
-  · cases i
-    · exact ⟨_, _, Lookup.zero ..⟩
-    · rename_i ih _
-      have ⟨A, l, h⟩ := ih <| Nat.succ_lt_succ_iff.mp lt
-      exact ⟨A.subst Expr.wk, l, Lookup.succ _ h⟩
-
-end Lookup
+variable {χ : Type*} {E E' : Axioms χ} {Γ : Ctx χ} {A A' t : Expr χ} {l l' : Nat}
 
 /-! ## Level synthesis and uniqueness -/
 
@@ -40,7 +14,7 @@ Furthermore, the correctness proof `eq_synthLvl` needs zero metatheory.
 Does this imply we could omit level annotations from the syntax?
 In the interpretation function, we'd invoke `synthLvl.go` on `ExtSeq`.  -/
 noncomputable def synthLvl (Γ : Ctx χ) (e : Expr χ) : Nat :=
-  go (Γ.map (·.2)) e
+  go (List.map (·.2) Γ) e
 where
   go (Γ : List Nat) : Expr χ → Nat
   | .ax _ A => go Γ A
diff --git a/HoTTLean/Syntax/Typing.lean b/HoTTLean/Syntax/Typing.lean
index 2dc9ee83..3e6f1a37 100644
--- a/HoTTLean/Syntax/Typing.lean
+++ b/HoTTLean/Syntax/Typing.lean
@@ -1,4 +1,5 @@
 import HoTTLean.Syntax.Autosubst
+import HoTTLean.Tactic.MutualInduction
 
 /-! ## Typing rules
 
@@ -7,12 +8,6 @@ as `Prop`-valued relations. -/
 
 namespace SynthLean
 
-declare_syntax_cat judgment
-scoped syntax:50 term:51 : judgment
-scoped syntax:50 term:51 " ≡ " term:51 : judgment
-scoped syntax:50 term:51 " : " term:51 : judgment
-scoped syntax:50 term:51 " ≡ " term:51 " : " term:51 : judgment
-
 /-- The maximum `l` for which `Γ ⊢[l] 𝒥` makes sense.
 When set to `0`, types cannot be quantified over at all. -/
 -- TODO: this should be a parameter,
@@ -32,11 +27,33 @@ This does mean we cannot have type constants at level `univMax`.
 
 We do *not* use `Axioms` for definitions;
 the native Lean `Environment` is used instead. -/
+-- TODO: "theory", not "axiom environment"
 abbrev Axioms (χ : Type*) := χ → Option { Al : Expr χ × Nat // Al.1.isClosed ∧ Al.2 ≤ univMax }
 
 /-- A typing context consisting of type expressions and their universe levels. -/
 abbrev Ctx (χ : Type*) := List (Expr χ × Nat)
 
+namespace Ctx
+
+variable {χ χ' : Type*} (f : χ → χ')
+
+def map (Γ : Ctx χ) : Ctx χ' :=
+  List.map (fun (A, l) => (A.map f, l)) Γ
+
+@[simp] theorem length_map (Γ : Ctx χ) : (Γ.map f).length = Γ.length := by
+  simp [Ctx.map]
+
+@[simp] theorem map_id_fun : map (fun (c : χ) => c) = id := by
+  funext; simp [map]
+
+@[simp] theorem map_id_fun' : map (id : χ → χ) = id := map_id_fun
+
+@[simp] theorem map_nil : map f [] = [] := rfl
+
+@[simp] theorem map_cons {A l Γ} : map f ((A, l) :: Γ) = (A.map f, l) :: map f Γ := rfl
+
+end Ctx
+
 variable {χ : Type*} (E : Axioms χ)
 
 /-- `Lookup Γ i A l` means that `A = A'[↑ⁱ⁺¹]` where `Γ[i] = (A', l)`.
@@ -45,6 +62,18 @@ inductive Lookup : Ctx χ → Nat → Expr χ → Nat → Prop where
   | zero (Γ A l) : Lookup ((A,l) :: Γ) 0 (A.subst Expr.wk) l
   | succ {Γ A i l} (Bk) : Lookup Γ i A l → Lookup (Bk :: Γ) (i+1) (A.subst Expr.wk) l
 
+theorem Lookup.map {χ'} (f : χ → χ') {Γ i A l} (H : Lookup Γ i A l) :
+    Lookup (Γ.map f) i (A.map f) l := by
+  induction H
+  case zero => simp only [Expr.subst_map]; apply Lookup.zero
+  case succ ih => simp only [Expr.subst_map]; apply Lookup.succ _ ih
+
+declare_syntax_cat judgment
+scoped syntax:50 term:51 : judgment
+scoped syntax:50 term:51 " ≡ " term:51 : judgment
+scoped syntax:50 term:51 " : " term:51 : judgment
+scoped syntax:50 term:51 " ≡ " term:51 " : " term:51 : judgment
+
 /-- Judgment syntax not parameterized by an environment.
 Used locally to define typing rules without repeating `E ∣ Γ`. -/
 local syntax:25 term:51 " ⊢[" term:51 "] " judgment:50 : term
@@ -405,4 +434,46 @@ this forces `Axioms` to be finitely supported. -/
 abbrev Axioms.Wf (E : Axioms χ) :=
   ∀ ⦃c p⦄, E c = some p → E ∣ [] ⊢[p.val.2] p.val.1
 
+/-! ## Lookup well-formedness -/
+
+namespace Lookup
+variable {Γ : Ctx χ} {A A' : Expr χ} {l i : Nat}
+
+theorem lt_length : Lookup Γ i A l → i < Γ.length := by
+  intro lk; induction lk <;> (dsimp; omega)
+
+theorem lvl_eq (lk : Lookup Γ i A l) : l = (Γ[i]'lk.lt_length).2 := by
+  induction lk <;> grind
+
+theorem tp_uniq (lk : Lookup Γ i A l) (lk' : Lookup Γ i A' l) : A = A' := by
+  induction lk generalizing A' <;> grind [cases Lookup]
+
+theorem of_lt_length : i < Γ.length → ∃ A l, Lookup Γ i A l := by
+  intro lt
+  induction Γ generalizing i
+  · cases lt
+  · cases i
+    · exact ⟨_, _, Lookup.zero ..⟩
+    · rename_i ih _
+      have ⟨A, l, h⟩ := ih <| Nat.succ_lt_succ_iff.mp lt
+      exact ⟨A.subst Expr.wk, l, Lookup.succ _ h⟩
+
+end Lookup
+
+/-! ## Closed expressions -/
+
+variable {E : Axioms χ}
+
+private theorem isClosed_all :
+    (∀ {Γ l A}, E ∣ Γ ⊢[l] A → A.isClosed Γ.length) ∧
+    (∀ {Γ l A t}, E ∣ Γ ⊢[l] t : A → t.isClosed Γ.length) := by
+  mutual_induction WfTp
+  case bvar =>
+    intros; rename_i lk _
+    simp [Expr.isClosed, lk.lt_length]
+  all_goals grind [Expr.isClosed]
+
+theorem WfTp.isClosed {l A} : E ∣ [] ⊢[l] A → A.isClosed := isClosed_all.1
+theorem WfTm.isClosed {l A t} : E ∣ [] ⊢[l] t : A → t.isClosed := isClosed_all.2
+
 end SynthLean
diff --git a/HoTTLean/Typechecker/Equate.lean b/HoTTLean/Typechecker/Equate.lean
index 6b38e88f..a8894676 100644
--- a/HoTTLean/Typechecker/Equate.lean
+++ b/HoTTLean/Typechecker/Equate.lean
@@ -3,12 +3,27 @@ import HoTTLean.Typechecker.Evaluate
 namespace SynthLean
 open Qq
 
+namespace TraceCls
+def equate := `SynthLean.Typechecker.Equate
+def equateTp := equate ++ `tp
+def equateTm := equate ++ `tm
+def equateNeut := equate ++ `neut
+
+initialize
+  Lean.registerTraceClass equate
+  Lean.registerTraceClass equateTp (inherited := true)
+  Lean.registerTraceClass equateTm (inherited := true)
+  Lean.registerTraceClass equateNeut (inherited := true)
+end TraceCls
+
 variable {_u : Lean.Level} {χ : Q(Type _u)}
 
 mutual
 partial def equateTp (d : Q(Nat)) (l : Q(Nat)) (vT' vU' : Q(Val $χ)) :
     TypecheckerM Q(∀ {E Γ T U}, $d = Γ.length →
       ValEqTp E Γ $l $vT' T → ValEqTp E Γ $l $vU' U → E ∣ Γ ⊢[$l] T ≡ U) := do
+  Lean.withTraceNode TraceCls.equateTp (fun e =>
+    return m!"{Lean.exceptEmoji e} [{d}] ⊢[{l}] {vT'} ≡?≡ {vU'}") do
   let key := (⟨d⟩, ⟨l⟩, ⟨vT'⟩, ⟨vU'⟩)
   if let some pf := (← get).equateTp[key]? then return pf
   eventually (fun pf =>
@@ -103,6 +118,8 @@ partial def equateTm (d : Q(Nat)) (l : Q(Nat)) (vT vt vu : Q(Val $χ)) :
     TypecheckerM Q(∀ {E Γ T t u}, $d = Γ.length →
       ValEqTp E Γ $l $vT T → ValEqTm E Γ $l $vt t T → ValEqTm E Γ $l $vu u T →
       E ∣ Γ ⊢[$l] t ≡ u : T) := do
+  Lean.withTraceNode TraceCls.equateTm (fun e =>
+    return m!"{Lean.exceptEmoji e} [{d}] ⊢[{l}] {vt} ≡?≡ {vu} : {vT}") do
   let key := (⟨d⟩, ⟨l⟩, ⟨vT⟩, ⟨vt⟩, ⟨vu⟩)
   if let some pf := (← get).equateTm[key]? then return pf
   eventually (fun pf =>
@@ -219,6 +236,8 @@ partial def equateNeutTm (d : Q(Nat)) (nt nu : Q(Neut $χ)) :
     TypecheckerM Q(∀ {E Γ T U t u l}, $d = Γ.length →
       NeutEqTm E Γ l $nt t T → NeutEqTm E Γ l $nu u U →
       (E ∣ Γ ⊢[l] T ≡ U) ∧ (E ∣ Γ ⊢[l] t ≡ u : T)) := do
+  Lean.withTraceNode TraceCls.equateNeut (fun e =>
+    return m!"{Lean.exceptEmoji e} [{d}] ⊢ {nt} ≡?≡ {nu}") do
   let key := (⟨d⟩, ⟨nt⟩, ⟨nu⟩)
   if let some pf := (← get).equateNeutTm[key]? then return pf
   eventually (fun pf =>
diff --git a/HoTTLean/Typechecker/Synth.lean b/HoTTLean/Typechecker/Synth.lean
index bbfc8ed7..04d05925 100644
--- a/HoTTLean/Typechecker/Synth.lean
+++ b/HoTTLean/Typechecker/Synth.lean
@@ -1,5 +1,6 @@
 import HoTTLean.Typechecker.Equate
-import HoTTLean.Frontend.Checked
+import HoTTLean.Frontend.Reflected
+import HoTTLean.Frontend.Instances
 
 /-! ## Typechecker
 
@@ -9,14 +10,17 @@ For now it is specialized to axioms named by `Lean.Name`. -/
 
 namespace SynthLean
 open Qq
+open CategoryTheory
+open Model UnstructuredUniverse
 
 def traceClsTypechecker : Lean.Name := `SynthLean.Typechecker
 
 initialize
   Lean.registerTraceClass traceClsTypechecker
 
-partial def lookupVar (vΓ : Q(TpEnv Lean.Name)) (i : Q(Nat)) :
-    Lean.MetaM ((vA : Q(Val Lean.Name)) × (l : Q(Nat)) ×
+/-- Look a De Bruijn index up in a type environment. -/
+partial def lookupVar {u : Lean.Level} {χ : Q(Type u)} (vΓ : Q(TpEnv $χ)) (i : Q(Nat)) :
+    Lean.MetaM ((vA : Q(Val $χ)) × (l : Q(Nat)) ×
       Q(∀ {E Γ}, TpEnvEqCtx E $vΓ Γ → ∃ A,
         ValEqTp E Γ $l $vA A ∧ Lookup Γ $i A $l)) :=
   match i, vΓ with
@@ -38,19 +42,20 @@ partial def lookupVar (vΓ : Q(TpEnv Lean.Name)) (i : Q(Nat)) :
       exact ⟨_, vA.wk vB.wf_tp, lk.succ ..⟩
     )⟩
 
-partial def lookupAxiom (E : Q(Axioms Lean.Name)) (c : Q(Lean.Name)) : Lean.MetaM
-    ((A : Q(Expr Lean.Name)) × (l : Q(Nat)) × Q(∃ h, $E $c = some ⟨($A, $l), h⟩) ⊕
-      Q($E $c = none)) := do
+/-- Look up a named axiom in an axiom environment. -/
+partial def lookupAxiom (E : Q(Axioms Lean.Name)) (c : Q(Lean.Name)) :
+    Lean.MetaM ((A : Q(Expr Lean.Name)) × (l : Q(Nat)) ×
+      Q(∃ h, $E $c = some ⟨($A, $l), h⟩) ⊕ Q($E $c = none)) := do
   match E with
   | ~q(.empty _) => return .inr q(by rfl)
-  | ~q(Axioms.snoc $E' $l $c' $A $l_le $A_cl) =>
+  | ~q(@Axioms.snoc _ _ $E' $c' $A $l _ $Awf) =>
     let b : Q(Bool) ← Lean.Meta.whnf q(decide ($c' = $c))
     have : $b =Q decide ($c' = $c) := .unsafeIntro
     match b with
     | ~q(true) =>
       return Sum.inl ⟨q($A), q($l), q(by as_aux_lemma =>
         have : $c' = $c := by rwa [decide_eq_true_iff] at *
-        simp +zetaDelta [this, ($A_cl), ($l_le)]
+        simp +zetaDelta [this, ($Awf).isClosed, ($Awf).le_univMax]
       )⟩
     | ~q(false) =>
       match ← lookupAxiom q($E') q($c) with
@@ -59,51 +64,27 @@ partial def lookupAxiom (E : Q(Axioms Lean.Name)) (c : Q(Lean.Name)) : Lean.Meta
           have : $c' ≠ $c := by rwa [decide_eq_false_iff_not] at *
           have ⟨h, eq⟩ := $h
           refine ⟨h, ?_⟩
-          simpa +zetaDelta [CheckedAx.snocAxioms, Axioms.snoc, this.symm] using eq
+          simpa +zetaDelta [ReflectedAx.snocAxioms, Axioms.snoc, this.symm] using eq
         )⟩
       | .inr h =>
         return .inr q(by as_aux_lemma =>
           have : $c' ≠ $c := by rwa [decide_eq_false_iff_not] at *
-          simpa +zetaDelta [CheckedAx.snocAxioms, Axioms.snoc, this.symm] using $h
+          simpa +zetaDelta [ReflectedAx.snocAxioms, Axioms.snoc, this.symm] using $h
         )
     | _ =>
       throwError "could not determine whether\
           {Lean.indentExpr q($c') |>.nest 2}\
         {Lean.indentD "="}\
           {Lean.indentExpr c |>.nest 2}"
-  | ~q(CheckedAx.snocAxioms _) =>
+  | ~q(ReflectedAx.snocAxioms _) =>
     let E ← Lean.Meta.unfoldDefinition E
     lookupAxiom E c
   | _ => throwError "unsupported axiom environment{Lean.indentExpr E}"
 
-partial def checkAxiomsLe (E E' : Q(Axioms Lean.Name)) : Lean.MetaM Q($E ≤ $E') := do
-  match E with
-  | ~q(.empty _) => return q(($E').empty_le)
-  | ~q(Axioms.snoc $E₀ $l' $c' $A' $l_le $A_cl) =>
-    let le ← checkAxiomsLe q($E₀) q($E')
-    let .inl ⟨A, l, En⟩ ← lookupAxiom q($E') q($c')
-      | throwError "could not prove that '{c'}' is contained in{Lean.indentExpr E'}"
-    let ⟨_⟩ ← assertDefEqQ q($A) q($A')
-    let ⟨_⟩ ← assertDefEqQ q($l) q($l')
-    return q(by as_aux_lemma =>
-      dsimp +zetaDelta only [CheckedAx.snocAxioms]
-      have ⟨_, h⟩ := $En
-      apply Axioms.snoc_le $le _ _ _ _ _ h
-    )
-  | ~q(CheckedAx.snocAxioms _) =>
-    let E ← Lean.Meta.unfoldDefinition E
-    checkAxiomsLe E E'
-  | _ =>
-    throwError "could not prove\
-        {Lean.indentExpr E |>.nest 2}\
-      {Lean.indentD "≤"}\
-        {Lean.indentExpr E' |>.nest 2}"
-
 mutual
-variable (E : Q(Axioms Lean.Name)) (Ewf : Q(($E).Wf))
-
-partial def checkTp (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (T : Q(Expr Lean.Name)) :
-    TypecheckerM Q(∀ {Γ}, TpEnvEqCtx $E $vΓ Γ → $E ∣ Γ ⊢[$l] ($T)) :=
+partial def checkTp {u : Lean.Level} {χ : Q(Type u)} (𝕋 : Q(Axioms $χ))
+    (vΓ : Q(TpEnv $χ)) (l : Q(Nat)) (T : Q(Expr $χ)) :
+    TypecheckerM Q(∀ {Γ}, ($𝕋).Wf → TpEnvEqCtx $𝕋 $vΓ Γ → $𝕋 ∣ Γ ⊢[$l] ($T)) :=
   Lean.withTraceNode traceClsTypechecker (fun e =>
     return m!"{Lean.exceptEmoji e} {vΓ} ⊢[{l}] {T}") do
   let key := (⟨vΓ⟩, ⟨l⟩, ⟨T⟩)
@@ -113,58 +94,58 @@ partial def checkTp (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (T : Q(Expr Lean.Nam
   match T with
   | ~q(.pi $k $k' $A $B) => do
     let leq ← equateNat q($l) q(max $k $k')
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     let ⟨vA, vAeq⟩ ← evalTpId q($vΓ) q($A)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
+    let Bwf ← checkTp q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($B)
     return q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      apply WfTp.pi <| $Bwf <| vΓ.snoc <| $vAeq vΓ <| $Awf vΓ
+      apply WfTp.pi <| $Bwf 𝕋 <| vΓ.snoc <| $vAeq vΓ <| $Awf 𝕋 vΓ
     )
   | ~q(.sigma $k $k' $A $B) => do
     let leq ← equateNat q($l) q(max $k $k')
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     let ⟨vA, vAeq⟩ ← evalTpId q($vΓ) q($A)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
+    let Bwf ← checkTp q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($B)
     return q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      apply WfTp.sigma <| $Bwf <| vΓ.snoc <| $vAeq vΓ <| $Awf vΓ
+      apply WfTp.sigma <| $Bwf 𝕋 <| vΓ.snoc <| $vAeq vΓ <| $Awf 𝕋 vΓ
     )
   | ~q(.Id $k $A $a $b) => do
     let leq ← equateNat q($l) q($k)
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     let ⟨vA, vAeq⟩ ← evalTpId q($vΓ) q($A)
-    let awf ← checkTm q($vΓ) q($k) q($vA) q($a)
-    let bwf ← checkTm q($vΓ) q($k) q($vA) q($b)
+    let awf ← checkTm q($𝕋) q($vΓ) q($k) q($vA) q($a)
+    let bwf ← checkTm q($𝕋) q($vΓ) q($k) q($vA) q($b)
     return q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have := $vAeq vΓ ($Awf vΓ)
-      apply WfTp.Id ($awf vΓ this) ($bwf vΓ this)
+      have := $vAeq vΓ ($Awf 𝕋 vΓ)
+      apply WfTp.Id ($awf 𝕋 vΓ this) ($bwf 𝕋 vΓ this)
     )
   | ~q(.univ $n) => do
     let ln ← equateNat q($l) q($n + 1)
     let nmax ← ltNat q($n) q(univMax)
     return q(by as_aux_lemma =>
-      introv vΓ
+      introv _ vΓ
       subst_vars
       apply WfTp.univ vΓ.wf_ctx $nmax
     )
   | ~q(.el $a) => do
     let lmax ← ltNat q($l) q(univMax)
-    let awf ← checkTm q($vΓ) q($l + 1) q(.univ $l) q($a)
+    let awf ← checkTm q($𝕋) q($vΓ) q($l + 1) q(.univ $l) q($a)
     return q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       simp +zetaDelta only
-      apply WfTp.el <| $awf vΓ (ValEqTp.univ vΓ.wf_ctx $lmax)
+      apply WfTp.el <| $awf 𝕋 vΓ (ValEqTp.univ vΓ.wf_ctx $lmax)
     )
   | T => throwError "expected a type, got{Lean.indentExpr T}"
 
-partial def checkTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat))
-    (vT : Q(Val Lean.Name)) (t : Q(Expr Lean.Name)) :
-    TypecheckerM Q(∀ {Γ T}, TpEnvEqCtx $E $vΓ Γ → ValEqTp $E Γ $l $vT T →
-      $E ∣ Γ ⊢[$l] ($t) : T) := do
+partial def checkTm {u : Lean.Level} {χ : Q(Type u)} (𝕋 : Q(Axioms $χ))
+    (vΓ : Q(TpEnv $χ)) (l : Q(Nat)) (vT : Q(Val $χ)) (t : Q(Expr $χ)) :
+    TypecheckerM Q(∀ {Γ T}, ($𝕋).Wf → TpEnvEqCtx $𝕋 $vΓ Γ → ValEqTp $𝕋 Γ $l $vT T →
+      $𝕋 ∣ Γ ⊢[$l] ($t) : T) := do
   Lean.withTraceNode traceClsTypechecker (fun e =>
     return m!"{Lean.exceptEmoji e} {vΓ} ⊢[{l}] {t} ⇐ {vT}") do
   let key := (⟨vΓ⟩, ⟨l⟩, ⟨vT⟩, ⟨t⟩)
@@ -173,18 +154,19 @@ partial def checkTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat))
     modify fun st => { st with checkTm := st.checkTm.insert key pf }) do
   /- We could do something more bidirectional,
   but all terms synthesize (thanks to extensive annotations). -/
-  let ⟨vU, tU⟩ ← synthTm q($vΓ) q($l) q($t)
+  let ⟨vU, tU⟩ ← synthTm q($𝕋) q($vΓ) q($l) q($t)
   let eq ← equateTp q(($vΓ).length) q($l) q($vU) q($vT)
   return q(by as_aux_lemma =>
-    introv vΓ vT
-    have ⟨_, vU, t⟩ := $tU vΓ
+    introv 𝕋 vΓ vT
+    have ⟨_, vU, t⟩ := $tU 𝕋 vΓ
     apply t.conv <| $eq vΓ.length_eq vU vT
   )
 
--- TODO: infer rather than check universe level?
-partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Name)) :
-    TypecheckerM ((vT : Q(Val Lean.Name)) × Q(∀ {Γ}, TpEnvEqCtx $E $vΓ Γ →
-      ∃ T, ValEqTp $E Γ $l $vT T ∧ ($E ∣ Γ ⊢[$l] ($t) : T))) :=
+-- FIXME: infer rather than check universe level?
+partial def synthTm {u : Lean.Level} {χ : Q(Type u)} (𝕋 : Q(Axioms $χ))
+    (vΓ : Q(TpEnv $χ)) (l : Q(Nat)) (t : Q(Expr $χ)) :
+    TypecheckerM ((vT : Q(Val $χ)) × Q(∀ {Γ}, ($𝕋).Wf → TpEnvEqCtx $𝕋 $vΓ Γ →
+      ∃ T, ValEqTp $𝕋 Γ $l $vT T ∧ ($𝕋 ∣ Γ ⊢[$l] ($t) : T))) :=
   Lean.withTraceNode (ε := Lean.Exception) traceClsTypechecker (fun
     | .ok ⟨vT, _⟩ => return m!"✅️ {vΓ} ⊢[{l}] {t} ⇒ {vT}"
     | .error _ => return m!"❌️ {vΓ} ⊢[{l}] {t} ⇒ _") do
@@ -193,15 +175,34 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
   eventually (fun ⟨v, pf⟩ =>
     modify fun st => { st with synthTm := st.synthTm.insert key (v, pf) }) do
   match t with
-  | ~q(@CheckedDef.val _ $E' $defn) => do
-    -- Ensure the definition uses a subset of the available axioms.
-    let le ← checkAxiomsLe q($E') q($E)
+  | ~q(Expr.map (@HasTheoryMap.map _ _ $𝕋₀ $𝕋'' $_inst) $t') => do
+    let .defEq _ ← isDefEqQ q($𝕋) q($𝕋'')
+      | throwError "got translation into theory{Lean.indentExpr 𝕋''}\n\
+        while checking w.r.t. theory{Lean.indentExpr 𝕋}"
+    /- FIXME: This synthesis call is the only place we need `Fact 𝕋.Wf` instances.
+    Can it be avoided? -/
+    let 𝕋₀_wf ← synthInstanceQ q(Fact ($𝕋₀).Wf)
+    /- NOTE: We may only map closed expressions;
+    we can't map the typing environment backwards. -/
+    let ⟨vT, tT⟩ ← synthTm q($𝕋₀) q([]) q($l) q($t')
+    return ⟨q(($vT).map (HasTheoryMap.map $𝕋₀ $𝕋'')), q(by as_aux_lemma =>
+      introv 𝕋 vΓ; have Γwf := vΓ.wf_ctx; clear vΓ
+      have ⟨_, vT, t'⟩ := $tT ($𝕋₀_wf).out .nil
+      have := vT.map (HasTheoryMap.map_wf $𝕋₀ $𝕋'') |>.wk_many Γwf
+      refine ⟨_, this, ?_⟩
+      have := t'.map (HasTheoryMap.map_wf $𝕋₀ $𝕋'') |>.subst (WfSb.terminal .bvar Γwf)
+      simpa using this
+    )⟩
+  | ~q(@ReflectedDef.val _ $𝕋' $defn) => do
+    let .defEq _ ← isDefEqQ q($𝕋) q($𝕋')
+      | throwError "got definition in theory{Lean.indentExpr 𝕋'}\n\
+        while checking w.r.t. theory{Lean.indentExpr 𝕋}"
     let _ ← equateNat q($l) q(($defn).l)
     return ⟨q(($defn).nfTp), q(by as_aux_lemma =>
-      introv vΓ; have Γwf := vΓ.wf_ctx; clear vΓ
+      introv _ vΓ; have Γwf := vΓ.wf_ctx; clear vΓ
       subst_vars
       induction Γ
-      . exact ⟨_, ($defn).wf_nfTp.of_axioms_le $le, ($defn).wf_val.of_axioms_le $le⟩
+      . exact ⟨_, ($defn).wf_nfTp, ($defn).wf_val⟩
       . rename_i ih
         have B := Γwf.inv_snoc
         have ⟨_, vA, t⟩ := ih B.wf_ctx
@@ -209,15 +210,17 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
         convert t.subst (WfSb.wk B) using 1
         rw [Expr.subst_of_isClosed _ ($defn).wf_val.isClosed]
     )⟩
-  | ~q(CheckedAx.val $ax) => do
-    let le ← checkAxiomsLe q(($ax).snocAxioms) q($E)
+  | ~q(ReflectedAx.val $ax) => do
+    let _decEq ← synthInstanceQ q(DecidableEq $χ)
+    let .defEq _ ← isDefEqQ q($𝕋) q(($ax).snocAxioms)
+      | throwError "got axiom in theory{Lean.indentExpr q(($ax).snocAxioms)}\n\
+        while checking w.r.t. theory{Lean.indentExpr 𝕋}"
     let _ ← equateNat q($l) q(($ax).l)
     return ⟨q(($ax).nfTp), q(by as_aux_lemma =>
-      introv vΓ; have Γwf := vΓ.wf_ctx; clear vΓ
+      introv _ vΓ; have Γwf := vΓ.wf_ctx; clear vΓ
       subst_vars
-      have le' := Trans.trans ($ax).le_snocAxioms $le
       induction Γ
-      . exact ⟨_, ($ax).wf_nfTp.of_axioms_le le', ($ax).wf_val.of_axioms_le $le⟩
+      . exact ⟨_, ($ax).wf_nfTp.of_axioms_le ($ax).le_snocAxioms, ($ax).wf_val⟩
       . rename_i ih
         have B := Γwf.inv_snoc
         have ⟨_, vA, t⟩ := ih B.wf_ctx
@@ -226,41 +229,74 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
         rwa [Expr.subst_of_isClosed _ ($ax).wf_val.isClosed] at this
     )⟩
   | ~q(.ax $c $A) => do
-    let .inl ⟨A', l', get⟩ ← lookupAxiom q($E) q($c)
-      | throwError "could not find constant '{c}' in environment{Lean.indentExpr E}"
-    let leq ← equateNat q($l) q($l')
-    -- TODO: relax to a defeq check?
-    let ⟨_⟩ ← assertDefEqQ q($A) q($A')
-    -- NOTE: could also evaluate in empty environment here and then weaken `ValEqTp`;
-    -- I think it makes no difference.
-    let ⟨vA, vApost⟩ ← evalTpId q($vΓ) q($A)
-    return ⟨vA, q(by as_aux_lemma =>
-      introv vΓ
-      subst_vars
-      have ⟨_, Ec⟩ := $get
-      have := $vApost vΓ (($Ewf).atCtx vΓ.wf_ctx Ec)
-      refine ⟨_, this, .ax vΓ.wf_ctx Ec this.wf_tp⟩
-    )⟩
+    try -- an internal theory.
+      let w ← Lean.Meta.mkFreshLevelMVar
+      let 𝒞 ← mkFreshExprMVarQ q(Type w)
+      let _cat ← mkFreshExprMVarQ q(CategoryTheory.Category.{u,w} $𝒞)
+      let _ct ← mkFreshExprMVarQ q(CategoryTheory.ChosenTerminal.{u,w} $𝒞)
+      let s ← mkFreshExprMVarQ q(UHomSeq $𝒞)
+      let .defEq _ ← isDefEqQ q($χ) q(($s).SigInt) | throw (.internal ⟨1337⟩)
+      let .defEq _ ← isDefEqQ q($𝕋) q(($s).thyInt) | throw (.internal ⟨1337⟩)
+      match c with
+      | ~q(UHomSeq.SigInt.ty (l := $l') $lt $sA) =>
+        -- TODO: relax to equateTp?
+        let .defEq _ ← isDefEqQ q($A) q(.univ $l')
+          | throwError "unexpected type of semantic type constant{Lean.indentExpr A}"
+        let _ ← equateNat q($l) q($l' + 1)
+        return ⟨q(.univ $l'), q(by as_aux_lemma =>
+          introv 𝕋 vΓ
+          subst_vars
+          refine ⟨_,
+            .univ vΓ.wf_ctx $lt,
+            .ax vΓ.wf_ctx (Al := ⟨(.univ $l', $l' + 1), by simp [Expr.isClosed]; omega⟩)
+              rfl
+              (.univ vΓ.wf_ctx $lt)⟩
+        )⟩
+      | ~q(UHomSeq.SigInt.tm ..) => throwError "TODO: term deinterpretation is not implemented"
+      | _ => throwError "unknown base constant{Lean.indentExpr c}"
+    catch e =>
+      let .internal ⟨1337⟩ := e | throw e
+      try -- named axioms.
+        let .defEq _ ← isLevelDefEqQ u 0 | throw (.internal ⟨1337⟩)
+        let .defEq _ ← isDefEqQ q($χ) q(Lean.Name) | throw (.internal ⟨1337⟩)
+        let .inl ⟨A', l', get⟩ ← lookupAxiom 𝕋 c
+          | throwError "could not find constant '{c}' in theory{Lean.indentExpr 𝕋}"
+        let leq ← equateNat q($l) q($l')
+        -- TODO: relax to an `equateTp` check?
+        let ⟨_⟩ ← assertDefEqQ q($A) q($A')
+        let ⟨vA, vApost⟩ ← evalTpId q($vΓ) q($A)
+        /- NOTE: Could also evaluate in empty environment here and then weaken `ValEqTp`;
+        I think it makes no difference. -/
+        return ⟨vA, q(by as_aux_lemma =>
+          introv 𝕋 vΓ
+          subst_vars
+          have ⟨_, Ec⟩ := $get
+          have := $vApost vΓ (𝕋.atCtx vΓ.wf_ctx Ec)
+          refine ⟨_, this, .ax vΓ.wf_ctx Ec this.wf_tp⟩
+        )⟩
+      catch e =>
+        let .internal ⟨1337⟩ := e | throw e
+        throwError "got unknown theory{Lean.indentExpr 𝕋}"
   | ~q(.bvar $i) => do
     let ⟨vA, m, lk⟩ ← lookupVar q($vΓ) q($i)
     let lm ← equateNat q($l) q($m)
     return ⟨vA, q(by as_aux_lemma =>
-      introv vΓ
+      introv _ vΓ
       have ⟨_, vA, lk⟩ := $lk vΓ
       subst_vars
       exact ⟨_, vA, WfTm.bvar vΓ.wf_ctx lk⟩
     )⟩
   | ~q(.lam $k $k' $A $b) => do
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     let ⟨vA, vAeq⟩ ← evalTpId q($vΓ) q($A)
-    let ⟨vB, bB⟩ ← synthTm q(($vA, $k) :: $vΓ) q($k') q($b)
+    let ⟨vB, bB⟩ ← synthTm q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($b)
     let lmax ← equateNat q($l) q(max $k $k')
     return ⟨q(.pi $k $k' $vA (.of_val ($vΓ).toEnv $vB)), q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have A := $Awf vΓ
+      have A := $Awf 𝕋 vΓ
       have vA := $vAeq vΓ A
-      have ⟨B, vB, b⟩ := $bB (vΓ.snoc vA)
+      have ⟨B, vB, b⟩ := $bB 𝕋 (vΓ.snoc vA)
       refine ⟨.pi $k $k' $A B, ?_, WfTm.lam b⟩
       apply ValEqTp.pi vA
       convert ClosEqTp.clos_val_tp vΓ.toEnv_wf _ vB using 1
@@ -269,16 +305,16 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
     )⟩
   | ~q(.app $k $k' $B $f $a) => do
     let lk' ← equateNat q($l) q($k')
-    let ⟨vA, vApost⟩ ← synthTm q($vΓ) q($k) q($a)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
-    let fwf ← checkTm q($vΓ) q(max $k $k') q(.pi $k $k' $vA (.of_expr ($vΓ).toEnv $B)) q($f)
+    let ⟨vA, vApost⟩ ← synthTm q($𝕋) q($vΓ) q($k) q($a)
+    let Bwf ← checkTp q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($B)
+    let fwf ← checkTm q($𝕋) q($vΓ) q(max $k $k') q(.pi $k $k' $vA (.of_expr ($vΓ).toEnv $B)) q($f)
     let ⟨va, vaeq⟩ ← evalTmId q($vΓ) q($a)
     let ⟨vBa, vBaeq⟩ ← evalTp q($va :: ($vΓ).toEnv) q($B)
     return ⟨vBa, q(by as_aux_lemma =>
-      introv vΓ
-      have ⟨_, vA, a⟩ := $vApost vΓ
-      have B := $Bwf <| vΓ.snoc vA
-      have f := $fwf vΓ <| ValEqTp.pi vA <|
+      introv 𝕋 vΓ
+      have ⟨_, vA, a⟩ := $vApost 𝕋 vΓ
+      have B := $Bwf 𝕋 <| vΓ.snoc vA
+      have f := $fwf 𝕋 vΓ <| ValEqTp.pi vA <|
         ClosEqTp.clos_tp vΓ.toEnv_wf (by convert EqTp.refl_tp a.wf_tp using 1; autosubst) B
       have va := $vaeq vΓ a
       have := vΓ.toEnv_wf.snoc va.wf_tm.wf_tp (by convert va using 1; autosubst)
@@ -288,19 +324,19 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
     )⟩
   | ~q(.pair $k $k' $B $f $s) => do
     let lmax ← equateNat q($l) q(max $k $k')
-    let ⟨vA, fA⟩ ← synthTm q($vΓ) q($k) q($f)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
+    let ⟨vA, fA⟩ ← synthTm q($𝕋) q($vΓ) q($k) q($f)
+    let Bwf ← checkTp q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($B)
     let ⟨vf, vfpost⟩ ← evalTmId q($vΓ) q($f)
     let ⟨vBf, vBfpost⟩ ← evalTp q($vf :: ($vΓ).toEnv) q($B)
-    let swf ← checkTm q($vΓ) q($k') q($vBf) q($s)
+    let swf ← checkTm q($𝕋) q($vΓ) q($k') q($vBf) q($s)
     return ⟨q(.sigma $k $k' $vA (.of_expr ($vΓ).toEnv $B)), q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have ⟨_, vA, f⟩ := $fA vΓ
-      have B := $Bwf <| vΓ.snoc vA
+      have ⟨_, vA, f⟩ := $fA 𝕋 vΓ
+      have B := $Bwf 𝕋 <| vΓ.snoc vA
       have vf := $vfpost vΓ f
       have vBf := $vBfpost (vΓ.toEnv_wf.snoc f.wf_tp (by convert vf using 1; autosubst)) B
-      have s := $swf vΓ vBf
+      have s := $swf 𝕋 vΓ vBf
       have := ValEqTp.sigma vA <|
         ClosEqTp.clos_tp vΓ.toEnv_wf (by convert EqTp.refl_tp vA.wf_tp using 1; autosubst) B
       refine ⟨_, this, ?_⟩
@@ -309,18 +345,18 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
     )⟩
   | ~q(.fst $k $k' $A $B $p) => do
     let leq ← equateNat q($l) q($k)
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     let ⟨vA, vApost⟩ ← evalTpId q($vΓ) q($A)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
+    let Bwf ← checkTp q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($B)
     let pwf ← checkTm
-      q($vΓ) q(max $k $k') q(.sigma $k $k' $vA (.of_expr ($vΓ).toEnv $B)) q($p)
+      q($𝕋) q($vΓ) q(max $k $k') q(.sigma $k $k' $vA (.of_expr ($vΓ).toEnv $B)) q($p)
     return ⟨vA, q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have A := $Awf vΓ
+      have A := $Awf 𝕋 vΓ
       have vA := $vApost vΓ A
-      have B := $Bwf <| vΓ.snoc vA
-      have p := $pwf vΓ <| ValEqTp.sigma vA <|
+      have B := $Bwf 𝕋 <| vΓ.snoc vA
+      have p := $pwf 𝕋 vΓ <| ValEqTp.sigma vA <|
         ClosEqTp.clos_tp vΓ.toEnv_wf (by convert EqTp.refl_tp vA.wf_tp using 1; autosubst) B
       refine ⟨_, vA, ?_⟩
       simp +zetaDelta only [autosubst] at p ⊢
@@ -328,21 +364,21 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
     )⟩
   | ~q(.snd $k $k' $A $B $p) => do
     let leq ← equateNat q($l) q($k')
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     let ⟨vA, vApost⟩ ← evalTpId q($vΓ) q($A)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
+    let Bwf ← checkTp q($𝕋) q(($vA, $k) :: $vΓ) q($k') q($B)
     let pwf ←
-      checkTm q($vΓ) q(max $k $k') q(.sigma $k $k' $vA (.of_expr ($vΓ).toEnv $B)) q($p)
+      checkTm q($𝕋) q($vΓ) q(max $k $k') q(.sigma $k $k' $vA (.of_expr ($vΓ).toEnv $B)) q($p)
     let ⟨vp, vppost⟩ ← evalTmId q($vΓ) q($p)
     let ⟨vf, vfpost⟩ ← evalFst q($vp)
     let ⟨vBf, vBfpost⟩ ← evalTp q($vf :: ($vΓ).toEnv) q($B)
     return ⟨vBf, q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have A := $Awf vΓ
+      have A := $Awf 𝕋 vΓ
       have vA := $vApost vΓ A
-      have B := $Bwf <| vΓ.snoc vA
-      have p := $pwf vΓ <| ValEqTp.sigma vA <|
+      have B := $Bwf 𝕋 <| vΓ.snoc vA
+      have p := $pwf 𝕋 vΓ <| ValEqTp.sigma vA <|
         ClosEqTp.clos_tp vΓ.toEnv_wf (by convert EqTp.refl_tp vA.wf_tp using 1; autosubst) B
       have vp := $vppost vΓ p
       have vf := $vfpost vp
@@ -354,44 +390,44 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
     )⟩
   | ~q(.refl $k $a) => do
     let leq ← equateNat q($l) q($k)
-    let ⟨vA, vApost⟩ ← synthTm q($vΓ) q($l) q($a)
+    let ⟨vA, vApost⟩ ← synthTm q($𝕋) q($vΓ) q($l) q($a)
     let ⟨va, vapost⟩ ← evalTmId q($vΓ) q($a)
     return ⟨q(.Id $k $vA $va $va), q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have ⟨_, vA, a⟩ := $vApost vΓ
+      have ⟨_, vA, a⟩ := $vApost 𝕋 vΓ
       have va := $vapost vΓ a
       refine ⟨_, ValEqTp.Id vA va va, WfTm.refl a⟩
     )⟩
   | ~q(.idRec $k $k' $a $M $r $b $h) => do
     let leq ← equateNat q($l) q($k')
-    let ⟨vA, vApost⟩ ← synthTm q($vΓ) q($k) q($a)
+    let ⟨vA, vApost⟩ ← synthTm q($𝕋) q($vΓ) q($k) q($a)
     let ⟨va, vapost⟩ ← evalTmId q($vΓ) q($a)
-    let Mwf ← checkTp
+    let Mwf ← checkTp q($𝕋)
       q((.Id $k $vA $va (.neut (.bvar ($vΓ).length) $vA), $k) :: ($vA, $k) :: $vΓ) q($k') q($M)
     let ⟨vMa, vMapost⟩ ← evalTp q((.refl $k $va) :: $va :: ($vΓ).toEnv) q($M)
-    let rwf ← checkTm q($vΓ) q($k') q($vMa) q($r)
-    let bwf ← checkTm q($vΓ) q($k) q($vA) q($b)
+    let rwf ← checkTm q($𝕋) q($vΓ) q($k') q($vMa) q($r)
+    let bwf ← checkTm q($𝕋) q($vΓ) q($k) q($vA) q($b)
     let ⟨vb, vbpost⟩ ← evalTmId q($vΓ) q($b)
-    let hwf ← checkTm q($vΓ) q($k) q(.Id $k $vA $va $vb) q($h)
+    let hwf ← checkTm q($𝕋) q($vΓ) q($k) q(.Id $k $vA $va $vb) q($h)
     let ⟨vh, vhpost⟩ ← evalTmId q($vΓ) q($h)
     let ⟨vMb, vMbpost⟩ ← evalTp q($vh :: $vb :: ($vΓ).toEnv) q($M)
     return ⟨q($vMb), q(by as_aux_lemma =>
-      introv vΓ
+      introv 𝕋 vΓ
       subst_vars
-      have ⟨_, vA, a⟩ := $vApost vΓ
+      have ⟨_, vA, a⟩ := $vApost 𝕋 vΓ
       have va := $vapost vΓ a
       have := ValEqTp.Id_bvar vA va
       rw [← vΓ.length_eq] at this
-      have M := $Mwf (vΓ.snoc vA |>.snoc this)
+      have M := $Mwf 𝕋 (vΓ.snoc vA |>.snoc this)
       have := vΓ.toEnv_wf
         |>.snoc a.wf_tp (autosubst% va)
         |>.snoc (WfTp.Id_bvar a) (autosubst% ValEqTm.refl va)
       have vMa := $vMapost this M
-      have r := $rwf vΓ vMa
-      have b := $bwf vΓ vA
+      have r := $rwf 𝕋 vΓ vMa
+      have b := $bwf 𝕋 vΓ vA
       have vb := $vbpost vΓ b
-      have h := $hwf vΓ (ValEqTp.Id vA va vb)
+      have h := $hwf 𝕋 vΓ (ValEqTp.Id vA va vb)
       have vh := $vhpost vΓ h
       have := vΓ.toEnv_wf
         |>.snoc a.wf_tp (autosubst% vb)
@@ -403,10 +439,10 @@ partial def synthTm (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat)) (t : Q(Expr Lean.Nam
     -- TODO: WHNF `l`? See comment at `evalTp`.
     let ~q(.succ $k) := l | throwError "expected _+1, got{Lean.indentExpr l}"
     let lmax ← ltNat q($k) q(univMax)
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+    let Awf ← checkTp q($𝕋) q($vΓ) q($k) q($A)
     return ⟨q(.univ $k), q(by as_aux_lemma =>
-      introv vΓ
-      exact ⟨_, ValEqTp.univ vΓ.wf_ctx $lmax, WfTm.code $lmax ($Awf vΓ)⟩
+      introv 𝕋 vΓ
+      exact ⟨_, ValEqTp.univ vΓ.wf_ctx $lmax, WfTm.code $lmax ($Awf 𝕋 vΓ)⟩
     )⟩
   | t =>
     throwError "expected a term, got{Lean.indentExpr t}"
diff --git a/HoTTLean/Typechecker/Util.lean b/HoTTLean/Typechecker/Util.lean
index 5d7abbbd..771a0fd1 100644
--- a/HoTTLean/Typechecker/Util.lean
+++ b/HoTTLean/Typechecker/Util.lean
@@ -14,10 +14,17 @@ def mkLetFVarsQ {u : Level} {T : Q(Sort u)} (xs : Array Lean.Expr) (e : Q($T))
   mkLetFVars xs e (usedLetOnly := usedLetOnly) (generalizeNondepLet := generalizeNondepLet)
     (binderInfoForMVars := binderInfoForMVars)
 
+/-- Like `inferTypeQ` but yields `Type u` rather than `Sort u`. -/
+def inferTypeQ' (e : Expr) : MetaM ((u : Level) × (α : Q(Type $u)) × Q($α)) := do
+  let α ← inferType e
+  let .sort (.succ u) ← whnf (← inferType α) | throwError "not a type{indentExpr α}"
+  pure ⟨u, α, e⟩
+
 end Qq
 
 namespace SynthLean
 open Qq
+open Lean Meta
 
 def equateNat (n m : Q(Nat)) : Lean.MetaM Q($n = $m) := do
   let some vn ← Lean.Meta.evalNat (← Lean.Meta.whnf n)
@@ -36,6 +43,12 @@ def ltNat (n m : Q(Nat)) : Lean.MetaM Q($n < $m) := do
   let pf ← Lean.Meta.mkEqRefl q(decide ($n < $m))
   Lean.Meta.mkAppM ``of_decide_eq_true #[pf]
 
+unsafe def evalExprExprUnsafe (e : Q(Lean.Expr)) : MetaM Lean.Expr :=
+  evalExpr' Lean.Expr ``Lean.Expr e
+
+@[implemented_by evalExprExprUnsafe]
+opaque evalExprExpr (e : Q(Lean.Expr)) : MetaM Lean.Expr
+
 end SynthLean
 
 -- /-- Hacks to use during development:
diff --git a/HoTTLean/Typechecker/Value.lean b/HoTTLean/Typechecker/Value.lean
index f88be533..89607ea6 100644
--- a/HoTTLean/Typechecker/Value.lean
+++ b/HoTTLean/Typechecker/Value.lean
@@ -568,6 +568,15 @@ theorem EnvEqSb.wk {Δ Eᵥ σ Γ} (h : EnvEqSb E Δ Eᵥ σ Γ) {C k} (hC : E 
     EnvEqSb E ((C,k) :: Δ) Eᵥ (Expr.comp Expr.wk σ) Γ :=
   wk_all.2.2.2.2.2.2 h hC
 
+theorem ValEqTp.wk_many {l vA A} (h : ValEqTp E [] l vA A) {Γ} (hΓ : WfCtx E Γ) :
+    ValEqTp E Γ l vA A := by
+  have A_cl : A.isClosed := h.wf_tp.isClosed
+  induction Γ with
+  | nil => assumption
+  | cons _ _ ih =>
+    cases hΓ with | snoc Γ A
+    simpa [Expr.subst_of_isClosed _ A_cl] using (ih Γ).wk A
+
 /-! ## Type environments -/
 
 /-- A type environment is a context where all types are in NF. -/
@@ -639,47 +648,201 @@ theorem TpEnvEqCtx.toEnv_wf {vΓ Γ} : TpEnvEqCtx E vΓ Γ → EnvEqSb E Γ vΓ.
 
 /-! ## Monotonicity w.r.t. axioms -/
 
-attribute [local grind .] WfCtx.of_axioms_le WfTp.of_axioms_le WfTm.of_axioms_le EqTp.of_axioms_le
-  EqTm.of_axioms_le in
-private theorem of_axioms_le_all {E E' : Axioms χ} (le : E ≤ E') :
-    (∀ {Γ l vA A}, ValEqTp E Γ l vA A → ValEqTp E' Γ l vA A) ∧
-    (∀ {Γ l vt t A}, ValEqTm E Γ l vt t A → ValEqTm E' Γ l vt t A) ∧
-    (∀ {Γ l vt t A}, NeutEqTm E Γ l vt t A → NeutEqTm E' Γ l vt t A) ∧
-    (∀ {Γ l l' A vB B}, ClosEqTp E Γ l l' A vB B → ClosEqTp E' Γ l l' A vB B) ∧
-    (∀ {Γ A l B l' l'' vC C}, Clos₂EqTp E Γ A l B l' l'' vC C → Clos₂EqTp E' Γ A l B l' l'' vC C) ∧
-    (∀ {Γ l l' A B vb b}, ClosEqTm E Γ l l' A B vb b → ClosEqTm E' Γ l l' A B vb b) ∧
-    (∀ {Γ Eᵥ σ Δ}, EnvEqSb E Γ Eᵥ σ Δ → EnvEqSb E' Γ Eᵥ σ Δ) := by
+section
+variable {χ χ' : Type*} (f : χ → χ')
+
+mutual
+-- Semireducible so that the typechecker can WHNF through applications of `map` to constructors.
+-- FIXME: The WHNFs become quite gnarly. Use a custom reducer instead?
+@[semireducible]
+def Val.map : Val χ → Val χ'
+  | .pi l l' A B => .pi l l' A.map B.map
+  | .sigma l l' A B => .sigma l l' A.map B.map
+  | .Id l A t u => .Id l A.map t.map u.map
+  | .univ l => .univ l
+  | .el a => .el a.map
+  | .lam l l' vA b => .lam l l' vA.map b.map
+  | .pair l l' t u => .pair l l' t.map u.map
+  | .refl l t => .refl l t.map
+  | .code A => .code A.map
+  | .neut n A => .neut n.map A.map
+
+@[semireducible]
+def Neut.map : Neut χ → Neut χ'
+  | .ax c A => .ax (f c) A.map
+  | .bvar i => .bvar i
+  | .app l l' A f a => .app l l' A.map f.map a.map
+  | .fst l l' p => .fst l l' p.map
+  | .snd l l' p => .snd l l' p.map
+  | .idRec l l' A a M r h => .idRec l l' A.map a.map M.map r.map h.map
+
+@[semireducible]
+def Clos.map : Clos χ → Clos χ'
+  | .of_val env v => .of_val (env.map Val.map) v.map
+  | .of_expr env t => .of_expr (env.map Val.map) (t.map f)
+end
+
+private theorem map_id_all :
+    (∀ v, Val.map (id : χ → χ) v = v) ∧
+    (∀ n, Neut.map (id : χ → χ) n = n) ∧
+    (∀ c, Clos.map (id : χ → χ) c = c) := by
+  refine ⟨
+    Val.rec (motive_4 := fun l => l.map (Val.map id) = l)
+      ?pi ?sigma ?Id ?univ ?el ?lam ?pair ?refl ?code ?neut
+      ?ax ?bvar ?app ?fst ?snd ?idRec ?of_val ?of_expr ?nil ?cons,
+    Neut.rec
+      ?pi ?sigma ?Id ?univ ?el ?lam ?pair ?refl ?code ?neut
+      ?ax ?bvar ?app ?fst ?snd ?idRec ?of_val ?of_expr ?nil ?cons,
+    Clos.rec
+      ?pi ?sigma ?Id ?univ ?el ?lam ?pair ?refl ?code ?neut
+      ?ax ?bvar ?app ?fst ?snd ?idRec ?of_val ?of_expr ?nil ?cons
+  ⟩
+  all_goals simp [Val.map, Neut.map, Clos.map]; try grind
+
+@[simp] theorem Val.map_id_fun : Val.map (id : χ → χ) = id := funext map_id_all.1
+@[simp] theorem Val.map_id_fun' : Val.map (fun (c : χ) => c) = id := map_id_fun
+@[simp] theorem Neut.map_id_fun : Neut.map (id : χ → χ) = id := funext map_id_all.2.1
+@[simp] theorem Neut.map_id_fun' : Neut.map (fun (c : χ) => c) = id := Neut.map_id_fun
+@[simp] theorem Clos.map_id_fun : Clos.map (id : χ → χ) = id := funext map_id_all.2.2
+@[simp] theorem Clos.map_id_fun' : Clos.map (fun (c : χ) => c) = id := Clos.map_id_fun
+
+variable {f} {𝕋 : Axioms χ} {𝕋' : Axioms χ'} (H : WfTheoryMap 𝕋 f 𝕋')
+include H
+
+attribute [local grind .] WfCtx.map WfTp.map EqTp.map EqTm.map in
+private theorem map_all :
+    (∀ {Γ l vA A}, ValEqTp 𝕋 Γ l vA A →
+      ValEqTp 𝕋' (Γ.map f) l (vA.map f) (A.map f)) ∧
+    (∀ {Γ l vt t A}, ValEqTm 𝕋 Γ l vt t A →
+      ValEqTm 𝕋' (Γ.map f) l (vt.map f) (t.map f) (A.map f)) ∧
+    (∀ {Γ l vt t A}, NeutEqTm 𝕋 Γ l vt t A →
+      NeutEqTm 𝕋' (Γ.map f) l (vt.map f) (t.map f) (A.map f)) ∧
+    (∀ {Γ l l' A vB B}, ClosEqTp 𝕋 Γ l l' A vB B →
+      ClosEqTp 𝕋' (Γ.map f) l l' (A.map f) (vB.map f) (B.map f)) ∧
+    (∀ {Γ A l B l' l'' vC C}, Clos₂EqTp 𝕋 Γ A l B l' l'' vC C →
+      Clos₂EqTp 𝕋' (Γ.map f) (A.map f) l (B.map f) l' l'' (vC.map f) (C.map f)) ∧
+    (∀ {Γ l l' A B vb b}, ClosEqTm 𝕋 Γ l l' A B vb b →
+      ClosEqTm 𝕋' (Γ.map f) l l' (A.map f) (B.map f) (vb.map f) (b.map f)) ∧
+    (∀ {Γ Eᵥ σ Δ}, EnvEqSb 𝕋 Γ Eᵥ σ Δ →
+      EnvEqSb 𝕋' (Γ.map f) (Eᵥ.map (·.map f)) (Expr.map f ∘ σ) (Δ.map f)) := by
   mutual_induction ValEqTp
-  case ax => introv _ Ec _ ihA; apply NeutEqTm.ax _ (le Ec) ihA; grind
-  grind_cases
+  all_goals
+    intros
+    try simp only [Val.map, Neut.map, Clos.map, Expr.map,
+      Expr.subst_map, ← Expr.map_toSb, ← Expr.snoc_map_comp, Expr.map_comp_wk, ← Expr.up_map_comp,
+      Ctx.map_cons] at *
+  case ax Al _ 𝕋c _ _ =>
+    apply NeutEqTm.ax (Al := ⟨(Al.1.1.map f, Al.1.2), by simp [Al.2]⟩)
+    . grind
+    . apply 𝕋c ▸ H.get_eq _ (Option.isSome_iff_exists.mpr ⟨_, 𝕋c⟩)
+    . assumption
+  case pi => apply ValEqTp.pi <;> grind
+  case sigma => apply ValEqTp.sigma <;> grind
+  case Id => apply ValEqTp.Id <;> grind
+  case univ => apply ValEqTp.univ <;> grind
+  case el => apply ValEqTp.el ‹_›
+  case conv_tp => apply ValEqTp.conv_tp ‹_›; grind
+  case lam => apply ValEqTm.lam <;> grind
+  case pair B _ _ _ _ => have := B.map H; apply ValEqTm.pair <;> grind [Ctx.map_cons]
+  case refl => apply ValEqTm.refl ‹_›
+  case code => apply ValEqTm.code <;> grind
+  case neut_tm => apply ValEqTm.neut_tm <;> grind
+  case conv_nf => apply ValEqTm.conv_nf ‹_› <;> grind
+  case bvar Γ lk => have := NeutEqTm.bvar (Γ.map H) (lk.map f); simpa using this
+  case app => apply NeutEqTm.app ‹_› <;> grind
+  case fst => apply NeutEqTm.fst ‹_›
+  case snd => apply NeutEqTm.snd ‹_›
+  case idRec => apply NeutEqTm.idRec ‹_› <;> grind
+  case conv_neut => apply NeutEqTm.conv_neut ‹_› <;> grind
+  case clos_tp Aeq B _ =>
+    have := Aeq.map H
+    simp only [Expr.subst_map] at this
+    apply ClosEqTp.clos_tp ‹_› this (B.map H)
+  case clos_val_tp Aeq _ _ _ =>
+    have := Aeq.map H
+    simp only [Expr.subst_map] at this
+    apply ClosEqTp.clos_val_tp ‹_› this ‹_›
+  case clos₂_tp Aeq Beq C _ =>
+    have Aeq' := Aeq.map H
+    have Beq' := Beq.map H
+    simp only [Expr.subst_map, ← Expr.up_map_comp] at *
+    apply Clos₂EqTp.clos₂_tp ‹_› Aeq' Beq' (C.map H)
+  case clos₂_val_tp Aeq Beq _ _ _ =>
+    have Aeq' := Aeq.map H
+    have Beq' := Beq.map H
+    simp only [Expr.subst_map, ← Expr.up_map_comp] at *
+    apply Clos₂EqTp.clos₂_val_tp ‹_› Aeq' Beq' ‹_›
+  case clos_tm Aeq Beq b _ =>
+    have Aeq' := Aeq.map H
+    have Beq' := Beq.map H
+    simp only [Expr.subst_map, ← Expr.up_map_comp] at *
+    apply ClosEqTm.clos_tm ‹_› Aeq' Beq' (b.map H)
+  case clos_val_tm Aeq Beq b _ _ =>
+    have Aeq' := Aeq.map H
+    have Beq' := Beq.map H
+    simp only [Expr.subst_map, ← Expr.up_map_comp] at *
+    apply ClosEqTm.clos_val_tm ‹_› Aeq' Beq' ‹_›
+  case nil => apply EnvEqSb.nil; grind
+  case snoc => apply EnvEqSb.snoc <;> grind
+
+variable {Γ l l' l'' A B C t u n b vA vB vC vt vn vb}
+
+theorem ValEqTp.map (h : ValEqTp 𝕋 Γ l vA A) : ValEqTp 𝕋' (Γ.map f) l (vA.map f) (A.map f) :=
+  map_all H |>.1 h
+
+theorem ValEqTm.map (h : ValEqTm 𝕋 Γ l vt t A) :
+    ValEqTm 𝕋' (Γ.map f) l (vt.map f) (t.map f) (A.map f) :=
+  map_all H |>.2.1 h
+
+theorem NeutEqTm.map (h : NeutEqTm 𝕋 Γ l vn n A) :
+    NeutEqTm 𝕋' (Γ.map f) l (vn.map f) (n.map f) (A.map f) :=
+  map_all H |>.2.2.1 h
+
+theorem ClosEqTp.map (h : ClosEqTp 𝕋 Γ l l' A vB B) :
+    ClosEqTp 𝕋' (Γ.map f) l l' (A.map f) (vB.map f) (B.map f) :=
+  map_all H |>.2.2.2.1 h
+
+theorem Clos₂EqTp.map (h : Clos₂EqTp 𝕋 Γ A l B l' l'' vC C) :
+    Clos₂EqTp 𝕋' (Γ.map f) (A.map f) l (B.map f) l' l'' (vC.map f) (C.map f) :=
+  map_all H |>.2.2.2.2.1 h
+
+theorem ClosEqTm.map (h : ClosEqTm 𝕋 Γ l l' A B vb b) :
+    ClosEqTm 𝕋' (Γ.map f) l l' (A.map f) (B.map f) (vb.map f) (b.map f) :=
+  map_all H |>.2.2.2.2.2.1 h
+
+theorem EnvEqSb.map {Δ Eᵥ σ Γ} (h : EnvEqSb 𝕋 Δ Eᵥ σ Γ) :
+    EnvEqSb 𝕋' (Δ.map f) (Eᵥ.map (·.map f)) (Expr.map f ∘ σ) (Γ.map f) :=
+  map_all H |>.2.2.2.2.2.2 h
+
+end
 
 theorem ValEqTp.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Γ l vA A} :
     ValEqTp E Γ l vA A → ValEqTp E' Γ l vA A :=
-  fun h => of_axioms_le_all le |>.1 h
+  fun h => by simpa using h.map (.of_le le)
 
 theorem ValEqTm.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Γ l vt t A} :
     ValEqTm E Γ l vt t A → ValEqTm E' Γ l vt t A :=
-  fun h => of_axioms_le_all le |>.2.1 h
+  fun h => by simpa using h.map (.of_le le)
 
 theorem NeutEqTm.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Γ l vn n A} :
     NeutEqTm E Γ l vn n A → NeutEqTm E' Γ l vn n A :=
-  fun h => of_axioms_le_all le |>.2.2.1 h
+  fun h => by simpa using h.map (.of_le le)
 
 theorem ClosEqTp.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Γ l l' A vB B} :
     ClosEqTp E Γ l l' A vB B → ClosEqTp E' Γ l l' A vB B :=
-  fun h => of_axioms_le_all le |>.2.2.2.1 h
+  fun h => by simpa using h.map (.of_le le)
 
 theorem Clos₂EqTp.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Γ A l B l' l'' vC C} :
     Clos₂EqTp E Γ A l B l' l'' vC C → Clos₂EqTp E' Γ A l B l' l'' vC C :=
-  fun h => of_axioms_le_all le |>.2.2.2.2.1 h
+  fun h => by simpa using h.map (.of_le le)
 
 theorem ClosEqTm.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Γ l l' A B vb b} :
     ClosEqTm E Γ l l' A B vb b → ClosEqTm E' Γ l l' A B vb b :=
-  fun h => of_axioms_le_all le |>.2.2.2.2.2.1 h
+  fun h => by simpa using h.map (.of_le le)
 
 theorem EnvEqSb.of_axioms_le {E E' : Axioms χ} (le : E ≤ E') {Δ Eᵥ σ Γ} :
     EnvEqSb E Δ Eᵥ σ Γ → EnvEqSb E' Δ Eᵥ σ Γ :=
-  fun h => of_axioms_le_all le |>.2.2.2.2.2.2 h
+  fun h => by simpa using h.map (.of_le le)
 
 /-! ## Misc lemmas -/
 
diff --git a/HoTTLeanTest.lean b/HoTTLeanTest.lean
new file mode 100644
index 00000000..49d60ddf
--- /dev/null
+++ b/HoTTLeanTest.lean
@@ -0,0 +1,5 @@
+import HoTTLeanTest.basic
+import HoTTLeanTest.import
+import HoTTLeanTest.hott0
+import HoTTLeanTest.prod_defeq
+import HoTTLeanTest.unitt
diff --git a/HoTTLeanTest/basic.lean b/HoTTLeanTest/basic.lean
new file mode 100644
index 00000000..d32d7bf7
--- /dev/null
+++ b/HoTTLeanTest/basic.lean
@@ -0,0 +1,102 @@
+import HoTTLean.Frontend.Reflect
+
+/-! Test basic typechecker functionality. -/
+
+/-! ## Universes -/
+
+@[reflect]
+def tp_univ : Type 1 := Type 0
+
+/-! ## Functions -/
+
+@[reflect]
+def tp_pi_nondep : Type 1 := Type 0 → Type 0
+
+def tm_lam_nondep : Type 0 → Type 0 := fun x => x
+
+def tp_pi : Type 1 := (A : Type 0) → A → A
+
+def tm_lam : (A : Type 0) → A → A := fun _ a => a
+
+def tm_app : (A : Type 0) → A → (A → A) → A := fun _ a f => f a
+
+/-! ## Products -/
+
+@[reflect]
+def tp_sigma : Type 1 :=
+  (A : Type) × A
+
+@[reflect]
+def tp_sigma_partial : (A : Type) → (B : A → Type) → Type :=
+  @Sigma
+
+@[reflect]
+def tm_pair_nondep : (_ : Type 1) × Type 1 :=
+  ⟨Type 0, Type 0⟩
+
+-- Noncomputable due to Lean issue https://github.com/leanprover/lean4/issues/9692
+-- FIXME: needs at least 4 universes.
+-- mltt noncomputable def tm_pair : (A : Type 2) × A :=
+--   ⟨Type 1, Type 0⟩
+
+@[reflect]
+def tm_fst : Type 2 :=
+  { fst := Type 1, snd := Type 0 : (A : Type 2) × A }.fst
+
+@[reflect]
+def tm_snd : Type 1 :=
+  { fst := Type 1, snd := Type 0 : (A : Type 2) × A }.snd
+
+/-! ## Identity types -/
+
+@[reflect]
+def tp_id : Type 2 :=
+  @Identity (Type 1) Type Type
+
+@[reflect]
+def tm_refl : @Identity (Type 1) Type Type :=
+  @Identity.refl (Type 1) Type
+
+@[reflect]
+noncomputable def tm_idRec (A B : Type) (eq : @Identity Type A B) (a : A) : B :=
+  @Identity.rec Type A (fun T _ => T) a B eq
+
+/-! ## Definitional equalities -/
+
+@[reflect]
+def defeq_el_code {A : Type} (a : A) : A :=
+  (fun (α : Type) (x : α) => x) ((fun (α : Type 1) (x : α) => x) Type A) a
+
+/-! ## Using previous definitions -/
+
+@[reflect]
+def tm_refl' : tp_id := tm_refl
+
+/-! ## Adding axioms -/
+
+@[reflect]
+axiom B : Type
+
+@[reflect]
+axiom b : B
+
+@[reflect]
+axiom C : B → Type
+
+@[reflect]
+axiom c : C b
+
+/-! ## Using axioms -/
+
+@[reflect]
+def Cb : Type := C b
+
+@[reflect]
+noncomputable def c' : Cb := c
+
+/-! ## Using `sorry` -/
+
+/-- warning: declaration uses `sorry` -/
+#guard_msgs in
+@[reflect]
+def foo : Type := sorry
diff --git a/HoTTLeanTest/hott0.lean b/HoTTLeanTest/hott0.lean
new file mode 100644
index 00000000..54ee9964
--- /dev/null
+++ b/HoTTLeanTest/hott0.lean
@@ -0,0 +1,74 @@
+import HoTTLean.Frontend.Reflect
+
+noncomputable section
+
+namespace HoTT0
+
+@[reflect]
+def isSection₀₀ {A B : Type} (f : A → B) (g : B → A) : Type :=
+  ∀ (a : A), Identity (g (f a)) a
+
+@[reflect]
+def isEquiv₀₀ {A B : Type} (f : A → B) : Type :=
+  Σ (g : B → A),
+    Σ (h : B → A),
+      Σ (_ : isSection₀₀ f g),
+        isSection₀₀ h f
+
+@[reflect]
+def happly {A : Type} {B : A → Type} {f g : (a : A) → B a} :
+    Identity f g → (a : A) → Identity (f a) (g a) :=
+  fun h _ => h.rec .rfl₀
+
+/-- HoTT book, Axiom 2.9.3. -/
+@[reflect]
+axiom funext₀₀ {A : Type} {B : A → Type} (f g : (a : A) → B a) :
+  isEquiv₀₀ (@happly _ _ f g)
+
+@[reflect]
+def isSection₁₀ {A : Type 1} {B : Type} (f : A → B) (g : B → A) : Type 1 :=
+  ∀ (a : A), Identity (g (f a)) a
+
+@[reflect]
+def isSection₀₁ {A : Type} {B : Type 1} (f : A → B) (g : B → A) : Type :=
+  ∀ (a : A), Identity (g (f a)) a
+
+@[reflect]
+def isEquiv₁₀ {A : Type 1} {B : Type} (f : A → B) : Type 1 :=
+  Σ (g : B → A),
+    Σ (h : B → A),
+      Σ (_ : isSection₁₀ f g),
+        isSection₀₁ h f
+
+@[reflect]
+def isEquiv₁₀_grpd {A : Type 1} {B : Type} (f : A → B) : Type 1 :=
+  Σ (g : B → A),
+    Σ (_ : isSection₁₀ f g),
+      isSection₀₁ g f
+
+@[reflect]
+def transport₀ {A B : Type} (h : Identity A B) (a : A) : B :=
+  h.rec a
+
+@[reflect]
+def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv₀₀ (transport₀ h) :=
+  h.rec ⟨fun a => a, fun a => a, fun _ => .rfl₀, fun _ => .rfl₀⟩
+
+@[reflect]
+def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
+  fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
+
+/-- The type `A` is (-1)-truncated. -/
+@[reflect]
+def isProp₀ (A : Type) : Type :=
+  ∀ (a a' : A), Identity a a'
+
+/-- The type `A` is 0-truncated. -/
+@[reflect]
+def isSet₀ (A : Type) : Type :=
+  ∀ (a b : A), isProp₀ (Identity a b)
+
+/-- The univalence axiom for sets. See HoTT book, Axiom 2.10.3. -/
+@[reflect]
+axiom setUv₀₀ {A B : Type} (A_set : isSet₀ A) (B_set : isSet₀ B) :
+  isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
diff --git a/HoTTLeanTest/import.lean b/HoTTLeanTest/import.lean
new file mode 100644
index 00000000..647b0eac
--- /dev/null
+++ b/HoTTLeanTest/import.lean
@@ -0,0 +1,12 @@
+import HoTTLeanTest.basic
+
+/-! Test importing a theory.
+
+Note: this is no longer as test-worthy since we deprecated theory-environments,
+and `@[reflect]` just uses the ordinary Lean environment. -/
+
+@[reflect]
+noncomputable def tm_refl'' : tp_id := tm_refl'
+
+@[reflect]
+def B'' : Type := B
diff --git a/HoTTLeanTest/prod_defeq.lean b/HoTTLeanTest/prod_defeq.lean
new file mode 100644
index 00000000..134c0bd4
--- /dev/null
+++ b/HoTTLeanTest/prod_defeq.lean
@@ -0,0 +1,72 @@
+import HoTTLean.Frontend.Reflect
+import HoTTLean.Model.Unstructured.Interpretation
+
+/-!
+Example requested by B. Mehta at
+https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean4Less.20discussion.20thread/near/561924413
+-/
+
+namespace SynthLean
+open Qq
+
+/-- Helper to check judgmental term equality. -/
+partial def equateWfTms (E : Q(Axioms Lean.Name))
+    (vΓ : Q(TpEnv Lean.Name)) (l : Q(Nat))
+    (a b T : Q(Expr Lean.Name)) :
+    TypecheckerM Q(∀ {Γ}, TpEnvEqCtx $E $vΓ Γ →
+      $E ∣ Γ ⊢[$l] ($a) : $T → $E ∣ Γ ⊢[$l] ($b) : $T →
+      $E ∣ Γ ⊢[$l] ($a) ≡ ($b) : $T) := do
+  let ⟨vT, vTeq⟩ ← evalTpId q($vΓ) q($T)
+  let ⟨va, vaeq⟩ ← evalTmId q($vΓ) q($a)
+  let ⟨vb, vbeq⟩ ← evalTmId q($vΓ) q($b)
+  let eq ← equateTm q(($vΓ).length) q($l) q($vT) q($va) q($vb)
+  return q(by as_aux_lemma =>
+    introv vΓ aT bT
+    apply ($eq) vΓ.length_eq ($vTeq vΓ aT.wf_tp) ($vaeq vΓ aT) ($vbeq vΓ bT)
+  )
+
+end SynthLean
+
+noncomputable section
+
+@[reflect]
+def MyProd (A B : Type) := Sigma fun (_ : A) => B
+
+@[reflect]
+def myFunc {A B C : Type} : (MyProd A B → C) → A → B → C :=
+  fun f a b ↦ f ⟨a, b⟩
+
+@[reflect] def myPi {A B : Type} : MyProd A B → A := fun x ↦ x.1
+@[reflect] def myPair {A B : Type} : A → B → MyProd A B := myFunc (fun x ↦ x)
+
+@[reflect] def aux1 {A B : Type} (x : A) (y : B) := myPi (myPair x y)
+@[reflect] def aux2 {A B : Type} (x : A) (y : B) := x
+
+@[reflect]
+def myPi_myPair {A B : Type} (x : A) (y : B) : Identity (aux1 x y) (aux2 x y) :=
+  Identity.refl _
+
+open SynthLean
+open Model UnstructuredUniverse Interpretation
+open CategoryTheory
+
+variable {𝒞 : Type} [Category 𝒞] [ChosenTerminal 𝒞] (s : UHomSeq 𝒞)
+  [s.PiSeq] [s.SigSeq] [s.IdSeq]
+
+def emptyInterp : Interpretation Lean.Name s where
+  ax _ _ _ := none
+
+instance : Fact ((emptyInterp s).Wf (.empty _)) := by
+  constructor; constructor; simp [emptyInterp, Axioms.empty]
+
+open Qq in
+example :
+    (emptyInterp s).interpTm aux1.reflection.wf_val =
+    (emptyInterp s).interpTm aux2.reflection.wf_val := by
+  apply interpTm_eq -- Reduce to internal judgmental equality
+  run_tac do -- Run the typechecker
+    let pf ← TypecheckerM.run <| equateWfTms
+      q(Axioms.empty Lean.Name) q([])
+      q(aux1.reflection.l) q(aux1.reflection.val) q(aux2.reflection.val) q(aux1.reflection.tp)
+    Lean.Elab.Tactic.closeMainGoal `equateTms
+      q($pf TpEnvEqCtx.nil aux1.reflection.wf_val aux2.reflection.wf_val)
diff --git a/HoTTLeanTest/unitt.lean b/HoTTLeanTest/unitt.lean
new file mode 100644
index 00000000..42b831dd
--- /dev/null
+++ b/HoTTLeanTest/unitt.lean
@@ -0,0 +1,78 @@
+import HoTTLean.Frontend.Reflect
+import HoTTLean.Model.Unstructured.Interpretation
+import HoTTLean.Groupoids.UHom
+import HoTTLean.Groupoids.Pi
+import HoTTLean.Groupoids.Sigma
+import HoTTLean.Groupoids.Id
+
+noncomputable section
+
+/-! ## Theory -/
+
+namespace UniTT
+
+@[reflect]
+axiom funext {α : Type} {β : α → Type} (f g : (a : α) → β a) :
+  (∀ a, Identity (f a) (g a)) → Identity f g
+
+@[reflect] axiom Unit : Type
+@[reflect] axiom u : Unit
+@[reflect] axiom uniq_u (u' : Unit) : Identity u' u
+
+#print u -- Prints `axiom u : Unit`
+#print u.reflection -- Prints `def u.reflection : CheckedAx (Axioms.empty.snoc Unit) := …`
+
+@[reflect]
+def uniq_fn {A : Type} (f g : A → Unit) : Identity f g := by
+  apply funext; intro; exact (uniq_u _).trans₀ (uniq_u _).symm₀
+
+/-! ## Interpretation -/
+
+open SynthLean
+open CategoryTheory MonoidalCategory GroupoidModel ChosenTerminal
+
+instance : uHomSeq.IdSeq := sorry
+
+theorem slen : univMax ≤ uHomSeq.length := by grind [uHomSeq, univMax]
+
+def Groupoid.asTy (G : Type 0) [Groupoid.{0,0} G] : 𝟭_ Ctx ⟶ uHomSeq[0].Ty :=
+  {
+    obj _ := Core.mk <| ULift.up <| Grpd.of G
+    map _ := CoreHom.mk <| Iso.refl _
+  }
+
+def sUnit : 𝟭_ Ctx ⟶ uHomSeq[0].Ty :=
+  Groupoid.asTy (Discrete _root_.Unit)
+
+def sUnit' : 𝟭_ Ctx ⟶ uHomSeq[1].Tm :=
+  uHomSeq.code (Nat.zero_lt_succ _) sUnit
+
+@[simp]
+def sUnit'_tp : sUnit' ≫ uHomSeq[1].tp = (uHomSeq.homSucc 0).wkU _ := by
+  simp [sUnit']
+
+open Model UnstructuredUniverse UHomSeq
+
+def I : Interpretation Lean.Name uHomSeq where
+  ax := fun
+    | ``Unit, 1, _ => some sUnit'
+    | _, _, _ => none
+
+theorem I_wf : I.Wf Unit.reflection.snocAxioms where
+  ax := by
+    intro _ _ Ec
+    unfold CheckedAx.snocAxioms Axioms.snoc at Ec
+    split_ifs at Ec <;> cases Ec
+    use sUnit'
+    subst_vars
+    unfold Unit.reflection
+    simp [I, Interpretation.ofType, UHomSeq.nilCObj]
+    rfl
+
+instance : Fact (I.Wf Unit.reflection.snocAxioms) := ⟨I_wf⟩
+
+example : I.interpTm Unit.reflection.wf_val = sUnit' := by
+  unfold Interpretation.interpTm Interpretation.ofTerm CheckedAx.val I Unit.reflection
+  simp only [Part.pure_eq_some, Part.get_some]
+  conv => rhs; rw [← Category.id_comp sUnit']
+  congr 1
diff --git a/HoTTLean/Frontend/Commands.lean b/attic/Frontend/Commands.lean
similarity index 95%
rename from HoTTLean/Frontend/Commands.lean
rename to attic/Frontend/Commands.lean
index 2f349ac6..b49062c6 100644
--- a/HoTTLean/Frontend/Commands.lean
+++ b/attic/Frontend/Commands.lean
@@ -17,11 +17,12 @@ def envDiff (old new : Environment) : Array ConstantInfo := Id.run do
     ret := ret.push i
   return ret
 
-/-- Find axioms used by the given constant in the given environment,
+/-- Find axioms used by the given constant in the given theory environment,
 and return them as an axiom environment.
 Assumes that all such axioms are present in the ambient environment
 as definitions of type `CheckedAx _` under the same name. -/
-def computeAxioms (thyEnv : Environment) (constNm : Name) : MetaM ((E : Q(Axioms Name)) × Q(($E).Wf)) := do
+def computeAxioms (thyEnv : Environment) (constNm : Name) :
+    MetaM ((E : Q(Axioms Name)) × Q(($E).Wf)) := do
   let (_, st) ← (CollectAxioms.collect constNm).run thyEnv |>.run {}
   let axioms := st.axioms
   -- The output includes `constNm` if it is itself an axiom.
@@ -65,7 +66,7 @@ to the Lean environment as a `CheckedAx`. -/
 def addCheckedAx (thyEnv : Environment) (ci : AxiomVal) : MetaM Unit := do
   let env ← getEnv
   let (l, T) ← withEnv thyEnv do
-    try translateAsTp ci.type |>.run env
+    try translateAsTp q(Lean.Name) ci.type |>.run env
     catch e =>
       throwError "failed to translate type{Lean.indentExpr ci.type}\nerror: {e.toMessageData}"
 
@@ -102,11 +103,11 @@ to the Lean environment as a `CheckedDef`. -/
 def addCheckedDef (thyEnv : Environment) (ci : DefinitionVal) : MetaM Unit := do
   let env ← getEnv
   let (l, T) ← withEnv thyEnv do
-    try translateAsTp ci.type |>.run env
+    try translateAsTp q(Lean.Name) ci.type |>.run env
     catch e =>
       throwError "failed to translate type{Lean.indentExpr ci.type}\nerror: {e.toMessageData}"
   let (k, t) ← withEnv thyEnv do
-    try translateAsTm ci.value |>.run env
+    try translateAsTm q(Lean.Name) ci.value |>.run env
     catch e =>
       throwError "failed to translate term{Lean.indentExpr ci.value}\nerror: {e.toMessageData}"
   if l != k then throwError "internal error: inferred level mismatch"
diff --git a/HoTTLean/Frontend/EnvExt.lean b/attic/Frontend/EnvExt.lean
similarity index 100%
rename from HoTTLean/Frontend/EnvExt.lean
rename to attic/Frontend/EnvExt.lean
diff --git a/lake-manifest.json b/lake-manifest.json
index 930c29a9..c0035dca 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -11,21 +11,21 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/sinhp/Poly",
+  {"url": "https://github.com/Vtec234/Poly",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "aedee22f07d681d845bcbe4a1fb9aa10f95c9977",
+   "rev": "c26e710a750cb9d769ee51d0b1b737f9eb437700",
    "name": "Poly",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "bump/v4.28.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32bd6c7c8ca4a4be1c71bc04df0c9cf929d04818",
+   "rev": "b8dad038b1b3a05b77d6884b15b8db03ec01dca1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8864a73bf79aad549e34eff972c606343935106d",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
+   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.77",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca",
+   "rev": "100083c18750b6a9b7553c65f6b052c0a2f6bcb4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0-rc2",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "hottlean",
diff --git a/lakefile.lean b/lakefile.lean
index 2807a875..9f484bc5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,13 +1,13 @@
 import Lake
 open Lake DSL
 
-require Poly from git "https://github.com/sinhp/Poly" @ "master"
+require Poly from git "https://github.com/Vtec234/Poly" @ "bump/v4.28.0-rc1"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.25.0-rc2"
+  "https://github.com/leanprover/doc-gen4" @ "v4.28.0-rc1"
 
 package hottlean where
   -- Settings applied to both builds and interactive editing
@@ -37,4 +37,4 @@ lean_lib HoTTLean where
   needs := #[Prelude]
 
 @[test_driver]
-lean_lib test where
+lean_lib HoTTLeanTest where
diff --git a/lean-toolchain b/lean-toolchain
index 137937a3..3e9b4e15 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.25.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.28.0-rc1
\ No newline at end of file
diff --git a/test.lean b/test.lean
deleted file mode 100644
index dc13b5c9..00000000
--- a/test.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import test.basic
-import test.import
-import test.hott0
diff --git a/test/basic.lean b/test/basic.lean
deleted file mode 100644
index 99b86d7e..00000000
--- a/test/basic.lean
+++ /dev/null
@@ -1,89 +0,0 @@
-import HoTTLean.Frontend.Commands
-
-/-! Test basic typechecker functionality. -/
-
-/-! ## Declaring theories -/
-
-declare_theory mltt
-
-declare_theory anothertt
-
-/-! ## Universes -/
-
-mltt def tp_univ : Type 1 := Type 0
-
-/-! ## Functions -/
-
-mltt def tp_pi_nondep : Type 1 := Type 0 → Type 0
-
-mltt def tm_lam_nondep : Type 0 → Type 0 := fun x => x
-
-mltt def tp_pi : Type 1 := (A : Type 0) → A → A
-
-mltt def tm_lam : (A : Type 0) → A → A := fun _ a => a
-
-mltt def tm_app : (A : Type 0) → A → (A → A) → A := fun _ a f => f a
-
-/-! ## Products -/
-
-mltt def tp_sigma : Type 1 :=
-  (A : Type) × A
-
-mltt def tp_sigma_partial : (A : Type) → (B : A → Type) → Type :=
-  @Sigma
-
-mltt def tm_pair_nondep : (_ : Type 1) × Type 1 :=
-  ⟨Type 0, Type 0⟩
-
--- Noncomputable due to Lean issue https://github.com/leanprover/lean4/issues/9692
--- FIXME: needs at least 4 universes.
--- mltt noncomputable def tm_pair : (A : Type 2) × A :=
---   ⟨Type 1, Type 0⟩
-
-mltt def tm_fst : Type 2 :=
-  { fst := Type 1, snd := Type 0 : (A : Type 2) × A }.fst
-
-mltt def tm_snd : Type 1 :=
-  { fst := Type 1, snd := Type 0 : (A : Type 2) × A }.snd
-
-/-! ## Identity types -/
-
-mltt def tp_id : Type 2 :=
-  @Identity (Type 1) Type Type
-
-mltt def tm_refl : @Identity (Type 1) Type Type :=
-  @Identity.refl (Type 1) Type
-
-mltt noncomputable def tm_idRec (A B : Type) (eq : @Identity Type A B) (a : A) : B :=
-  @Identity.rec Type A (fun T _ => T) a B eq
-
-/-! ## Definitional equalities -/
-
-mltt def defeq_el_code {A : Type} (a : A) : A :=
-  (fun (α : Type) (x : α) => x) ((fun (α : Type 1) (x : α) => x) Type A) a
-
-/-! ## Using previous definitions -/
-
-mltt def tm_refl' : tp_id := tm_refl
-
-/-! ## Adding axioms -/
-
-mltt axiom B : Type
-
-mltt axiom b : B
-
-mltt axiom C : B → Type
-
-mltt axiom c : C b
-
-/-! ## Using axioms -/
-
-mltt def Cb : Type := C b
-
-mltt noncomputable def c' : Cb := c
-
-/-! ## Using `sorry` -/
-
-/-- warning: declaration uses 'sorry' -/
-#guard_msgs in
-mltt def foo : Type := sorry
diff --git a/test/import.lean b/test/import.lean
deleted file mode 100644
index aab44aca..00000000
--- a/test/import.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-import test.basic
-
-/-! Test importing a theory. -/
-
-mltt noncomputable def tm_refl'' : tp_id := tm_refl'
-
-mltt def B'' : Type := B
diff --git a/test/unitt.lean b/test/unitt.lean
deleted file mode 100644
index 9024b7b1..00000000
--- a/test/unitt.lean
+++ /dev/null
@@ -1,76 +0,0 @@
-import HoTTLean.Frontend.Commands
-import HoTTLean.Model.Interpretation
-import HoTTLean.Groupoids.NaturalModelBase
-import HoTTLean.Groupoids.Pi
-import HoTTLean.Groupoids.Sigma
-import HoTTLean.Groupoids.Id
-
-noncomputable section
-
-/-! ## Theory -/
-
-declare_theory unitt
-
-namespace UniTT
-
-unitt axiom funext {α : Type} {β : α → Type} (f g : (a : α) → β a) :
-  (∀ a, Identity (f a) (g a)) → Identity f g
-
-unitt axiom Unit : Type
-unitt axiom u : Unit
-unitt axiom uniq_u (u' : Unit) : Identity u' u
-
-unitt #print u -- Prints `axiom u : Unit`
-#print u -- Prints `def u : CheckedAx (Axioms.empty.snoc Unit) := …`
-
-unitt def uniq_fn {A : Type} (f g : A → Unit) : Identity f g := by
-  apply funext; intro; exact (uniq_u _).trans₀ (uniq_u _).symm₀
-
-/-! ## Interpretation -/
-
-open SynthLean
-open CategoryTheory MonoidalCategory NaturalModel Universe GroupoidModel
-
-instance : uHomSeq.IdSeq := sorry
-
-theorem slen : univMax ≤ uHomSeq.length := by grind [uHomSeq, univMax]
-
-def Groupoid.asTy (G : Type 0) [Groupoid.{0,0} G] : y(𝟙_ Ctx) ⟶ uHomSeq[0].Ty :=
-  yonedaEquiv.symm <| ULift.up {
-      obj _ := Core.mk <| ULift.up <| Grpd.of G
-      map _ := CoreHom.mk <| Iso.refl _
-    }
-
-def sUnit : y(𝟙_ Ctx) ⟶ uHomSeq[0].Ty :=
-  Groupoid.asTy (Discrete _root_.Unit)
-
-def sUnit' : y(𝟙_ Ctx) ⟶ uHomSeq[1].Tm :=
-  uHomSeq.code (Nat.zero_lt_succ _) sUnit
-
-@[simp]
-def sUnit'_tp : sUnit' ≫ uHomSeq[1].tp = (uHomSeq.homSucc 0).wkU _ := by
-  simp [sUnit']
-
-def I : Universe.Interpretation Lean.Name uHomSeq where
-  ax := fun
-    | ``Unit, 1, _ => some sUnit'
-    | _, _, _ => none
-
-theorem I_wf : I.Wf slen Unit.snocAxioms where
-  ax := by
-    intro _ _ Ec
-    unfold CheckedAx.snocAxioms Axioms.snoc at Ec
-    split_ifs at Ec <;> cases Ec
-    use sUnit'
-    subst_vars
-    unfold Unit
-    simp [I, Interpretation.ofType, UHomSeq.nilCObj]
-    rfl
-
-instance : Fact (I.Wf slen Unit.snocAxioms) := ⟨I_wf⟩
-
-example : I.interpTm Unit.wf_val = sUnit' := by
-  unfold Interpretation.interpTm Interpretation.ofTerm CheckedAx.val I Unit
-  simp only [Part.pure_eq_some, Part.get_some]
-  conv => rhs; rw [← Category.id_comp sUnit']
-  congr 1; apply Limits.IsTerminal.hom_ext ChosenTerminal.isTerminal_yUnit