diff --git a/CHANGES.md b/CHANGES.md
index 4dbda127..7c91b4b7 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,4 +1,5 @@
 ## Catt
+- Improve efficiency by storing partially checked terms
 - Computation of cylinder compositions as a builtin
 - Computation of cone compositions as a builtin
 
diff --git a/coq_plugin/src/export.ml b/coq_plugin/src/export.ml
index fc84bf9a..d1ed6efc 100644
--- a/coq_plugin/src/export.ml
+++ b/coq_plugin/src/export.ml
@@ -20,6 +20,12 @@ let rec catt_var_to_coq_name v =
   | Var.Plus v -> catt_var_to_coq_name v ^ "_plus"
   | Var.Bridge v -> catt_var_to_coq_name v ^ "_bridge"
 
+let counter = ref 0
+
+let anon () =
+  incr counter;
+  Printf.sprintf "anonymous_term_%d" !counter
+
 let c_Q env sigma =
   let gr = Coqlib.lib_ref "core.eq.type" in
   Evd.fresh_global env sigma gr
@@ -280,7 +286,11 @@ end = struct
     match retrieve_lambda value sigma with
     | Some res -> res
     | None ->
-        let name = clean_name (Tm.full_name tm) in
+        let name =
+          match Tm.full_name tm with
+          | Some name -> clean_name name
+          | None -> anon ()
+        in
         let ctx = Tm.ctx tm in
         let tm = Tm.develop tm in
         let env, sigma, tm =
diff --git a/lib/builtin.ml b/lib/builtin.ml
index 52a55d17..8d0f3c4a 100644
--- a/lib/builtin.ml
+++ b/lib/builtin.ml
@@ -16,33 +16,39 @@ module Memo = struct
     check_coh (Br []) (Arr (Obj, Var (Db 0), Var (Db 0))) ("builtin_id", 0, [])
 end
 
-let rec ps_comp i =
-  match i with
-  | i when i <= 0 -> Error.fatal "builtin composition with less than 0 argument"
-  | i when i = 1 -> Br [ Br [] ]
-  | i -> ( match ps_comp (i - 1) with Br l -> Br (Br [] :: l))
+module Comp = struct
+  let tdb i = Var (Var.Db i)
+  let tree i = Br (List.init i (fun _ -> Br []))
+  let x i = if i = 0 then (tdb 0, Obj) else (tdb ((2 * i) - 1), Obj)
+  let f i = (tdb (2 * i), Arr (Obj, fst @@ x (i - 1), fst @@ x i))
 
-let comp_n arity =
-  let build_comp i =
-    let ps = ps_comp i in
-    let pp_data = (Printf.sprintf "builtin_comp%i" arity, 0, []) in
-    Coh.check_noninv ps (Var (Db 0)) (Var (Db 0)) pp_data
-  in
-  Memo.find arity build_comp
+  let comp_n arity =
+    let build_comp i =
+      let ps = tree i in
+      let pp_data = (Printf.sprintf "builtin_comp%i" arity, 0, []) in
+      Coh.check_noninv ps (fst (x 0)) (fst (x 0)) pp_data
+    in
+    Memo.find arity build_comp
 
-let arity_comp s expl =
-  let n = List.length s in
-  if expl || !Settings.explicit_substitutions then (n - 1) / 2 else n
+  let arity_comp s expl =
+    let n = List.length s in
+    if expl || !Settings.explicit_substitutions then (n - 1) / 2 else n
 
-let comp s expl =
-  let arity = arity_comp s expl in
-  comp_n arity
+  let comp s expl =
+    let arity = arity_comp s expl in
+    comp_n arity
 
-let bcomp x y f z g =
-  let comp = comp_n 2 in
-  let sub = [ (g, true); (z, false); (f, true); (y, false); (x, false) ] in
-  Coh (comp, sub)
+  let bcomp x y f z g =
+    let comp = comp_n 2 in
+    let sub = [ (g, true); (z, false); (f, true); (y, false); (x, false) ] in
+    Coh (comp, sub)
+end
 
+let ps_comp = Comp.tree
+let comp_n = Comp.comp_n
+let arity_comp = Comp.arity_comp
+let comp = Comp.comp
+let bcomp = Comp.bcomp
 let id = Memo.id
 
 let id_all_max ps =
@@ -84,16 +90,14 @@ let unbiased_unitor ps t =
     let coh = Coh.check_noninv ps t t ("endo", 0, []) in
     Coh (coh, id_all_max ps)
   in
-  let a =
-    UnnamedTm.ty (check_unnamed_term (Ctx.check (Unchecked.ps_to_ctx bdry)) t)
-  in
+  let a = Tm.ty (check_term (Ctx.check (Unchecked.ps_to_ctx bdry)) t) in
   let da = Unchecked.dim_ty a in
   let sub_base = Unchecked.ty_to_sub_ps a in
   let tgt = Coh (Suspension.coh (Some da) (id ()), (t, true) :: sub_base) in
   Coh.check_inv bdry src tgt ("unbiased_unitor", 0, [])
 
 let tdb i = Var (Var.Db i)
-let wcomp = ref (fun _ -> Error.fatal "Uninitialised forward reference")
+let wcomp = ref (fun _ -> Error.fatal "Uninitialised forward reference wcomp")
 
 (*
   (a *_n b) *_0 g -> (a *_0 g) *_n (b *_0 g)
diff --git a/lib/builtin.mli b/lib/builtin.mli
index 660ccb7f..ada2ed3e 100644
--- a/lib/builtin.mli
+++ b/lib/builtin.mli
@@ -3,6 +3,12 @@ open Common
 open Kernel
 open Unchecked_types.Unchecked_types(Coh)(Tm)
 
+module Comp : sig
+  val tree : int -> ps
+  val x : int -> constr
+  val f : int -> constr
+end
+
 val wcomp : (tm * ty -> int -> tm * ty -> tm * ty) ref
 val ps_comp : int -> ps
 val comp_n : int -> Coh.t
diff --git a/lib/command.ml b/lib/command.ml
index 7779c19d..8863d1b3 100644
--- a/lib/command.ml
+++ b/lib/command.ml
@@ -47,8 +47,8 @@ let check l e t =
         Some ty
   in
   let c = Kernel.Ctx.check c in
-  let tm = Kernel.check_unnamed_term c ?ty e in
-  let ty = Kernel.UnnamedTm.ty tm in
+  let tm = Kernel.check_term c ?ty e in
+  let ty = Kernel.Tm.ty tm in
   (e, ty)
 
 let exec_check_builtin b =
diff --git a/lib/cones.ml b/lib/cones.ml
index 9a7e5ba2..4177cf5f 100644
--- a/lib/cones.ml
+++ b/lib/cones.ml
@@ -208,7 +208,7 @@ module Codim1 = struct
     in
     let tm, _ = wcomp tm_1 1 tm_2 in
     let name = Printf.sprintf "builtin_conecomp(%d,%d,%d)" 2 1 2 in
-    check_term (Ctx.check ctx) (name, 0, []) tm
+    check_term (Ctx.check ctx) ~name:(name, 0, []) tm
 
   let intch n =
     let with_type ctx x = (Var x, fst (List.assoc x ctx)) in
@@ -263,7 +263,7 @@ module Codim1 = struct
               (Suspension.sub (Some 1)
                  (Opposite.sub (Cone.bdry_left (n - 1) (n - 2)) op_data))
           in
-          check_term (Ctx.check ctx_comp) (name, 0, []) (App (comp, sub))
+          check_term (Ctx.check ctx_comp) ~name:(name, 0, []) (App (comp, sub))
         in
         let intch = intch n in
         let socomp = (Tm.develop suspopcomp, Tm.ty suspopcomp) in
@@ -271,7 +271,7 @@ module Codim1 = struct
           if n mod 2 = 0 then wcomp socomp (n - 1) intch
           else wcomp intch (n - 1) socomp
         in
-        check_term (Ctx.check ctx_comp) (name, 0, []) tm
+        check_term (Ctx.check ctx_comp) ~name:(name, 0, []) tm
 end
 
 module Composition = struct
@@ -369,7 +369,7 @@ module Composition = struct
         let ctx, _, _ = Unchecked.db_levels ctx in
         let tm = Unchecked.tm_apply_sub (Tm.develop tm) names in
         let name = Printf.sprintf "builtin_conecomp(%d,%d,%d)" n k m in
-        let res = check_term (Ctx.check ctx) (name, 0, []) tm in
+        let res = check_term (Ctx.check ctx) ~name:(name, 0, []) tm in
         Hashtbl.add tbl (n, m, k) res;
         res
 end
diff --git a/lib/construct.ml b/lib/construct.ml
index d08bf225..206a4eba 100644
--- a/lib/construct.ml
+++ b/lib/construct.ml
@@ -2,7 +2,11 @@ open Common
 open Kernel
 open Unchecked_types.Unchecked_types (Coh) (Tm)
 
-type constr = tm * ty
+let to_tm (tm, _) = tm
+let to_ty (_, ty) = ty
+let characteristic_sub_ps (tm, ty) = (tm, true) :: Unchecked.ty_to_sub_ps ty
+let dim (_, ty) = Unchecked.dim_ty ty
+let arr (tm1, ty1) (tm2, _) = Arr (ty1, tm1, tm2)
 
 let rec bdry n (t, ty) =
   match (n, ty) with
@@ -11,7 +15,52 @@ let rec bdry n (t, ty) =
   | _, Arr (b, s, _) -> bdry (n - 1) (s, b)
   | _, _ -> assert false
 
-let _src n t = fst (bdry n t)
+let coh_app coh tms =
+  let elaborate ps tms =
+    let rec aux_list psl tms =
+      match (psl, tms) with
+      | [], t :: tms -> ([ (fst t, true) ], tms, snd t)
+      | [ ps ], tms -> (
+          let s, tms, ty = aux ps tms in
+          match ty with
+          | Arr (ty, src, tgt) -> (s @ [ (tgt, false); (src, false) ], tms, ty)
+          | _ -> assert false)
+      | ps :: psl, tms -> (
+          let s, tms, _ = aux_list psl tms in
+          let sub_ps, tms, ty = aux ps tms in
+          match ty with
+          | Arr (ty, _, tgt) -> (sub_ps @ ((tgt, false) :: s), tms, ty)
+          | _ -> assert false)
+      | _ -> assert false
+    and aux ps tms = match ps with Br l -> aux_list l tms in
+    let sub_ps, _, _ = aux ps tms in
+    sub_ps
+  in
+  let ps, ty, _ = Coh.forget coh in
+  let sub = elaborate ps tms in
+  (Coh (coh, sub), Unchecked.ty_apply_sub_ps ty sub)
+
+let of_coh coh =
+  let ps, ty, _ = Coh.forget coh in
+  let id = Unchecked.identity_ps ps in
+  (Coh (coh, id), ty)
+
+let make_sub ctx list =
+  List.map2 (fun (x, (_, b)) t -> (x, (fst t, b))) ctx list
+
+let tm_app_sub tm sub =
+  let ty = Tm.ty tm in
+  (App (tm, sub), Unchecked.ty_apply_sub ty sub)
+
+let of_tm tm =
+  let c = Tm.ctx tm in
+  tm_app_sub tm (Unchecked.identity c)
+
+let tm_app tm sub =
+  let sub = make_sub (Tm.ctx tm) sub in
+  tm_app_sub tm sub
+
+let src n t = fst (bdry n t)
 let tgt n t = snd (bdry n t)
 let wcomp = Functorialisation.wcomp
 let () = Builtin.wcomp := wcomp
@@ -84,3 +133,103 @@ let intch_comp_mn a b c =
 
 let opposite (t, ty) op_data = (Opposite.tm t op_data, Opposite.ty ty op_data)
 let inv (t, ty) = (Inverse.compute_inverse t, Inverse.ty ty)
+
+let id constr =
+  let d = dim constr in
+  ( Coh (Suspension.coh (Some d) (Builtin.id ()), characteristic_sub_ps constr),
+    arr constr constr )
+
+let rec id_n n constr =
+  match n with
+  | 0 -> constr
+  | n when n > 0 -> id (id_n (n - 1) constr)
+  | _ -> Error.fatal "call to id_n with a negative argument"
+
+let apply_sub (tm, ty) sigma =
+  (Unchecked.tm_apply_sub tm sigma, Unchecked.ty_apply_sub ty sigma)
+
+let apply_sub_ps (tm, ty) sigma =
+  (Unchecked.tm_apply_sub_ps tm sigma, Unchecked.ty_apply_sub_ps ty sigma)
+
+let rename (tm, ty) sigma =
+  (Unchecked.tm_rename tm sigma, Unchecked.ty_rename ty sigma)
+
+let inverse (tm, ty) = (Inverse.compute_inverse tm, Inverse.ty ty)
+let suspend i (tm, ty) = (Suspension.tm (Some i) tm, Suspension.ty (Some i) ty)
+
+let functorialise (tm, ty) vars =
+  (Functorialisation.tm_one_step_tm tm vars, Functorialisation.ty ty vars tm)
+
+(* TODO: more optimised implementation of this function *)
+let comp_n constrs =
+  let constrs_rev = List.rev constrs in
+  let first = function [] -> assert false | h :: _ -> h in
+  let rec glue_subs = function
+    | [ c ] -> characteristic_sub_ps c
+    | c :: constrs ->
+        (to_tm c, true) :: (to_tm (tgt 1 c), false) :: glue_subs constrs
+    | [] -> assert false
+  in
+  let l = List.length constrs in
+  let c = first constrs in
+  let d = dim c in
+  ( Coh (Suspension.coh (Some (d - 1)) (Builtin.comp_n l), glue_subs constrs_rev),
+    arr (src 1 c) (tgt 1 (first constrs_rev)) )
+
+let comp c1 c2 = comp_n [ c1; c2 ]
+let comp3 c1 c2 c3 = comp_n [ c1; c2; c3 ]
+let op dims (tm, ty) = (Opposite.tm tm dims, Opposite.ty ty dims)
+
+let drop n xs =
+  let rec aux xs counter =
+    match xs with
+    | [] -> []
+    | h :: tl -> if counter > 0 then h :: aux tl (counter - 1) else []
+  in
+  aux xs (List.length xs - n)
+
+let characteristic_sub_ps_composite constrs =
+  let rec aux = function
+    | [] -> assert false
+    | [ constr ] -> characteristic_sub_ps constr
+    | constr :: tail ->
+        [ (to_tm constr, true); (to_tm @@ tgt 1 constr, false) ] @ aux tail
+  in
+  aux @@ List.rev constrs
+
+let glue_subs_along k subs =
+  let rec aux = function
+    | [] -> assert false
+    | [ sub ] -> sub
+    | sub :: subs -> drop ((2 * k) + 1) sub @ aux subs
+  in
+  aux @@ List.rev subs
+
+let rec whisk_n n dims =
+  let l = List.length dims in
+  let comp = Builtin.comp_n l in
+  let func_data =
+    List.rev
+    @@ List.mapi (fun idx dim -> (Var.Db (2 * (idx + 1)), dim - 1)) dims
+  in
+  let whisk = Functorialisation.coh_successively comp func_data in
+  Suspension.checked_tm (Some n) whisk
+
+and wcomp_n k constrs =
+  let dims_adjusted = List.map (fun c -> dim c - k) constrs in
+  let whisk = whisk_n k dims_adjusted in
+  let whisk_sub_ps =
+    glue_subs_along k (List.map characteristic_sub_ps constrs)
+  in
+  let whisk_sub = Unchecked.sub_ps_to_sub whisk_sub_ps in
+  (App (whisk, whisk_sub), Unchecked.ty_apply_sub_ps (Tm.ty whisk) whisk_sub_ps)
+
+let witness constr =
+  let tm = to_tm constr in
+  let d = dim constr in
+  let ty =
+    arr (wcomp constr (d - 1) (inverse constr)) (id_n 1 (src 1 constr))
+  in
+  (Inverse.compute_witness tm, ty)
+
+let develop (tm, ty) = (Unchecked.develop_tm tm, Unchecked.develop_ty ty)
diff --git a/lib/construct.mli b/lib/construct.mli
index f1bd97c5..d7db2a2b 100644
--- a/lib/construct.mli
+++ b/lib/construct.mli
@@ -2,11 +2,40 @@ open Common
 open Kernel
 open Unchecked_types.Unchecked_types(Coh)(Tm)
 
-type constr = tm * ty
-
+val to_tm : constr -> tm
+val to_ty : constr -> ty
+val arr : constr -> constr -> ty
+val characteristic_sub_ps : constr -> sub_ps
+val coh_app : Coh.t -> constr list -> constr
+val of_coh : Coh.t -> constr
+val make_sub : ctx -> constr list -> sub
+val tm_app_sub : Tm.t -> sub -> constr
+val tm_app : Tm.t -> constr list -> constr
+val of_tm : Tm.t -> constr
 val wcomp : constr -> int -> constr -> constr
 val wcomp3 : constr -> int -> constr -> int -> constr -> constr
 val intch_comp_nm : constr -> constr -> constr -> constr
 val intch_comp_mn : constr -> constr -> constr -> constr
 val opposite : constr -> op_data -> constr
 val inv : constr -> constr
+val functorialise : constr -> Var.t list -> constr
+val id : constr -> constr
+val id_n : int -> constr -> constr
+val dim : constr -> int
+val apply_sub : constr -> sub -> constr
+val apply_sub_ps : constr -> sub_ps -> constr
+val rename : constr -> (Var.t * tm) list -> constr
+val bdry : int -> constr -> constr * constr
+val src : int -> constr -> constr
+val tgt : int -> constr -> constr
+val inverse : constr -> constr
+val suspend : int -> constr -> constr
+val comp_n : constr list -> constr
+val comp : constr -> constr -> constr
+val comp3 : constr -> constr -> constr -> constr
+val op : int list -> constr -> constr
+val witness : constr -> constr
+val glue_subs_along : int -> 'a list list -> 'a list
+val wcomp_n : int -> constr list -> constr
+val characteristic_sub_ps_composite : constr list -> sub_ps
+val develop : constr -> constr
diff --git a/lib/cubical_composite.ml b/lib/cubical_composite.ml
index 406c582a..73e94890 100644
--- a/lib/cubical_composite.ml
+++ b/lib/cubical_composite.ml
@@ -412,7 +412,7 @@ let coh_depth1 coh l =
   in
   let comp = Suspension.coh (Some d) (Builtin.comp_n 3) in
   let ctx = F.ctx (Unchecked.ps_to_ctx ps) l in
-  let pp_data = F.pp_data l pp_data in
-  check_term (Ctx.check ctx) pp_data (Coh (comp, comp_sub_ps))
+  let name = F.pp_data l pp_data in
+  check_term (Ctx.check ctx) ~name (Coh (comp, comp_sub_ps))
 
 let init () = F.coh_depth1 := coh_depth1
diff --git a/lib/cylinders.ml b/lib/cylinders.ml
index a6614b79..d7428f28 100644
--- a/lib/cylinders.ml
+++ b/lib/cylinders.ml
@@ -258,7 +258,7 @@ module Codim1 = struct
     let c = Tm.ctx cubcomp in
     let sub = List.map2 (fun (x, _) y -> (x, y)) c sub_ps in
     let tm = App (cubcomp, sub) in
-    check_term (Ctx.check (ctx 2)) ("cylcomp(2,1,2)", 0, []) tm
+    check_term (Ctx.check (ctx 2)) ~name:("cylcomp(2,1,2)", 0, []) tm
 
   let intch n =
     let with_type ctx x = (Var x, fst (List.assoc x ctx)) in
@@ -320,14 +320,14 @@ module Codim1 = struct
               (Suspension.sub (Some 1) (Cylinder.bdry_left (n - 1) (n - 2)))
           in
           Io.debug "substitution:%s" (Unchecked.sub_to_string_debug sub);
-          check_term (Ctx.check ctx_comp) (name, 0, []) (App (comp, sub))
+          check_term (Ctx.check ctx_comp) ~name:(name, 0, []) (App (comp, sub))
         in
         let intch_lower, intch_upper = intch n in
         let scomp = (Tm.develop suspcomp, Tm.ty suspcomp) in
         let tm, _ =
           Construct.wcomp3 intch_lower (n - 1) scomp (n - 1) intch_upper
         in
-        check_term (Ctx.check ctx_comp) (name, 0, []) tm
+        check_term (Ctx.check ctx_comp) ~name:(name, 0, []) tm
 end
 
 module Composition = struct
@@ -467,7 +467,7 @@ module Composition = struct
         let ctx, _, _ = Unchecked.db_levels ctx in
         let tm = Unchecked.tm_apply_sub (Tm.develop tm) names in
         let name = Printf.sprintf "builtin_conecomp(%d,%d,%d)" n k m in
-        let res = check_term (Ctx.check ctx) (name, 0, []) tm in
+        let res = check_term (Ctx.check ctx) ~name:(name, 0, []) tm in
         Hashtbl.add tbl (n, m, k) res;
         res
 end
@@ -602,7 +602,9 @@ module Stacking = struct
           in
           let c = Tm.ctx tm in
           let sub = List.map2 (fun (x, _) y -> (x, y)) c sub_ps in
-          check_term (Ctx.check ctx) ("builtin_cylstack", 0, []) (App (tm, sub))
+          check_term (Ctx.check ctx)
+            ~name:("builtin_cylstack", 0, [])
+            (App (tm, sub))
       | n ->
           let _, upper_incl = ctx (n - 1) in
           let lb = Cylinder.base_lower (n - 1) in
diff --git a/lib/environment.ml b/lib/environment.ml
index f9c15ff8..6a7d8665 100644
--- a/lib/environment.ml
+++ b/lib/environment.ml
@@ -28,7 +28,7 @@ let value_ctx v =
   | Tm t -> Tm.ctx t
 
 let value_to_string v =
-  match v with Coh c -> Coh.to_string c | Tm t -> Tm.name t
+  match v with Coh c -> Coh.to_string c | Tm t -> Tm.to_string t
 
 type v = { value : value; dim_input : int; dim_output : int }
 type t = (Var.t, v) Hashtbl.t
@@ -40,7 +40,7 @@ let add_let v c ?ty t =
   try
     let pp_data = (Var.to_string v, 0, []) in
     let kc = Kernel.Ctx.check c in
-    let tm = Kernel.check_term kc pp_data ?ty t in
+    let tm = Kernel.check_term kc ?ty ~name:pp_data t in
     let ty = Kernel.(Ty.forget (Tm.typ tm)) in
     let dim_input = Unchecked.dim_ctx c in
     let dim_output = Unchecked.dim_ty ty in
diff --git a/lib/functorialisation.ml b/lib/functorialisation.ml
index a920df00..b2363de5 100644
--- a/lib/functorialisation.ml
+++ b/lib/functorialisation.ml
@@ -6,7 +6,8 @@ exception FunctorialiseMeta
 exception NotClosed
 exception Unsupported
 
-let coh_depth1 = ref (fun _ -> Error.fatal "Uninitialised forward reference")
+let coh_depth1 =
+  ref (fun _ -> Error.fatal "Uninitialised forward reference coh_depth1")
 
 module Memo = struct
   let tbl_whisk = Hashtbl.create 97
@@ -217,9 +218,9 @@ and coh coh l =
 and coh_successively c l =
   let l, next = next_round l in
   if l = [] then
-    let ps, _, pp_data = Coh.forget c in
+    let ps, _, name = Coh.forget c in
     let id = Unchecked.identity_ps ps in
-    check_term (Ctx.check (Unchecked.ps_to_ctx ps)) pp_data (Coh (c, id))
+    check_term (Ctx.check (Unchecked.ps_to_ctx ps)) ~name (Coh (c, id))
   else
     let cohf, names = coh c l in
     let next =
@@ -318,7 +319,7 @@ let rec sub s l =
       | _ -> assert false)
 
 (* Functorialisation once with respect to every maximal argument *)
-let coh_all c =
+let coh_all_depth0 c =
   let ps, _, _ = Coh.forget c in
   let ct = Unchecked.ps_to_ctx ps in
   let d = Unchecked.dim_ps ps in
@@ -329,9 +330,17 @@ let coh_all c =
   in
   coh_depth0 c l
 
+(* Functorialisation once with respect to every maximal argument *)
+let coh_all c =
+  let ps, _, _ = Coh.forget c in
+  let l = List.map fst (Unchecked.ps_to_ctx ps) in
+  coh c l
+
 (* Functorialisation a term: exposed function *)
 let tm t l =
-  report_errors (fun _ -> tm_successively t l) (lazy ("term: " ^ Tm.name t))
+  report_errors
+    (fun _ -> tm_successively t l)
+    (lazy ("term: " ^ Tm.to_string t))
 
 let ps p l =
   let c = ctx (Unchecked.ps_to_ctx p) l in
diff --git a/lib/functorialisation.mli b/lib/functorialisation.mli
index d3e35cf6..fca2ed0c 100644
--- a/lib/functorialisation.mli
+++ b/lib/functorialisation.mli
@@ -8,7 +8,8 @@ val tgt_renaming : Var.t list -> (Var.t * tm) list
 val coh : Coh.t -> Var.t list -> Tm.t
 val coh_successively : Coh.t -> (Var.t * int) list -> Tm.t
 val coh_depth0 : Coh.t -> Var.t list -> Coh.t
-val coh_all : Coh.t -> Coh.t
+val coh_all_depth0 : Coh.t -> Coh.t
+val coh_all : Coh.t -> Tm.t
 val tm_one_step_tm : tm -> Var.t list -> tm
 val ty : ty -> Var.t list -> tm -> ty
 val tm : Tm.t -> (Var.t * int) list -> Tm.t
diff --git a/lib/inverse.ml b/lib/inverse.ml
index e24bd0d1..ed5f223d 100644
--- a/lib/inverse.ml
+++ b/lib/inverse.ml
@@ -135,7 +135,7 @@ and cancel_all_linear_comp t =
         in
         Unchecked.wedge_sub_ps_bp lsubs
   in
-  Coh (Functorialisation.coh_all c, compute_sub 0 ps sub Obj)
+  Coh (Functorialisation.coh_all_depth0 c, compute_sub 0 ps sub Obj)
 
 and compute_witness t =
   match t with
@@ -244,3 +244,11 @@ let compute_witness t =
     Error.inversion
       ("term: " ^ Unchecked.tm_to_string t)
       (Printf.sprintf "term %s is not invertible" s)
+
+let inverse t =
+  fst
+    (Tm.apply
+       (fun x -> x)
+       compute_inverse
+       (fun (n, s, f) -> (Printf.sprintf "I(%s)" n, s, f))
+       t)
diff --git a/lib/inverse.mli b/lib/inverse.mli
index ad990648..a6158c3a 100644
--- a/lib/inverse.mli
+++ b/lib/inverse.mli
@@ -4,3 +4,4 @@ open Unchecked_types.Unchecked_types(Coh)(Tm)
 val ty : ty -> ty
 val compute_inverse : tm -> tm
 val compute_witness : tm -> tm
+val inverse : Tm.t -> Tm.t
diff --git a/lib/kernel.ml b/lib/kernel.ml
index ccc79f36..9f4a0639 100644
--- a/lib/kernel.ml
+++ b/lib/kernel.ml
@@ -20,7 +20,7 @@ module rec Sub : sig
   val tgt : t -> Ctx.t
 end = struct
   type t = {
-    list : UnnamedTm.t list;
+    list : Tm.t list;
     src : Ctx.t;
     tgt : Ctx.t;
     unchecked : Unchecked_types(Coh)(Tm).sub;
@@ -34,7 +34,7 @@ end = struct
   module Types = Unchecked_types (Coh) (Tm)
 
   let tbl : (Ctx.t * PS.t * Types.sub_ps, Sub.t) Hashtbl.t = Hashtbl.create 7829
-  let free_vars s = List.concat (List.map UnnamedTm.free_vars s.list)
+  let free_vars s = List.concat (List.map Tm.free_vars s.list)
 
   let check src s tgt =
     Io.info ~v:5
@@ -56,8 +56,8 @@ end = struct
         | (x1, _) :: _, (x2, _) :: _ when x1 <> x2 -> raise sub_exn
         | (_, (t, _)) :: s, (_, a) :: _ ->
             let sub = aux src s (Ctx.tail tgt) in
-            let t = UnnamedTm.check src t in
-            Ty.check_equal (UnnamedTm.typ t) (Ty.apply_sub a sub);
+            let t = Tm.check src t in
+            Ty.check_equal (Tm.typ t) (Ty.apply_sub a sub);
             t :: sub.list
       in
       { list = expr s tgt; src; tgt; unchecked = s }
@@ -203,7 +203,7 @@ end = struct
     | PDrop ps ->
         let _, tf = marker ps in
         let v = try Ty.target tf with IsObj -> raise Invalid in
-        let y = try UnnamedTm.to_var v with IsCoh -> raise Invalid in
+        let y = try Tm.to_var v with IsCoh -> raise Invalid in
         let t =
           let rec aux = function
             | PNil (x, t) ->
@@ -237,8 +237,7 @@ end = struct
               try Ty.retrieve_arrow tf with IsObj -> raise Invalid
             in
             let fx, fy =
-              try (UnnamedTm.to_var u, UnnamedTm.to_var v)
-              with IsCoh -> raise Invalid
+              try (Tm.to_var u, Tm.to_var v) with IsCoh -> raise Invalid
             in
             if y <> fy then raise Invalid;
             let x, _ = marker ps in
@@ -314,14 +313,14 @@ and Ty : sig
   val is_full : t -> bool
   val is_obj : t -> bool
   val check_equal : t -> t -> unit
-  val morphism : UnnamedTm.t -> UnnamedTm.t -> Ty.t
+  val morphism : Tm.t -> Tm.t -> Ty.t
   val forget : t -> Unchecked_types(Coh)(Tm).ty
   val check : Ctx.t -> Unchecked_types(Coh)(Tm).ty -> t
   val apply_sub : t -> Sub.t -> t
-  val retrieve_arrow : t -> t * UnnamedTm.t * UnnamedTm.t
+  val retrieve_arrow : t -> t * Tm.t * Tm.t
   val under_type : t -> t
-  val source : t -> UnnamedTm.t
-  val target : t -> UnnamedTm.t
+  val source : t -> Tm.t
+  val target : t -> Tm.t
   val ctx : t -> Ctx.t
   val dim : t -> int
 end = struct
@@ -330,7 +329,7 @@ end = struct
   module Types = Unchecked_types (Coh) (Tm)
 
   (** A type exepression. *)
-  type expr = Obj | Arr of t * UnnamedTm.t * UnnamedTm.t
+  type expr = Obj | Arr of t * Tm.t * Tm.t
 
   and t = { c : Ctx.t; e : expr; unchecked : Types.ty }
 
@@ -357,8 +356,8 @@ end = struct
           | Obj -> Obj
           | Arr (a, u, v) ->
               let a = check c a in
-              let u = UnnamedTm.check c ~ty:a u in
-              let v = UnnamedTm.check c ~ty:a v in
+              let u = Tm.check c ~ty:a u in
+              let v = Tm.check c ~ty:a v in
               Arr (a, u, v)
           | Meta_ty _ -> raise MetaVariable
         in
@@ -371,8 +370,7 @@ end = struct
     match ty.e with
     | Obj -> []
     | Arr (t, u, v) ->
-        List.unions
-          [ free_vars t; UnnamedTm.free_vars u; UnnamedTm.free_vars v ]
+        List.unions [ free_vars t; Tm.free_vars u; Tm.free_vars v ]
 
   let is_full t = List.included (Ctx.domain t.c) (free_vars t)
   let forget t = t.unchecked
@@ -384,13 +382,13 @@ end = struct
     Unchecked.check_equal_ty (forget ty1) (forget ty2)
 
   let morphism t1 t2 =
-    let a1 = UnnamedTm.typ t1 in
-    let a2 = UnnamedTm.typ t2 in
+    let a1 = Tm.typ t1 in
+    let a2 = Tm.typ t2 in
     check_equal a1 a2;
     {
       c = a1.c;
       e = Arr (a1, t1, t2);
-      unchecked = Arr (forget a1, UnnamedTm.forget t1, UnnamedTm.forget t2);
+      unchecked = Arr (forget a1, Tm.forget t1, Tm.forget t2);
     }
 
   let apply_sub t s =
@@ -402,23 +400,48 @@ end = struct
 end
 
 (** Operations on terms. *)
-and UnnamedTm : sig
+and Tm : sig
   type t
 
+  (* Data extraction *)
   val to_var : t -> Var.t
   val typ : t -> Ty.t
   val ty : t -> Unchecked_types(Coh)(Tm).ty
+  val bdry : t -> t * t
+  val ctx : t -> Unchecked_types(Coh)(Tm).ctx
+  val forget : t -> Unchecked_types(Coh)(Tm).tm
+  val constr : t -> Unchecked_types(Coh)(Tm).constr
+  val name : t -> string option
+  val full_name : t -> string option
+  val func_data : t -> (Var.t * int) list list option
+  val pp_data : t -> pp_data option
+  val to_string : t -> string
+
+  (* Variable uses *)
   val free_vars : t -> Var.t list
   val is_full : t -> bool
-  val forget : t -> Unchecked_types(Coh)(Tm).tm
-  val check : Ctx.t -> ?ty:Ty.t -> Unchecked_types(Coh)(Tm).tm -> t
+
+  (* Production of terms *)
+  val of_coh : Coh.t -> t
+
+  val check :
+    Ctx.t -> ?ty:Ty.t -> ?name:pp_data -> Unchecked_types(Coh)(Tm).tm -> t
+
   val apply_sub : t -> Sub.t -> t
   val preimage : t -> Sub.t -> t
   val develop : t -> Unchecked_types(Coh)(Tm).tm
+
+  val apply :
+    (Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
+    (Unchecked_types(Coh)(Tm).tm -> Unchecked_types(Coh)(Tm).tm) ->
+    (pp_data -> pp_data) ->
+    t ->
+    t * Unchecked_types(Coh)(Tm).sub
 end = struct
   open Unchecked (Coh) (Tm)
   module Unchecked = Make (Coh) (Tm)
   module Types = Unchecked_types (Coh) (Tm)
+  module Display_maps = Unchecked.Display_maps
 
   type expr = Var of Var.t | Coh of Coh.t * Sub.t | App of Tm.t * Sub.t
 
@@ -427,11 +450,14 @@ end = struct
     e : expr;
     unchecked : Types.tm;
     mutable developped : Types.tm option;
+    name : pp_data option;
   }
 
   let typ t = t.ty
   let ty t = Ty.forget t.ty
-  let tbl : (Ctx.t * Types.tm, UnnamedTm.t) Hashtbl.t = Hashtbl.create 7829
+  let tbl : (Ctx.t * Types.tm, Tm.t) Hashtbl.t = Hashtbl.create 7829
+
+  (* TODO: this is incorrect: an applied term can be a variable *)
   let to_var tm = match tm.e with Var v -> v | Coh _ | App _ -> raise IsCoh
 
   let free_vars tm =
@@ -442,8 +468,9 @@ end = struct
 
   let is_full tm = List.included (Ctx.domain (Ty.ctx tm.ty)) (free_vars tm)
   let forget tm = tm.unchecked
+  let constr tm = (forget tm, ty tm)
 
-  let check c ?ty t =
+  let check c ?ty ?name t =
     Io.info ~v:5
       (lazy
         (Printf.sprintf "building kernel term %s in context %s"
@@ -455,19 +482,19 @@ end = struct
           match t with
           | Var x ->
               let e, ty = (Var x, Ty.check c (Ty.forget (Ctx.ty_var c x))) in
-              { ty; e; unchecked = t; developped = Some t }
+              { ty; e; unchecked = t; developped = Some t; name }
           | Meta_tm _ -> raise MetaVariable
           | Coh (coh, s) ->
               let sub = Sub.check_to_ps c s (Coh.ps coh) in
               let e, ty = (Coh (coh, sub), Ty.apply_sub (Coh.ty coh) sub) in
-              let tm = { ty; e; unchecked = t; developped = Some t } in
+              let tm = { ty; e; unchecked = t; developped = Some t; name } in
               Hashtbl.add tbl (c, t) tm;
               tm
           | App (u, s) ->
               let ty = Tm.typ u in
               let sub = Sub.check c s (Ty.ctx ty) in
               let e, ty = (App (u, sub), Ty.apply_sub ty sub) in
-              let tm = { ty; e; unchecked = t; developped = None } in
+              let tm = { ty; e; unchecked = t; developped = None; name } in
               Hashtbl.add tbl (c, t) tm;
               tm)
     in
@@ -504,69 +531,38 @@ end = struct
     let c = Sub.tgt sub in
     let t = Unchecked.tm_sub_preimage (forget t) (Sub.forget sub) in
     check c t
-end
-
-(** Operations on terms. *)
-and Tm : sig
-  type t
-
-  val typ : t -> Ty.t
-  val ty : t -> Unchecked_types(Coh)(Tm).ty
-  val ctx : t -> Unchecked_types(Coh)(Tm).ctx
-  val of_coh : Coh.t -> t
-  val check : Ctx.t -> ?ty:Ty.t -> pp_data -> Unchecked_types(Coh)(Tm).tm -> t
-  val name : t -> string
-  val full_name : t -> string
-  val func_data : t -> (Var.t * int) list list
-  val pp_data : t -> pp_data
-  val develop : t -> Unchecked_types(Coh)(Tm).tm
 
-  val apply :
-    (Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
-    (Unchecked_types(Coh)(Tm).tm -> Unchecked_types(Coh)(Tm).tm) ->
-    (pp_data -> pp_data) ->
-    t ->
-    t * Unchecked_types(Coh)(Tm).sub
-end = struct
-  open Unchecked (Coh) (Tm)
-  module Unchecked = Make (Coh) (Tm)
-  module Types = Unchecked_types (Coh) (Tm)
-  module Display_maps = Unchecked.Display_maps
+  let apply fun_ctx fun_tm fun_pp_data tm =
+    let c = fun_ctx (Ctx.forget (Ty.ctx (typ tm))) in
+    let db_sub = Unchecked.db_level_sub_inv c in
+    let c, _, _ = Unchecked.db_levels c in
+    let c = Ctx.check c in
+    let newexp = Unchecked.tm_apply_sub (fun_tm (forget tm)) db_sub in
+    let name =
+      Option.map
+        (fun pp_data ->
+          Display_maps.pp_data_rename (fun_pp_data pp_data) db_sub)
+        tm.name
+    in
+    (check c ?name newexp, db_sub)
 
-  type t = UnnamedTm.t * pp_data
+  let bdry t = (Ty.source (typ t), Ty.target (typ t))
+  let ctx t = Ctx.forget (Ty.ctx (typ t))
+  let name t = Option.map Unchecked.pp_data_to_string t.name
+  let full_name t = Option.map Unchecked.full_name t.name
+  let func_data t = Option.map (fun (_, _, f) -> f) t.name
+  let pp_data t = t.name
 
-  let typ (t, _) = UnnamedTm.typ t
-  let ty (t, _) = Ty.forget (UnnamedTm.typ t)
-  let ctx (t, _) = Ctx.forget (Ty.ctx (UnnamedTm.typ t))
-  let name (_, pp_data) = Unchecked.pp_data_to_string pp_data
-  let full_name (_, pp_data) = Unchecked.full_name pp_data
-  let func_data (_, (_, _, f)) = f
-  let pp_data (_, pp_data) = pp_data
+  let to_string t =
+    match full_name t with
+    | Some name -> name
+    | None -> Unchecked.tm_to_string (forget t)
 
   let of_coh coh =
     let ps, _, pp_data = Coh.forget coh in
     let id = Unchecked.identity_ps ps in
     let ctx = Unchecked.ps_to_ctx ps in
-    Tm.check (Ctx.check ctx) pp_data (Coh (coh, id))
-
-  let check c ?ty pp_data t =
-    Io.info ~v:5
-      (lazy
-        (Printf.sprintf "building kernel term %s in context %s"
-           (Unchecked.tm_to_string t) (Ctx.to_string c)));
-    let t = UnnamedTm.check c ?ty t in
-    (t, pp_data)
-
-  let develop (tm, _) = UnnamedTm.develop tm
-
-  let apply fun_ctx fun_tm fun_pp_data (tm, pp_data) =
-    let c = fun_ctx (Ctx.forget (Ty.ctx (UnnamedTm.typ tm))) in
-    let db_sub = Unchecked.db_level_sub_inv c in
-    let c, _, _ = Unchecked.db_levels c in
-    let c = Ctx.check c in
-    let pp_data = Display_maps.pp_data_rename (fun_pp_data pp_data) db_sub in
-    let tm = Unchecked.tm_apply_sub (fun_tm (UnnamedTm.forget tm)) db_sub in
-    (check c pp_data tm, db_sub)
+    check (Ctx.check ctx) ~name:pp_data (Coh (coh, id))
 end
 
 (** A coherence. *)
@@ -622,14 +618,7 @@ and Coh : sig
     t * Unchecked_types(Coh)(Tm).sub
 end = struct
   type cohInv = { ps : PS.t; ty : Ty.t }
-
-  type cohNonInv = {
-    ps : PS.t;
-    src : UnnamedTm.t;
-    tgt : UnnamedTm.t;
-    total_ty : Ty.t;
-  }
-
+  type cohNonInv = { ps : PS.t; src : Tm.t; tgt : Tm.t; total_ty : Ty.t }
   type t = Inv of cohInv * pp_data | NonInv of cohNonInv * pp_data
 
   module Types = Unchecked_types (Coh) (Tm)
@@ -654,8 +643,8 @@ end = struct
     | Inv (data, _) -> data.ty
     | NonInv (data, _) -> data.total_ty
 
-  let src c = UnnamedTm.forget (Ty.source (ty c))
-  let tgt c = UnnamedTm.forget (Ty.target (ty c))
+  let src c = Tm.forget (Ty.source (ty c))
+  let tgt c = Tm.forget (Ty.target (ty c))
   let is_inv = function Inv (_, _) -> true | NonInv (_, _) -> false
 
   let algebraic ps ty name =
@@ -668,12 +657,12 @@ end = struct
       in
       try
         let src_inclusion = PS.source ps in
-        let src = UnnamedTm.preimage src src_inclusion in
-        if not (UnnamedTm.is_full src) then raise NotAlgebraic
+        let src = Tm.preimage src src_inclusion in
+        if not (Tm.is_full src) then raise NotAlgebraic
         else
           let tgt_inclusion = PS.target ps in
-          let tgt = UnnamedTm.preimage tgt tgt_inclusion in
-          if not (UnnamedTm.is_full tgt) then raise NotAlgebraic
+          let tgt = Tm.preimage tgt tgt_inclusion in
+          if not (Tm.is_full tgt) then raise NotAlgebraic
           else NonInv ({ ps; src; tgt; total_ty = ty }, name)
       with NotInImage -> raise NotAlgebraic
 
@@ -712,16 +701,16 @@ end = struct
         let tgt_inclusion = PS.target ps in
         let bdry = PS.bdry ps in
         let cbdry = PS.to_ctx bdry in
-        let src = UnnamedTm.check cbdry src_unchkd in
-        if not (UnnamedTm.is_full src) then raise NotAlgebraic
+        let src = Tm.check cbdry src_unchkd in
+        if not (Tm.is_full src) then raise NotAlgebraic
         else
-          let tgt = UnnamedTm.check cbdry tgt_unchkd in
-          if not (UnnamedTm.is_full tgt) then raise NotAlgebraic
+          let tgt = Tm.check cbdry tgt_unchkd in
+          if not (Tm.is_full tgt) then raise NotAlgebraic
           else
             let total_ty =
               Ty.morphism
-                (UnnamedTm.apply_sub src src_inclusion)
-                (UnnamedTm.apply_sub tgt tgt_inclusion)
+                (Tm.apply_sub src src_inclusion)
+                (Tm.apply_sub tgt tgt_inclusion)
             in
             let coh = NonInv ({ ps; src; tgt; total_ty }, name) in
             Hashtbl.add tbl_noninv (ps_unchkd, src_unchkd, tgt_unchkd) coh;
@@ -733,8 +722,8 @@ end = struct
     | None ->
         let ctx = Ctx.check (Unchecked.ps_to_ctx ps_unchkd) in
         let ps = PS.mk ctx in
-        let src = UnnamedTm.check ctx src_unchkd in
-        let tgt = UnnamedTm.check ctx tgt_unchkd in
+        let src = Tm.check ctx src_unchkd in
+        let tgt = Tm.check ctx tgt_unchkd in
         let ty = Ty.morphism src tgt in
         if Ty.is_full ty then (
           let coh = Inv ({ ps; ty }, name) in
@@ -756,9 +745,7 @@ end = struct
     match c with
     | Inv (_, _) -> Error.fatal "non-invertible data of an invertible coh"
     | NonInv (d, _) ->
-        ( UnnamedTm.forget d.src,
-          UnnamedTm.forget d.tgt,
-          Ty.forget (UnnamedTm.typ d.src) )
+        (Tm.forget d.src, Tm.forget d.tgt, Ty.forget (Tm.typ d.src))
 
   let dim c =
     let ty = match c with Inv (d, _) -> d.ty | NonInv (d, _) -> d.total_ty in
@@ -830,15 +817,16 @@ let check_type ctx a =
   let ty = lazy ("type: " ^ Unchecked.ty_to_string a) in
   check (fun () -> Ty.check ctx a) ty
 
-let check_unnamed_term ctx ?ty t =
+let check_term ctx ?ty ?name t =
   let ty = Option.map (check_type ctx) ty in
   let tm = lazy ("term: " ^ Unchecked.tm_to_string t) in
-  check (fun () -> UnnamedTm.check ctx ?ty t) tm
+  check (fun () -> Tm.check ctx ?ty ?name t) tm
 
-let check_term ctx pp_data ?ty t =
-  let ty = Option.map (check_type ctx) ty in
-  let tm = lazy ("term: " ^ Unchecked.tm_to_string t) in
-  check (fun () -> Tm.check ctx pp_data ?ty t) tm
+let check_constr ?name ctx constr =
+  let ctx = Ctx.check ctx in
+  let t, ty = constr in
+  let ty = if !Settings.debug then None else Some ty in
+  check_term ctx ?ty ?name t
 
 let check_coh ps ty pp_data =
   let c = lazy ("coherence: " ^ Unchecked.pp_data_to_string pp_data) in
diff --git a/lib/kernel.mli b/lib/kernel.mli
index 554ad7ca..e7d907a9 100644
--- a/lib/kernel.mli
+++ b/lib/kernel.mli
@@ -60,13 +60,17 @@ and Tm : sig
 
   val typ : t -> Ty.t
   val ty : t -> Unchecked_types(Coh)(Tm).ty
+  val forget : t -> Unchecked_types(Coh)(Tm).tm
+  val constr : t -> Unchecked_types(Coh)(Tm).constr
+  val bdry : t -> t * t
   val ctx : t -> Unchecked_types(Coh)(Tm).ctx
-  val name : t -> string
-  val full_name : t -> string
-  val func_data : t -> (Var.t * int) list list
+  val name : t -> string option
+  val full_name : t -> string option
+  val func_data : t -> (Var.t * int) list list option
   val of_coh : Coh.t -> t
   val develop : t -> Unchecked_types(Coh)(Tm).tm
-  val pp_data : t -> pp_data
+  val pp_data : t -> pp_data option
+  val to_string : t -> string
 
   val apply :
     (Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
@@ -78,12 +82,6 @@ end
 
 open Unchecked_types(Coh)(Tm)
 
-module UnnamedTm : sig
-  type t
-
-  val ty : t -> ty
-end
-
 module Ctx : sig
   type t
 
@@ -165,6 +163,15 @@ module Unchecked : sig
   val list_to_sub : tm list -> ctx -> sub
   val list_to_db_level_sub : tm list -> (Var.t * tm) list
   val identity : ctx -> sub
+  val disc : int -> ps
+  val disc_ctx : int -> ctx
+  val disc_type : int -> ty
+  val sphere : int -> ctx
+  val sphere_inc : int -> sub
+  val disc_src : int -> sub_ps
+  val disc_tgt : int -> sub_ps
+  val develop_tm : tm -> tm
+  val develop_ty : ty -> ty
 end
 
 module Display_maps : sig
@@ -173,7 +180,7 @@ module Display_maps : sig
   val glue : sub -> sub -> sub -> ctx -> sub -> sub
 end
 
-val check_unnamed_term : Ctx.t -> ?ty:ty -> tm -> UnnamedTm.t
-val check_term : Ctx.t -> pp_data -> ?ty:ty -> tm -> Tm.t
+val check_term : Ctx.t -> ?ty:ty -> ?name:pp_data -> tm -> Tm.t
+val check_constr : ?name:pp_data -> ctx -> constr -> Tm.t
 val check_coh : ps -> ty -> pp_data -> Coh.t
 val check_sub : ctx -> sub -> ctx -> unit
diff --git a/lib/opposite.ml b/lib/opposite.ml
index 96c19abd..b8313637 100644
--- a/lib/opposite.ml
+++ b/lib/opposite.ml
@@ -102,9 +102,9 @@ let tm t op_data =
   t
 
 let checked_tm t op_data =
-  let pp_data = Tm.pp_data t in
+  let name = Option.map (fun a -> op_pp_data a op_data) (Tm.pp_data t) in
   let c = Tm.ctx t in
   let t = Tm.develop t in
   let c = ctx c op_data in
   let t = tm t op_data in
-  check_term (Ctx.check c) (op_pp_data pp_data op_data) t
+  check_term (Ctx.check c) ?name t
diff --git a/lib/telescope.ml b/lib/telescope.ml
index ab682e7f..d476e6aa 100644
--- a/lib/telescope.ml
+++ b/lib/telescope.ml
@@ -187,4 +187,4 @@ let rec telescope k =
 
 let checked k =
   let name = "builtin_telescope" ^ string_of_int k in
-  check_term (Ctx.check (ctx k)) (name, 0, []) (telescope k)
+  check_term (Ctx.check (ctx k)) ~name:(name, 0, []) (telescope k)
diff --git a/lib/unchecked.ml b/lib/unchecked.ml
index 2f96b48b..b55b8d97 100644
--- a/lib/unchecked.ml
+++ b/lib/unchecked.ml
@@ -17,8 +17,8 @@ struct
     val check_equal : CohT.t -> CohT.t -> unit
     val check : ps -> ty -> pp_data -> CohT.t
   end) (Tm : sig
-    val name : TmT.t -> string
-    val func_data : TmT.t -> (Var.t * int) list list
+    val name : TmT.t -> string option
+    val func_data : TmT.t -> (Var.t * int) list list option
     val develop : TmT.t -> Unchecked_types(CohT)(TmT).tm
 
     val apply :
@@ -435,11 +435,14 @@ struct
               let func = Coh.func_data c in
               Printf.sprintf "(%s%s)" (Coh.to_string c)
                 (sub_ps_to_string ~func s)
-        | App (t, s) ->
-            let func = Tm.func_data t in
-            let str_s, expl = sub_to_string ~func s in
-            let expl_str = if expl then "@" else "" in
-            Printf.sprintf "(%s%s%s)" expl_str (Tm.name t) str_s
+        | App (t, s) -> (
+            match Tm.name t with
+            | Some name ->
+                let func = Tm.func_data t in
+                let str_s, expl = sub_to_string ?func s in
+                let expl_str = if expl then "@" else "" in
+                Printf.sprintf "(%s%s%s)" expl_str name str_s
+            | None -> tm_to_string (tm_apply_sub (Tm.develop t) s))
 
       and sub_ps_to_string ?(func = []) s =
         match func with
@@ -568,6 +571,17 @@ struct
     let pp_data_to_string = Printing.pp_data_to_string
     let full_name = Printing.full_name
 
+    let rec tm_contains_var t x =
+      match t with
+      | Var v -> v = x
+      | Coh (_, s) -> List.exists (fun (t, _) -> tm_contains_var t x) s
+      | App (t, s) ->
+          List.exists
+            (fun (y, (u, _)) ->
+              tm_contains_var (Tm.develop t) y && tm_contains_var u x)
+            s
+      | Meta_tm _ -> Error.fatal "meta-variables should be resolved"
+
     let rec check_equal_ps ps1 ps2 =
       match (ps1, ps2) with
       | Br [], Br [] -> ()
@@ -602,8 +616,8 @@ struct
       | Coh (coh1, s1), Coh (coh2, s2) ->
           Coh.check_equal coh1 coh2;
           check_equal_sub_ps s1 s2
-      (* Define check_equal_sub and Tm.develop *)
-      | App (t1, s1), App (t2, s2) when t1 == t2 -> check_equal_sub s1 s2
+      | App (t1, s1), App (t2, s2) when t1 == t2 ->
+          check_equal_sub_on_support t1 s1 s2
       | App (t, s), ((Coh _ | App _ | Var _) as tm2)
       | ((Coh _ | Var _) as tm2), App (t, s) ->
           let c = Tm.develop t in
@@ -621,8 +635,12 @@ struct
     and check_equal_sub_ps s1 s2 =
       List.iter2 (fun (t1, _) (t2, _) -> check_equal_tm t1 t2) s1 s2
 
-    and check_equal_sub s1 s2 =
-      List.iter2 (fun (_, (t1, _)) (_, (t2, _)) -> check_equal_tm t1 t2) s1 s2
+    and check_equal_sub_on_support t s1 s2 =
+      List.iter2
+        (fun (x, (t1, _)) (y, (t2, _)) ->
+          Var.check_equal x y;
+          if tm_contains_var (Tm.develop t) x then check_equal_tm t1 t2)
+        s1 s2
 
     let rec check_equal_ctx ctx1 ctx2 =
       match (ctx1, ctx2) with
@@ -646,13 +664,6 @@ struct
     let check_equal_ctx ctx1 ctx2 =
       if ctx1 == ctx2 then () else check_equal_ctx ctx1 ctx2
 
-    let rec tm_contains_var t x =
-      match t with
-      | Var v -> v = x
-      | Coh (_, s) -> List.exists (fun (t, _) -> tm_contains_var t x) s
-      | App (_, s) -> List.exists (fun (_, (t, _)) -> tm_contains_var t x) s
-      | Meta_tm _ -> Error.fatal "meta-variables should be resolved"
-
     let rec ty_contains_var a x =
       match a with
       | Obj -> false
@@ -708,6 +719,47 @@ struct
       | [] -> []
       | (x, (_, e)) :: ctx -> (x, (Var x, e)) :: identity ctx
 
+    let rec disc = function 0 -> Br [] | n -> Br [ disc (n - 1) ]
+    let disc_ctx n = ps_to_ctx (disc n)
+
+    let rec disc_type n =
+      if n = 0 then Obj
+      else
+        Arr
+          ( disc_type (n - 1),
+            Var (Var.Db ((2 * n) - 2)),
+            Var (Var.Db ((2 * n) - 1)) )
+
+    let sphere n =
+      if n = -1 then []
+      else
+        let d = ps_to_ctx (disc n) in
+        (Var.Db ((2 * n) + 1), (disc_type n, true)) :: d
+
+    let sphere_inc n = identity (sphere n)
+    let disc_src n = identity_ps (disc n)
+
+    let disc_tgt n =
+      (Var (Var.Db ((2 * n) + 1)), true)
+      :: (Var (Var.Db ((2 * n) - 1)), true)
+      :: identity_ps (disc (n - 1))
+
+    let rec develop_tm tm =
+      match tm with
+      | Var v -> Var v
+      | Meta_tm i -> Meta_tm i
+      | Coh (coh, s) -> Coh (coh, develop_sub_ps s)
+      | App (tm, s) -> tm_apply_sub (Tm.develop tm) (develop_sub s)
+
+    and develop_sub_ps s = List.map (fun (t, b) -> (develop_tm t, b)) s
+    and develop_sub s = List.map (fun (x, (t, b)) -> (x, (develop_tm t, b))) s
+
+    let rec develop_ty ty =
+      match ty with
+      | Obj -> Obj
+      | Meta_ty i -> Meta_ty i
+      | Arr (a, t, u) -> Arr (develop_ty a, develop_tm t, develop_tm u)
+
     module Display_maps = struct
       (* Construction related to display maps, i.e. var to var substitutions *)
       let var_apply_sub v s =
diff --git a/lib/unchecked.mli b/lib/unchecked.mli
index e7a8e09e..9c69a95a 100644
--- a/lib/unchecked.mli
+++ b/lib/unchecked.mli
@@ -15,8 +15,8 @@ end) : sig
     val check_equal : Coh.t -> Coh.t -> unit
     val check : ps -> ty -> pp_data -> Coh.t
   end) (_ : sig
-    val name : Tm.t -> string
-    val func_data : Tm.t -> (Var.t * int) list list
+    val name : Tm.t -> string option
+    val func_data : Tm.t -> (Var.t * int) list list option
     val develop : Tm.t -> Unchecked_types(Coh)(Tm).tm
 
     val apply :
@@ -92,6 +92,15 @@ end) : sig
     val list_to_sub : tm list -> ctx -> sub
     val list_to_db_level_sub : tm list -> (Var.t * tm) list
     val identity : ctx -> sub
+    val disc : int -> ps
+    val disc_ctx : int -> ctx
+    val disc_type : int -> ty
+    val sphere : int -> ctx
+    val sphere_inc : int -> sub
+    val disc_src : int -> sub_ps
+    val disc_tgt : int -> sub_ps
+    val develop_tm : tm -> tm
+    val develop_ty : ty -> ty
 
     module Display_maps : sig
       val var_apply_sub : Var.t -> sub -> Var.t
diff --git a/lib/unchecked_types.ml b/lib/unchecked_types.ml
index c27a87be..a23125a4 100644
--- a/lib/unchecked_types.ml
+++ b/lib/unchecked_types.ml
@@ -21,6 +21,7 @@ module type Unchecked_types_sig = functor
 
   type ctx = (Var.t * (ty * bool)) list
   type meta_ctx = (int * ty) list
+  type constr = tm * ty
 end
 
 module Unchecked_types (Coh : sig
@@ -42,4 +43,5 @@ struct
 
   type ctx = (Var.t * (ty * bool)) list
   type meta_ctx = (int * ty) list
+  type constr = tm * ty
 end
diff --git a/lib/unchecked_types.mli b/lib/unchecked_types.mli
index debe595c..b15008a7 100644
--- a/lib/unchecked_types.mli
+++ b/lib/unchecked_types.mli
@@ -21,6 +21,7 @@ module type Unchecked_types_sig = functor
 
   type ctx = (Var.t * (ty * bool)) list
   type meta_ctx = (int * ty) list
+  type constr = tm * ty
 end
 
 module Unchecked_types : Unchecked_types_sig
diff --git a/test.t/run.t b/test.t/run.t
index f87971f5..f7eb3036 100644
--- a/test.t/run.t
+++ b/test.t/run.t
@@ -184,9 +184,9 @@
   [=^.^=] let optest1 = op_{1}((test  c d a b))
   [=I.I=] successfully defined term (test_op{1} z y g g' c g'' d x f f' a f'' b) of type (builtin_comp2_op{1} z y g x f) -> (builtin_comp2_op{1} z y g'' x f'').
   [=^.^=] let optest2 = op_{2}((test  b a d c))
-  [=I.I=] successfully defined term (test_op{2} x y f'' f' b f a z g'' g' d g c) of type (builtin_comp2_op{2} x y f z g) -> (builtin_comp2_op{2} x y f'' z g'').
+  [=I.I=] successfully defined term (test_op{2} x y f'' f' b f a z g'' g' d g c) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
   [=^.^=] let optest12 = op_{1,2}((test  d c b a))
-  [=I.I=] successfully defined term (test_op{1,2} z y g'' g' d g c x f'' f' b f a) of type (builtin_comp2_op{1,2} z y g x f) -> (builtin_comp2_op{1,2} z y g'' x f'').
+  [=I.I=] successfully defined term (test_op{1,2} z y g'' g' d g c x f'' f' b f a) of type (builtin_comp2_op{1} z y g x f) -> (builtin_comp2_op{1} z y g'' x f'').
   [=^.^=] let nested1 = op_{1}((_builtin_comp  [(_builtin_comp  c d)] [(_builtin_comp  a b)]))
   [=I.I=] successfully defined term (builtin_comp2_func[(.4,1) (.8,1)]_op{1} z y g g'' (!1builtin_comp2_op{1} z y g g' c g'' d) x f f'' (!1builtin_comp2_op{1} y x f f' a f'' b)) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
   [=^.^=] let nested2 = op_{2}((_builtin_comp  [(_builtin_comp  b a)] [(_builtin_comp  d c)]))
@@ -198,7 +198,7 @@
   [=^.^=] coh assoc_susp = (_builtin_comp  f (_builtin_comp  g h)) -> (_builtin_comp  (_builtin_comp  f g) h)
   [=I.I=] successfully defined assoc_susp.
   [=^.^=] let test = (_builtin_id  op_{3}((assoc_susp  f g h)))
-  [=I.I=] successfully defined term (!3builtin_id p q x w (!1builtin_comp2_op{3} p q x z (!1builtin_comp2_op{3} p q x y f z g) w h) (!1builtin_comp2_op{3} p q x y f w (!1builtin_comp2_op{3} p q y z g w h)) (assoc_susp_op{3} p q x y f z g w h)) of type (assoc_susp_op{3} p q x y f z g w h) -> (assoc_susp_op{3} p q x y f z g w h).
+  [=I.I=] successfully defined term (!3builtin_id p q x w (!1builtin_comp2 p q x z (!1builtin_comp2 p q x y f z g) w h) (!1builtin_comp2 p q x y f w (!1builtin_comp2 p q y z g w h)) (assoc_susp_op{3} p q x y f z g w h)) of type (assoc_susp_op{3} p q x y f z g w h) -> (assoc_susp_op{3} p q x y f z g w h).
 
   $ catt features/inverses.catt
   [=^.^=] let id_inv = I((_builtin_id  x))
@@ -664,6 +664,6 @@
   [=^.^=] coh eh1 = (_builtin_comp  a b) -> (_builtin_comp  I((unitl  f)) (_builtin_comp  (_builtin_comp  _ [a]) (_builtin_comp  (unitl  g) I(op_{1}((unitl  g)))) (_builtin_comp  [b] _)) op_{1}((unitl  h)))
   [=I.I=] successfully defined eh1.
   [=^.^=] let eh2 = (_builtin_comp  [(Ilsimp  _)] [(_builtin_comp  (_builtin_comp  _ [(_builtin_comp  (_builtin_comp  [(lsimp  _)] [op_{1}((Ilsimp  _))]) U((unit  _)))] _) (exch  b a))] [op_{1}((lsimp  _))])
-  [=I.I=] successfully defined term (!1builtin_comp3 [(Ilsimp x)] [(!2builtin_comp2 (!1builtin_comp3 (builtin_comp2 (builtin_id x) [a]) [(!2builtin_comp2 (!1builtin_comp2 [(lsimp x)] [(Ilsimp_op{1} x)]) (unit_Unit x))] (builtin_comp2 [b] (builtin_id x))) (exch b a))] [(lsimp_op{1} x)]) of type (!1builtin_comp3 (unitl^-1 (builtin_id x)) (!1builtin_comp3 (builtin_comp2 (builtin_id x) [a]) (!1builtin_comp2 (unitl (builtin_id x)) (unitl_op{1}^-1 (builtin_id_op{1} x))) (builtin_comp2 [b] (builtin_id x))) (unitl_op{1} (builtin_id_op{1} x))) -> (!1builtin_comp3 (unit^-1 x) (builtin_comp2 [b] [a]) (unit_op{1} x)).
+  [=I.I=] successfully defined term (!1builtin_comp3 [(Ilsimp x)] [(!2builtin_comp2 (!1builtin_comp3 (builtin_comp2 (builtin_id x) [a]) [(!2builtin_comp2 (!1builtin_comp2 [(lsimp x)] [(Ilsimp_op{1} x)]) (unit_Unit x))] (builtin_comp2 [b] (builtin_id x))) (exch b a))] [(lsimp_op{1} x)]) of type (!1builtin_comp3 (unitl^-1 (builtin_id x)) (!1builtin_comp3 (builtin_comp2 (builtin_id x) [a]) (!1builtin_comp2 (unitl (builtin_id x)) (unitl_op{1}^-1 (builtin_id x))) (builtin_comp2 [b] (builtin_id x))) (unitl_op{1} (builtin_id x))) -> (!1builtin_comp3 (unit^-1 x) (builtin_comp2 [b] [a]) (unit_op{1} x)).
   [=^.^=] let eh = (_builtin_comp  (eh1  a b) (eh2  a b) I(op_{1}((eh2  b a))) I(op_{1}((eh1  b a))))
-  [=I.I=] successfully defined term (!2builtin_comp4 (eh1 a b) (eh2 a b) (!1builtin_comp3 [(Ilsimp_op{1}^-1 x)] [(!2builtin_comp2 (exch_op{1}^-1 b a) (!1builtin_comp3 (builtin_comp2_func[(.6,1)]_op{1} (builtin_id_op{1} x) b) [(!2builtin_comp2 (unit_Unit_op{1}^-1 x) (!1builtin_comp2 [(lsimp_op{1}^-1 x)] [(Ilsimp_op{1}_op{1}^-1 x)]))] (builtin_comp2_func[(.4,1)]_op{1} a (builtin_id_op{1} x))))] [(lsimp_op{1}_op{1}^-1 x)]) (eh1_op{1}^-1 b a)) of type (!1builtin_comp2 a b) -> (!1builtin_comp2_op{1} b a).
+  [=I.I=] successfully defined term (!2builtin_comp4 (eh1 a b) (eh2 a b) (!1builtin_comp3 [(Ilsimp_op{1}^-1 x)] [(!2builtin_comp2 (exch_op{1}^-1 b a) (!1builtin_comp3 (builtin_comp2_func[(.6,1)]_op{1} (builtin_id x) b) [(!2builtin_comp2 (unit_Unit_op{1}^-1 x) (!1builtin_comp2 [(lsimp_op{1}^-1 x)] [(Ilsimp_op{1}_op{1}^-1 x)]))] (builtin_comp2_func[(.4,1)]_op{1} a (builtin_id x))))] [(lsimp_op{1}_op{1}^-1 x)]) (eh1_op{1}^-1 b a)) of type (!1builtin_comp2 a b) -> (!1builtin_comp2_op{1} b a).