From 578711cf10c713cd6302571ea7977e01f678050c Mon Sep 17 00:00:00 2001
From: regular-citizen <chiara@sarti.me>
Date: Wed, 28 Aug 2024 11:10:06 +0100
Subject: [PATCH 1/5] kernel performance improvement

---
 lib/kernel.ml     | 27 ++++++++++++++++-----------
 lib/unchecked.ml  | 12 ++++++++++++
 lib/unchecked.mli |  1 +
 3 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/lib/kernel.ml b/lib/kernel.ml
index 76c69edc..f819f140 100644
--- a/lib/kernel.ml
+++ b/lib/kernel.ml
@@ -111,7 +111,8 @@ end = struct
   let to_string ctx = Unchecked.ctx_to_string (forget ctx)
 
   let check_equal ctx1 ctx2 =
-    Unchecked.check_equal_ctx (forget ctx1) (forget ctx2)
+    if ctx1 == ctx2 then ()
+    else Unchecked.check_equal_ctx (forget ctx1) (forget ctx2)
 
   let check_notin ctx x =
     try
@@ -274,7 +275,9 @@ end = struct
   let target ps =
     Sub.check_to_ps (to_ctx ps) (Unchecked.ps_tgt ps.tree) (bdry ps)
 
-  let check_equal ps1 ps2 = Unchecked.check_equal_ps ps1.tree ps2.tree
+  let check_equal ps1 ps2 =
+    if ps1.tree == ps2.tree then ()
+    else Unchecked.check_equal_ps ps1.tree ps2.tree
 end
 
 and Ty : sig
@@ -570,15 +573,17 @@ end = struct
     (PS.forget ps, Ty.forget ty, pp_data)
 
   let check_equal coh1 coh2 =
-    match (coh1, coh2) with
-    | Inv (d1, _), Inv (d2, _) ->
-        PS.check_equal d1.ps d2.ps;
-        Ty.check_equal d1.ty d2.ty
-    | NonInv (d1, _), NonInv (d2, _) ->
-        PS.check_equal d1.ps d2.ps;
-        Ty.check_equal d1.total_ty d2.total_ty
-    | Inv _, NonInv _ | NonInv _, Inv _ ->
-        raise (NotEqual (to_string coh1, to_string coh2))
+    if coh1 == coh2 then ()
+    else
+      match (coh1, coh2) with
+      | Inv (d1, _), Inv (d2, _) ->
+          PS.check_equal d1.ps d2.ps;
+          Ty.check_equal d1.ty d2.ty
+      | NonInv (d1, _), NonInv (d2, _) ->
+          PS.check_equal d1.ps d2.ps;
+          Ty.check_equal d1.total_ty d2.total_ty
+      | Inv _, NonInv _ | NonInv _, Inv _ ->
+          raise (NotEqual (to_string coh1, to_string coh2))
 end
 
 module U = Unchecked (Coh)
diff --git a/lib/unchecked.ml b/lib/unchecked.ml
index 3f74d629..b1bf958c 100644
--- a/lib/unchecked.ml
+++ b/lib/unchecked.ml
@@ -185,6 +185,18 @@ struct
       | _ :: _, [] | [], _ :: _ ->
           raise (NotEqual (ctx_to_string ctx1, ctx_to_string ctx2))
 
+    let check_equal_ty ty1 ty2 =
+      if ty1 == ty2 then () else check_equal_ty ty1 ty2
+
+    let check_equal_tm tm1 tm2 =
+      if tm1 == tm2 then () else check_equal_tm tm1 tm2
+
+    let check_equal_sub_ps s1 s2 =
+      if s1 == s2 then () else check_equal_sub_ps s1 s2
+
+    let check_equal_ctx ctx1 ctx2 =
+      if ctx1 == ctx2 then () else check_equal_ctx ctx1 ctx2
+
     let rec tm_do_on_variables tm f =
       match tm with
       | Var v -> f v
diff --git a/lib/unchecked.mli b/lib/unchecked.mli
index 77caf8e2..dd18223e 100644
--- a/lib/unchecked.mli
+++ b/lib/unchecked.mli
@@ -28,6 +28,7 @@ end) : sig
     val check_equal_ps : ps -> ps -> unit
     val check_equal_ty : ty -> ty -> unit
     val check_equal_tm : tm -> tm -> unit
+    val check_equal_sub_ps : sub_ps -> sub_ps -> unit
     val dim_ctx : ctx -> int
     val dim_ty : ty -> int
     val dim_ps : ps -> int

From 29da81ce6926d4fe300b33d1589236a31c17a9b1 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Mon, 2 Sep 2024 14:25:08 +0100
Subject: [PATCH 2/5] add memoisation to the kernel

---
 lib/kernel.ml    | 218 ++++++++++++++++++++++++++++++-----------------
 lib/unchecked.ml |  10 ++-
 2 files changed, 150 insertions(+), 78 deletions(-)

diff --git a/lib/kernel.ml b/lib/kernel.ml
index f819f140..1b0f1bbe 100644
--- a/lib/kernel.ml
+++ b/lib/kernel.ml
@@ -30,7 +30,9 @@ end = struct
 
   open Unchecked (Coh)
   module Unchecked = Make (Coh)
+  module Types = Unchecked_types (Coh)
 
+  let tbl : (Ctx.t * PS.t * Types.sub_ps, Sub.t) Hashtbl.t = Hashtbl.create 7829
   let free_vars s = List.concat (List.map Tm.free_vars s.list)
 
   let check src s tgt =
@@ -61,14 +63,19 @@ end = struct
     in
     aux src s tgt
 
-  let check_to_ps src s tgt =
-    let tgt = PS.to_ctx tgt in
-    let s =
-      try List.map2 (fun (x, _) (t, _) -> (x, t)) (Ctx.value tgt) s
-      with Invalid_argument _ ->
-        Error.fatal "uncaught wrong number of arguments"
-    in
-    check src s tgt
+  let check_to_ps src s tgt_ps =
+    match Hashtbl.find_opt tbl (src, tgt_ps, s) with
+    | Some sub -> sub
+    | None ->
+        let tgt = PS.to_ctx tgt_ps in
+        let s_assoc =
+          try List.map2 (fun (x, _) (t, _) -> (x, t)) (Ctx.value tgt) s
+          with Invalid_argument _ ->
+            Error.fatal "uncaught wrong number of arguments"
+        in
+        let sub = check src s_assoc tgt in
+        Hashtbl.add tbl (src, tgt_ps, s) sub;
+        sub
 
   let forget s = s.unchecked
 end
@@ -94,6 +101,8 @@ end = struct
   open Unchecked (Coh)
   module Unchecked = Make (Coh)
 
+  let tbl : (Unchecked_types(Coh).ctx, Ctx.t) Hashtbl.t = Hashtbl.create 7829
+
   let tail ctx =
     match (ctx.c, ctx.unchecked) with
     | [], (_ :: _ | []) -> Error.fatal "computing tail of an empty context"
@@ -129,9 +138,16 @@ end = struct
     }
 
   let check c =
-    List.fold_right
-      (fun (x, (t, expl)) c -> Ctx.extend ~expl c x t)
-      c (Ctx.empty ())
+    match Hashtbl.find_opt tbl c with
+    | Some ctx -> ctx
+    | None ->
+        let ctx =
+          List.fold_right
+            (fun (x, (t, expl)) c -> Ctx.extend ~expl c x t)
+            c (Ctx.empty ())
+        in
+        Hashtbl.add tbl c ctx;
+        ctx
 end
 
 (** Operations on pasting schemes. *)
@@ -164,6 +180,8 @@ end = struct
 
   (* TODO:fix level of explicitness here *)
 
+  let tbl : (Ctx.t, PS.t) Hashtbl.t = Hashtbl.create 7829
+
   (** Create a context from a pasting scheme. *)
   let old_rep_to_ctx ps =
     let rec list ps =
@@ -258,8 +276,13 @@ end = struct
     Br (fst (build_till_previous ps))
 
   let mk (l : Ctx.t) =
-    let oldrep = make_old l in
-    { tree = make_tree oldrep; ctx = l }
+    match Hashtbl.find_opt tbl l with
+    | Some ps -> ps
+    | None ->
+        let oldrep = make_old l in
+        let ps = { tree = make_tree oldrep; ctx = l } in
+        Hashtbl.add tbl l ps;
+        ps
 
   let forget ps = ps.tree
   let to_string ps = Unchecked.ps_to_string (forget ps)
@@ -305,7 +328,9 @@ end = struct
 
   open Unchecked (Coh)
   module Unchecked = Make (Coh)
+  module Types = Unchecked_types (Coh)
 
+  let tbl : (Ctx.t * Types.ty, Ty.t) Hashtbl.t = Hashtbl.create 7829
   let is_obj t = t.e = Obj
 
   let retrieve_arrow ty =
@@ -319,17 +344,22 @@ end = struct
       (lazy
         (Printf.sprintf "building kernel type %s in context %s"
            (Unchecked.ty_to_string t) (Ctx.to_string c)));
-    let e =
-      match t with
-      | Obj -> Obj
-      | Arr (a, u, v) ->
-          let a = check c a 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
-    { c; e; unchecked = t }
+    match Hashtbl.find_opt tbl (c, t) with
+    | Some ty -> ty
+    | None ->
+        let e =
+          match t with
+          | Obj -> Obj
+          | Arr (a, u, v) ->
+              let a = check c a 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
+        let ty = { c; e; unchecked = t } in
+        Hashtbl.add tbl (c, t) ty;
+        ty
 
   (** Free variables of a type. *)
   let rec free_vars ty =
@@ -386,7 +416,9 @@ end = struct
 
   open Unchecked (Coh)
   module Unchecked = Make (Coh)
+  module Types = Unchecked_types (Coh)
 
+  let tbl : (Ctx.t * Types.tm, Tm.t) Hashtbl.t = Hashtbl.create 7829
   let to_var tm = match tm.e with Var v -> v | Coh _ -> raise IsCoh
 
   let free_vars tm =
@@ -402,15 +434,20 @@ end = struct
         (Printf.sprintf "building kernel term %s in context %s"
            (Unchecked.tm_to_string t) (Ctx.to_string c)));
     let tm =
-      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 }
-      | 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
-          { ty; e; unchecked = t }
+      match Hashtbl.find_opt tbl (c, t) with
+      | Some tm -> tm
+      | None -> (
+          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 }
+          | 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 } in
+              Hashtbl.add tbl (c, t) tm;
+              tm)
     in
     match ty with
     | None -> tm
@@ -464,6 +501,16 @@ end = struct
   type cohNonInv = { ps : PS.t; src : Tm.t; tgt : Tm.t; total_ty : Ty.t }
   type t = Inv of cohInv * coh_pp_data | NonInv of cohNonInv * coh_pp_data
 
+  module Types = Unchecked_types (Coh)
+
+  let tbl : (ps * Types.ty, Coh.t) Hashtbl.t = Hashtbl.create 7829
+
+  let tbl_inv : (ps * Types.tm * Types.tm, Coh.t) Hashtbl.t =
+    Hashtbl.create 7829
+
+  let tbl_noninv : (ps * Types.tm * Types.tm, Coh.t) Hashtbl.t =
+    Hashtbl.create 7829
+
   exception NotAlgebraic
 
   open Unchecked (Coh)
@@ -496,53 +543,70 @@ end = struct
           else NonInv ({ ps; src; tgt; total_ty = ty }, name)
       with NotInImage -> raise NotAlgebraic
 
-  let check ps t ((name, _, _) as pp_data) =
+  let check ps_unchkd t_unchkd ((name, _, _) as pp_data) =
     Io.info ~v:5
       (lazy
         (Printf.sprintf "checking coherence (%s,%s)"
-           (Unchecked.ps_to_string ps)
-           (Unchecked.ty_to_string t)));
-    try
-      let cps = Ctx.check (Unchecked.ps_to_ctx ps) in
-      let ps = PS.mk cps in
-      let t = Ty.check cps t in
-      algebraic ps t pp_data
-    with
-    | NotAlgebraic ->
-        Error.not_valid_coherence name
-          (Printf.sprintf "type %s not full in pasting scheme %s"
-             (Unchecked.ty_to_string t)
-             Unchecked.(ctx_to_string (ps_to_ctx ps)))
-    | DoubledVar s ->
-        Error.not_valid_coherence name
-          (Printf.sprintf "variable %s appears twice in the context" s)
-
-  let check_noninv ps src tgt name =
-    let ps = PS.mk (Ctx.check (Unchecked.ps_to_ctx ps)) in
-    let src_inclusion = PS.source ps in
-    let tgt_inclusion = PS.target ps in
-    let bdry = PS.bdry ps in
-    let cbdry = PS.to_ctx bdry in
-    let src = Tm.check cbdry src in
-    if not (Tm.is_full src) then raise NotAlgebraic
-    else
-      let tgt = Tm.check cbdry tgt in
-      if not (Tm.is_full tgt) then raise NotAlgebraic
-      else
-        let total_ty =
-          Ty.morphism
-            (Tm.apply_sub src src_inclusion)
-            (Tm.apply_sub tgt tgt_inclusion)
-        in
-        NonInv ({ ps; src; tgt; total_ty }, name)
-
-  let check_inv ps src tgt name =
-    let ctx = Ctx.check (Unchecked.ps_to_ctx ps) in
-    let ps = PS.mk ctx in
-    let src = Tm.check ctx src in
-    let tgt = Tm.check ctx tgt in
-    let ty = Ty.morphism src tgt in
-    if Ty.is_full ty then Inv ({ ps; ty }, name) else raise NotAlgebraic
+           (Unchecked.ps_to_string ps_unchkd)
+           (Unchecked.ty_to_string t_unchkd)));
+    match Hashtbl.find_opt tbl (ps_unchkd, t_unchkd) with
+    | Some coh -> coh
+    | None -> (
+        try
+          let cps = Ctx.check (Unchecked.ps_to_ctx ps_unchkd) in
+          let ps = PS.mk cps in
+          let t = Ty.check cps t_unchkd in
+          let coh = algebraic ps t pp_data in
+          Hashtbl.add tbl (ps_unchkd, t_unchkd) coh;
+          coh
+        with
+        | NotAlgebraic ->
+            Error.not_valid_coherence name
+              (Printf.sprintf "type %s not algebraic in pasting scheme %s"
+                 (Unchecked.ty_to_string t_unchkd)
+                 Unchecked.(ctx_to_string (ps_to_ctx ps_unchkd)))
+        | DoubledVar s ->
+            Error.not_valid_coherence name
+              (Printf.sprintf "variable %s appears twice in the context" s))
+
+  let check_noninv ps_unchkd src_unchkd tgt_unchkd name =
+    match Hashtbl.find_opt tbl_noninv (ps_unchkd, src_unchkd, tgt_unchkd) with
+    | Some coh -> coh
+    | None ->
+        let ps = PS.mk (Ctx.check (Unchecked.ps_to_ctx ps_unchkd)) in
+        let src_inclusion = PS.source ps in
+        let tgt_inclusion = PS.target ps in
+        let bdry = PS.bdry ps in
+        let cbdry = PS.to_ctx bdry in
+        let src = Tm.check cbdry src_unchkd in
+        if not (Tm.is_full src) then raise NotAlgebraic
+        else
+          let tgt = Tm.check cbdry tgt_unchkd in
+          if not (Tm.is_full tgt) then raise NotAlgebraic
+          else
+            let total_ty =
+              Ty.morphism
+                (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;
+            coh
+
+  let check_inv ps_unchkd src_unchkd tgt_unchkd name =
+    match Hashtbl.find_opt tbl_inv (ps_unchkd, src_unchkd, tgt_unchkd) with
+    | Some coh -> coh
+    | None ->
+        let ctx = Ctx.check (Unchecked.ps_to_ctx ps_unchkd) in
+        let ps = PS.mk ctx 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
+          Hashtbl.add tbl_inv (ps_unchkd, src_unchkd, tgt_unchkd) coh;
+          coh)
+        else raise NotAlgebraic
 
   let data c =
     match c with
diff --git a/lib/unchecked.ml b/lib/unchecked.ml
index b1bf958c..0135b6b2 100644
--- a/lib/unchecked.ml
+++ b/lib/unchecked.ml
@@ -413,7 +413,15 @@ struct
       let incls, _ = canonical_inclusions l in
       incls
 
-    let ps_to_ctx ps = (ps_to_ctx_rp ps).ctx
+    let tbl_ps_to_ctx : (ps, ctx) Hashtbl.t = Hashtbl.create 7829
+
+    let ps_to_ctx ps =
+      match Hashtbl.find_opt tbl_ps_to_ctx ps with
+      | Some ctx -> ctx
+      | None ->
+          let ctx = (ps_to_ctx_rp ps).ctx in
+          Hashtbl.add tbl_ps_to_ctx ps ctx;
+          ctx
 
     let suspwedge_subs_ps list_subs list_ps =
       let incls = canonical_inclusions list_ps in

From ea7cb98a1f919cf7873cd5fc25842427c37c7ad7 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Mon, 2 Sep 2024 15:54:52 +0100
Subject: [PATCH 3/5] add landmarks for profiling

---
 dune-workspace | 9 +++++++++
 flake.nix      | 2 ++
 lib/dune       | 3 ++-
 3 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 dune-workspace

diff --git a/dune-workspace b/dune-workspace
new file mode 100644
index 00000000..653c2f3f
--- /dev/null
+++ b/dune-workspace
@@ -0,0 +1,9 @@
+(lang dune 3.7)
+
+(context default)
+(context
+  (default
+     (name profiling)
+     (instrument_with landmarks)
+     (env
+       (_ (env-vars ("OCAML_LANDMARKS" "output=profile.txt"))))))
\ No newline at end of file
diff --git a/flake.nix b/flake.nix
index b0bc2eed..8c93e2e6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -192,6 +192,8 @@
               ocamlformat
               ocp-indent
               ocamlformat-rpc-lib
+              landmarks
+              landmarks-ppx
               utop
             ]);
 
diff --git a/lib/dune b/lib/dune
index 5a8f9749..f461e413 100644
--- a/lib/dune
+++ b/lib/dune
@@ -7,4 +7,5 @@
  (name catt)
  (public_name catt)
  (modules_without_implementation raw_types)
- (libraries base))
+ (libraries base)
+ (instrumentation (backend landmarks --auto)))

From 73d0c9b7e0b9c3b0134e4562fe9a483516dbfe3a Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 1 Oct 2024 11:08:30 +0100
Subject: [PATCH 4/5] prevent identity to be named builtin_id when builtins are
 not used

---
 lib/builtin.ml       | 6 +++---
 lib/builtin.mli      | 2 +-
 lib/inverse.ml       | 4 ++--
 lib/telescope.ml     | 8 ++++----
 lib/translate_raw.ml | 2 +-
 5 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/lib/builtin.ml b/lib/builtin.ml
index 70682399..1b6d3a42 100644
--- a/lib/builtin.ml
+++ b/lib/builtin.ml
@@ -12,7 +12,7 @@ module Memo = struct
       Hashtbl.add tbl i res;
       res
 
-  let id =
+  let id _ =
     check_coh (Br []) (Arr (Obj, Var (Db 0), Var (Db 0))) ("builtin_id", 0, [])
 end
 
@@ -46,7 +46,7 @@ let id_all_max ps =
     let t = Var (Db 0) in
     match l with
     | [] -> [ (t, false) ]
-    | Br [] :: l -> (Coh (id, [ (t, true) ]), true) :: (t, false) :: id_map l
+    | Br [] :: l -> (Coh (id (), [ (t, true) ]), true) :: (t, false) :: id_map l
     | _ -> Error.fatal "identity must be inserted on maximal argument"
   in
   let rec aux i ps =
@@ -71,5 +71,5 @@ let unbiased_unitor ps 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
+  let tgt = Coh (Suspension.coh (Some da) (id ()), (t, true) :: sub_base) in
   Coh.check_inv bdry src tgt ("unbiased_unitor", 0, [])
diff --git a/lib/builtin.mli b/lib/builtin.mli
index bb19207e..04b831d1 100644
--- a/lib/builtin.mli
+++ b/lib/builtin.mli
@@ -7,5 +7,5 @@ val ps_comp : int -> ps
 val comp_n : int -> Coh.t
 val comp : subR -> bool -> Coh.t
 val arity_comp : subR -> bool -> int
-val id : Coh.t
+val id : unit -> Coh.t
 val unbiased_unitor : ps -> tm -> Coh.t
diff --git a/lib/inverse.ml b/lib/inverse.ml
index 389a2fc8..e97c0920 100644
--- a/lib/inverse.ml
+++ b/lib/inverse.ml
@@ -105,7 +105,7 @@ and cancel_all_linear_comp t =
         let id_src_t =
           let sub_base = Unchecked.ty_to_sub_ps ty_base in
           let id =
-            Suspension.coh (Some (Unchecked.dim_ty ty_base)) Builtin.id
+            Suspension.coh (Some (Unchecked.dim_ty ty_base)) (Builtin.id ())
           in
           Coh (id, (src_t, true) :: sub_base)
         in
@@ -164,7 +164,7 @@ and compute_witness_coh_inv c s ~ps ~pp_data ~d ~sub_base ~u ~v =
     Coh (comp, c_c_inv)
   in
   let tgt_wit =
-    let id = Suspension.coh (Some (d - 1)) Builtin.id in
+    let id = Suspension.coh (Some (d - 1)) (Builtin.id ()) in
     let sub_id_u = (u, true) :: sub_base in
     Coh (id, sub_id_u)
   in
diff --git a/lib/telescope.ml b/lib/telescope.ml
index 0f16b733..2d32fe93 100644
--- a/lib/telescope.ml
+++ b/lib/telescope.ml
@@ -55,7 +55,7 @@ let middle_unitor k =
             :: (Var (Db ((2 * i) - 1)), false)
             :: compute_sub (i - 1)
         | i when i = k + 1 ->
-            let id = Coh (Builtin.id, [ (Var (Db ((2 * k) - 1)), false) ]) in
+            let id = Coh (Builtin.id (), [ (Var (Db ((2 * k) - 1)), false) ]) in
             (id, true) :: (Var (Db ((2 * k) - 1)), false) :: compute_sub k
         | i ->
             (Var (Db ((2 * i) - 2)), true)
@@ -96,7 +96,7 @@ let type_cell_max k =
             (Var (obj k), false);
             (Var (obj (k - 1)), false);
           ] ),
-      Coh (Builtin.id, [ (Var (obj (k - 1)), true) ]) )
+      Coh (Builtin.id (), [ (Var (obj (k - 1)), true) ]) )
 
 let rec ctx k =
   match k with
@@ -133,7 +133,7 @@ let rec subs_telescope_bdry ?(whisk = false) k =
           List.append left
             [
               (Var (cell_max k), true);
-              (Coh (Builtin.id, [ (Var (obj (k - 1)), true) ]), false);
+              (Coh (Builtin.id (), [ (Var (obj (k - 1)), true) ]), false);
               (src_max_var, false);
               (Var (obj (k - 1)), false);
             ] )
@@ -173,7 +173,7 @@ let rec telescope k =
       let sub_telescope =
         [
           (telescope (k - 1), true);
-          (Coh (Builtin.id, [ (tdb 0, true) ]), false);
+          (Coh (Builtin.id (), [ (tdb 0, true) ]), false);
           (m3, true);
           (tgt_m3, false);
           (m2, true);
diff --git a/lib/translate_raw.ml b/lib/translate_raw.ml
index 62c6229e..78be6d61 100644
--- a/lib/translate_raw.ml
+++ b/lib/translate_raw.ml
@@ -28,7 +28,7 @@ let rec tm t =
           (Unchecked.tm_apply_sub t s, meta_types))
   | Sub (BuiltinR b, s, susp, expl) ->
       let builtin_coh =
-        match b with Comp -> Builtin.comp s expl | Id -> Builtin.id
+        match b with Comp -> Builtin.comp s expl | Id -> Builtin.id ()
       in
       make_coh builtin_coh s susp expl
   | Op (l, t) ->

From e168adab4b04dc3ea60dca941185d3d74c2b313b Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 1 Oct 2024 11:33:26 +0100
Subject: [PATCH 5/5] update test oracles

---
 test.t/features/naturality.catt |  2 -
 test.t/run.t                    | 76 +++++++++++++++++----------------
 2 files changed, 39 insertions(+), 39 deletions(-)

diff --git a/test.t/features/naturality.catt b/test.t/features/naturality.catt
index 0821ffcf..8a7555cd 100644
--- a/test.t/features/naturality.catt
+++ b/test.t/features/naturality.catt
@@ -27,8 +27,6 @@ let exch (x : *) (y : *) (z : *)
          (a : f -> f') (b : g -> g')
          = whiskl [a] b
 
-# coh unbiase (x(f)y(g)z(h)w) : comp (comp f g) h -> (comp f g h)
-
 coh whiskl3 (x(f)y(g(a(m)b)h)z) : comp f [a] -> comp f [b]
 
 let nat_whiskl3 (x : *) (y : *) (z : *)
diff --git a/test.t/run.t b/test.t/run.t
index 1de76f54..a4051664 100644
--- a/test.t/run.t
+++ b/test.t/run.t
@@ -74,7 +74,7 @@
   [=^.^=] coh unbiase = (_builtin_comp  (_builtin_comp  f g) h) -> (_builtin_comp  f g h)
   [=I.I=] successfully defined unbiase.
   [=^.^=] coh unit_bis = (_builtin_comp  x y f y (_builtin_id  y)) -> f
-  [=I.I=] successfully defined unit_bis.
+  [=I.I=] successfully defined unit.
   [=^.^=] coh unbiase = (_builtin_comp  _ _ (_builtin_comp  _ _ f _ g) _ h) -> (_builtin_comp  _ _ f _ g _ h)
   [=I.I=] successfully defined unbiase.
 
@@ -120,6 +120,8 @@
   [=^.^=] coh simpl = (sq  (_builtin_id  x)) -> (_builtin_id  x)
   [=I.I=] inferring constraints for context:  (x: *).
   [=I.I=] context elaborated to  (x: *).
+  [=I.I=] checking coherence: builtin_id.
+  [=I.I=] checking coherence: builtin_id.
   [=I.I=] inferring constraints for type: _ty18 | (builtin_comp2 (builtin_id x) (builtin_id x)) -> (builtin_id x).
   [=I.I=] type elaborated to * | x -> x | (builtin_comp2 (builtin_id x) (builtin_id x)) -> (builtin_id x).
   [=I.I=] checking coherence: simpl.
@@ -168,19 +170,19 @@
   [=^.^=] let optest1 = op_{1}((test  c d a b))
   [=I.I=] successfully defined term (test_op{1} x y f f' a f'' b z g g' c g'' d) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
   [=^.^=] let optest2 = op_{2}((test  b a d c))
-  [=I.I=] successfully defined term (test_op{2} x y f f' a f'' b z g g' c g'' d) 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{1} x y f f' a f'' b z g g' c g'' d) 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} x y f f' a f'' b z g g' c g'' d) of type (builtin_comp2_op{1,2} x y f z g) -> (builtin_comp2_op{1,2} x y f'' z g'').
+  [=I.I=] successfully defined term (test_op{1} x y f f' a f'' b z g g' c g'' d) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
   [=^.^=] let nested1 = op_{1}((_builtin_comp  [(_builtin_comp  c d)] [(_builtin_comp  a b)]))
-  [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{1} x y f f'' (!1builtin_comp2_op{1} x y f f' a f'' b) z g g'' (!1builtin_comp2_op{1} y z g g' c g'' d)) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
+  [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{1} x y f f'' (!1builtin_comp2 x y f f' a f'' b) z g g'' (!1builtin_comp2 y z g g' c g'' d)) 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)]))
-  [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{2} x y f f'' (!1builtin_comp2_op{2} x y f f' a f'' b) z g g'' (!1builtin_comp2_op{2} y z g g' c g'' d)) 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 (builtin_comp2_func[1 1]_op{1} x y f f'' (!1builtin_comp2 x y f f' a f'' b) z g g'' (!1builtin_comp2 y z g g' c g'' d)) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
   [=^.^=] let nested12 = op_{1,2}((_builtin_comp  [(_builtin_comp  d c)] [(_builtin_comp  b a)]))
-  [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{1,2} x y f f'' (!1builtin_comp2_op{1,2} x y f f' a f'' b) z g g'' (!1builtin_comp2_op{1,2} y z g g' c g'' d)) of type (builtin_comp2_op{1,2} x y f z g) -> (builtin_comp2_op{1,2} x y f'' z g'').
+  [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{1} x y f f'' (!1builtin_comp2 x y f f' a f'' b) z g g'' (!1builtin_comp2 y z g g' c g'' d)) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
 
   $ catt features/inverses.catt
   [=^.^=] let id_inv = I((_builtin_id  x))
-  [=I.I=] successfully defined term (builtin_id^-1 x) of type x -> x.
+  [=I.I=] successfully defined term (builtin_id x) of type x -> x.
   [=^.^=] coh assoc = (_builtin_comp  (_builtin_comp  f g) h) -> (_builtin_comp  f (_builtin_comp  g h))
   [=I.I=] successfully defined assoc.
   [=^.^=] coh unbiase = (_builtin_comp  f (_builtin_comp  g h)) -> (_builtin_comp  f g h)
@@ -198,31 +200,31 @@
   [=^.^=] let unitl_inv = I((unitl  f))
   [=I.I=] successfully defined term (unitl^-1 f) of type f -> (builtin_comp2 (builtin_id x) f).
   [=^.^=] let assoc_unbiase_inv = I((_builtin_comp  (assoc  f f f) (unbiase  f f f)))
-  [=I.I=] successfully defined term (!1builtin_comp2_op{2} (unbiase^-1 f f f) (assoc^-1 f f f)) of type (builtin_comp3 f f f) -> (builtin_comp2 (builtin_comp2 f f) f).
+  [=I.I=] successfully defined term (!1builtin_comp2 (unbiase^-1 f f f) (assoc^-1 f f f)) of type (builtin_comp3 f f f) -> (builtin_comp2 (builtin_comp2 f f) f).
   [=^.^=] let id_id_inv = I((_builtin_comp  (_builtin_id  x) (_builtin_id  x)))
-  [=I.I=] successfully defined term (builtin_comp2_op{1} (builtin_id^-1 x) (builtin_id^-1 x)) of type x -> x.
+  [=I.I=] successfully defined term (builtin_comp2_op{1} (builtin_id x) (builtin_id x)) of type x -> x.
   [=^.^=] check I((_builtin_comp  (_builtin_id  x) [(_builtin_comp  (assoc  f f f) (unbiase  f f f))] (_builtin_id  x)))
-  [=I.I=] valid term (builtin_comp3_func[1]_op{2} (builtin_id x) (!1builtin_comp2_op{2} (unbiase^-1 f f f) (assoc^-1 f f f)) (builtin_id x)) of type (builtin_comp3_op{2} (builtin_id x) (builtin_comp3 f f f) (builtin_id x)) -> (builtin_comp3_op{2} (builtin_id x) (builtin_comp2 (builtin_comp2 f f) f) (builtin_id x)).
+  [=I.I=] valid term (builtin_comp3_func[1]_op{2} (builtin_id x) (!1builtin_comp2 (unbiase^-1 f f f) (assoc^-1 f f f)) (builtin_id x)) of type (builtin_comp3_op{2} (builtin_id x) (builtin_comp3 f f f) (builtin_id x)) -> (builtin_comp3_op{2} (builtin_id x) (builtin_comp2 (builtin_comp2 f f) f) (builtin_id x)).
   [=^.^=] check I((21comp  (assoc  f f f) (unbiase  f f f) (assoc  f f f)))
-  [=I.I=] valid term (21comp_op{2} (unbiase^-1 f f f) (assoc^-1 f f f) (assoc^-1 f f f)) of type (builtin_comp2_op{2} (builtin_comp3 f f f) (builtin_comp2 f (builtin_comp2 f f))) -> (builtin_comp2_op{2} (builtin_comp2 (builtin_comp2 f f) f) (builtin_comp2 (builtin_comp2 f f) f)).
+  [=I.I=] valid term (21comp_op{2} (unbiase^-1 f f f) (assoc^-1 f f f) (assoc^-1 f f f)) of type (builtin_comp2_op{1} (builtin_comp3 f f f) (builtin_comp2 f (builtin_comp2 f f))) -> (builtin_comp2_op{1} (builtin_comp2 (builtin_comp2 f f) f) (builtin_comp2 (builtin_comp2 f f) f)).
   [=^.^=] check I((2whisk  (_builtin_id  f) (_builtin_id  f) f))
-  [=I.I=] valid term (2whisk_op{2} (!1builtin_id^-1 f) (!1builtin_id^-1 f) f) of type (builtin_comp2_op{2} f f) -> (builtin_comp2_op{2} f f).
+  [=I.I=] valid term (2whisk_op{2} (!1builtin_id f) (!1builtin_id f) f) of type (builtin_comp2_op{1} f f) -> (builtin_comp2_op{1} f f).
   [=^.^=] check I((_builtin_comp  [(_builtin_comp  (assoc  (_builtin_id  f) (_builtin_id  f) (_builtin_id  f)) (unbiase  (_builtin_id  f) (_builtin_id  f) (_builtin_id  f)))] (_builtin_id  f)))
-  [=I.I=] valid term (!1builtin_comp2_func[1]_op{3} (!2builtin_comp2_op{3} (!1unbiase^-1 (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)) (!1assoc^-1 (!1builtin_id f) (!1builtin_id f) (!1builtin_id f))) (!1builtin_id f)) of type (!1builtin_comp2_op{3} (!1builtin_comp3 (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)) (!1builtin_id f)) -> (!1builtin_comp2_op{3} (!1builtin_comp2 (!1builtin_comp2 (!1builtin_id f) (!1builtin_id f)) (!1builtin_id f)) (!1builtin_id f)).
+  [=I.I=] valid term (!1builtin_comp2 [(!2builtin_comp2 (!1unbiase^-1 (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)) (!1assoc^-1 (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)))] (!1builtin_id f)) of type (!1builtin_comp2 (!1builtin_comp3 (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)) (!1builtin_id f)) -> (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 (!1builtin_id f) (!1builtin_id f)) (!1builtin_id f)) (!1builtin_id f)).
   [=^.^=] check I((_builtin_comp  [(_builtin_comp  (assoc  f f f) (unbiase  f f f))] (_builtin_comp  (_builtin_id  x) I((_builtin_id  x))) [I((_builtin_comp  (_builtin_id  g) (_builtin_id  g)))] (_builtin_id  y)))
-  [=I.I=] valid term (builtin_comp4_func[1 1]_op{2} (!1builtin_comp2_op{2} (unbiase^-1 f f f) (assoc^-1 f f f)) (builtin_comp2 (builtin_id x) (builtin_id^-1 x)) (!1builtin_comp2_op{2}_op{2} (!1builtin_id^-1^-1 g) (!1builtin_id^-1^-1 g)) (builtin_id y)) of type (builtin_comp4_op{2} (builtin_comp3 f f f) (builtin_comp2 (builtin_id x) (builtin_id^-1 x)) g (builtin_id y)) -> (builtin_comp4_op{2} (builtin_comp2 (builtin_comp2 f f) f) (builtin_comp2 (builtin_id x) (builtin_id^-1 x)) g (builtin_id y)).
+  [=I.I=] valid term (builtin_comp4_func[1 1]_op{2} (!1builtin_comp2 (unbiase^-1 f f f) (assoc^-1 f f f)) (builtin_comp2 (builtin_id x) (builtin_id x)) (!1builtin_comp2 (!1builtin_id g) (!1builtin_id g)) (builtin_id y)) of type (builtin_comp4_op{2} (builtin_comp3 f f f) (builtin_comp2 (builtin_id x) (builtin_id x)) g (builtin_id y)) -> (builtin_comp4_op{2} (builtin_comp2 (builtin_comp2 f f) f) (builtin_comp2 (builtin_id x) (builtin_id x)) g (builtin_id y)).
   [=^.^=] check I((assoc  x y f z g w h))
   [=I.I=] valid term (assoc^-1 f g h) of type (builtin_comp2 f (builtin_comp2 g h)) -> (builtin_comp2 (builtin_comp2 f g) h).
   [=^.^=] check U((assoc  f g h))
   [=I.I=] valid term (assoc_Unit f g h) of type (!1builtin_comp2 (builtin_comp2 (builtin_comp2 f g) h) (builtin_comp2 f (builtin_comp2 g h)) (assoc f g h) (assoc^-1 f g h)) -> (!1builtin_id (builtin_comp2 (builtin_comp2 f g) h)).
   [=^.^=] check U((_builtin_comp  (_builtin_id  f) (_builtin_id  f)))
-  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (!1builtin_id f) (!1builtin_id f) (!1builtin_id^-1 f) (!1builtin_id^-1 f)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (!1builtin_id f) (!1builtin_id f) (!1builtin_id^-1 f) (!1builtin_id^-1 f)) (!1builtin_comp3 (!1builtin_id f) (!1builtin_id_Unit f) (!1builtin_id^-1 f)) (!1unit (!1builtin_id f) (!1builtin_id^-1 f)) (!1builtin_id_Unit f))]) (unbiased_unitor f)) of type (!1builtin_comp2 (!1builtin_comp2 (!1builtin_id f) (!1builtin_id f)) (!1builtin_comp2_op{2} (!1builtin_id^-1 f) (!1builtin_id^-1 f))) -> (!1builtin_id f).
+  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (!1builtin_id f) (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (!1builtin_id f) (!1builtin_id f) (!1builtin_id f) (!1builtin_id f)) (!1builtin_comp3 (!1builtin_id f) (!1builtin_id_Unit f) (!1builtin_id f)) (!1unit (!1builtin_id f) (!1builtin_id f)) (!1builtin_id_Unit f))]) (unbiased_unitor f)) of type (!1builtin_comp2 (!1builtin_comp2 (!1builtin_id f) (!1builtin_id f)) (!1builtin_comp2 (!1builtin_id f) (!1builtin_id f))) -> (!1builtin_id f).
   [=^.^=] check U((_builtin_comp  [(_builtin_id  f)] [(_builtin_id  g)]))
-  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (!1builtin_id f) (!1builtin_id^-1 f) (!1builtin_id g) (!1builtin_id^-1 g)) (unbiased_comp_red [(!1builtin_id_Unit f)] [(!1builtin_id_Unit g)]) (unbiased_unitor f g)) of type (!1builtin_comp2 (builtin_comp2 [(!1builtin_id f)] [(!1builtin_id g)]) (builtin_comp2_func[1 1]_op{2} (!1builtin_id^-1 f) (!1builtin_id^-1 g))) -> (!1builtin_id (builtin_comp2 f g)).
+  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (!1builtin_id f) (!1builtin_id f) (!1builtin_id g) (!1builtin_id g)) (unbiased_comp_red [(!1builtin_id_Unit f)] [(!1builtin_id_Unit g)]) (unbiased_unitor f g)) of type (!1builtin_comp2 (builtin_comp2 [(!1builtin_id f)] [(!1builtin_id g)]) (builtin_comp2_func[1 1]_op{2} (!1builtin_id f) (!1builtin_id g))) -> (!1builtin_id (builtin_comp2 f g)).
   [=^.^=] check U((_builtin_comp  (assoc  f f f) (unbiase  f f f)))
-  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (assoc f f f) (unbiase f f f) (unbiase^-1 f f f) (assoc^-1 f f f)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (assoc f f f) (unbiase f f f) (unbiase^-1 f f f) (assoc^-1 f f f)) (!1builtin_comp3 (assoc f f f) (unbiase_Unit f f f) (assoc^-1 f f f)) (!1unit (assoc f f f) (assoc^-1 f f f)) (assoc_Unit f f f))]) (unbiased_unitor (builtin_comp2 (builtin_comp2 f f) f))) of type (!1builtin_comp2 (!1builtin_comp2 (assoc f f f) (unbiase f f f)) (!1builtin_comp2_op{2} (unbiase^-1 f f f) (assoc^-1 f f f))) -> (!1builtin_id (builtin_comp2 (builtin_comp2 f f) f)).
+  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (assoc f f f) (unbiase f f f) (unbiase^-1 f f f) (assoc^-1 f f f)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (assoc f f f) (unbiase f f f) (unbiase^-1 f f f) (assoc^-1 f f f)) (!1builtin_comp3 (assoc f f f) (unbiase_Unit f f f) (assoc^-1 f f f)) (!1unit (assoc f f f) (assoc^-1 f f f)) (assoc_Unit f f f))]) (unbiased_unitor (builtin_comp2 (builtin_comp2 f f) f))) of type (!1builtin_comp2 (!1builtin_comp2 (assoc f f f) (unbiase f f f)) (!1builtin_comp2 (unbiase^-1 f f f) (assoc^-1 f f f))) -> (!1builtin_id (builtin_comp2 (builtin_comp2 f f) f)).
   [=^.^=] check U((_builtin_comp  (assoc  f f g) (_builtin_id  (_builtin_comp  f (_builtin_comp  f g))) (unbiase  f f g) I((unbiase  f f g))))
-  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (unbiase^-1^-1 f f g) (unbiase^-1 f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (unbiase^-1^-1 f f g) (unbiase^-1 f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1builtin_comp7 (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1_Unit f f g) (unbiase^-1 f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1unit (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!2builtin_comp4 (!1focus (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1builtin_comp5 (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase_Unit f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1unit (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!2builtin_comp4 (!1focus (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1builtin_comp3 (assoc f f g) (!1builtin_id_Unit (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1unit (assoc f f g) (assoc^-1 f f g)) (assoc_Unit f f g))))]) (unbiased_unitor (builtin_comp2 (builtin_comp2 f f) g))) of type (!1builtin_comp2 (!1builtin_comp4 (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g)) (!1builtin_comp4_op{2} (unbiase^-1^-1 f f g) (unbiase^-1 f f g) (!1builtin_id^-1 (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g))) -> (!1builtin_id (builtin_comp2 (builtin_comp2 f f) g)).
+  [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1builtin_comp7 (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1_Unit f f g) (unbiase^-1 f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1unit (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!2builtin_comp4 (!1focus (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1builtin_comp5 (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase_Unit f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1unit (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!2builtin_comp4 (!1focus (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1builtin_comp3 (assoc f f g) (!1builtin_id_Unit (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g)) (!1unit (assoc f f g) (assoc^-1 f f g)) (assoc_Unit f f g))))]) (unbiased_unitor (builtin_comp2 (builtin_comp2 f f) g))) of type (!1builtin_comp2 (!1builtin_comp4 (assoc f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (unbiase f f g) (unbiase^-1 f f g)) (!1builtin_comp4 (unbiase f f g) (unbiase^-1 f f g) (!1builtin_id (builtin_comp2 f (builtin_comp2 f g))) (assoc^-1 f f g))) -> (!1builtin_id (builtin_comp2 (builtin_comp2 f f) g)).
   [=^.^=] check U((21comp  (assoc  f f f) (unbiase  f f f) (assoc  g g g)))
   [=I.I=] valid term (!2builtin_comp3 (vertical_grouping (assoc f f f) (unbiase f f f) (unbiase^-1 f f f) (assoc^-1 f f f) (assoc g g g) (assoc^-1 g g g)) (unbiased_comp_red [(!2builtin_comp4 (!1focus (assoc f f f) (unbiase f f f) (unbiase^-1 f f f) (assoc^-1 f f f)) (!1builtin_comp3 (assoc f f f) (unbiase_Unit f f f) (assoc^-1 f f f)) (!1unit (assoc f f f) (assoc^-1 f f f)) (assoc_Unit f f f))] [(assoc_Unit g g g)]) (unbiased_unitor (builtin_comp2 (builtin_comp2 f f) f) (builtin_comp2 (builtin_comp2 g g) g))) of type (!1builtin_comp2 (21comp (assoc f f f) (unbiase f f f) (assoc g g g)) (21comp_op{2} (unbiase^-1 f f f) (assoc^-1 f f f) (assoc^-1 g g g))) -> (!1builtin_id (builtin_comp2 (builtin_comp2 (builtin_comp2 f f) f) (builtin_comp2 (builtin_comp2 g g) g))).
 
@@ -240,43 +242,43 @@
   [=^.^=] let nat_assoc = (assoc  [a] [b] [c])
   [=I.I=] successfully defined term (assoc [a] [b] [c]) of type (!1builtin_comp2 (assoc f g h) (builtin_comp2 [a] [(builtin_comp2 [b] [c])])) -> (!1builtin_comp2 (builtin_comp2 [(builtin_comp2 [a] [b])] [c]) (assoc f' g' h')).
   [=^.^=] let whiskL = (_builtin_comp  f [a])
-  [=I.I=] successfully defined term (builtin_comp2 f [a]) of type (builtin_comp2 f g) -> (builtin_comp2 f h).
+  [=I.I=] successfully defined term (whiskl f a) of type (builtin_comp2 f g) -> (builtin_comp2 f h).
   [=^.^=] let nat_assoc = (assoc  [a] [[B]] [c])
   [=I.I=] successfully defined term (assoc [a] [[B]] [c]) of type (!2builtin_comp2 (assoc [a] [b] [c]) (!1builtin_comp2 [(builtin_comp2 [[(builtin_comp2 [a] [[B]])]] [c])] (assoc f' g' h'))) -> (!2builtin_comp2 (!1builtin_comp2 (assoc f g h) [(builtin_comp2 [a] [[(builtin_comp2 [[B]] [c])]])]) (assoc [a] [b'] [c])).
   [=^.^=] let exch = (whiskl  [a] b)
   [=I.I=] successfully defined term (whiskl [a] b) of type (!1builtin_comp2 (whiskl f b) (builtin_comp2 [a] g')) -> (!1builtin_comp2 (builtin_comp2 [a] g) (whiskl f' b)).
   [=^.^=] coh whiskl3 = (_builtin_comp  f [a]) -> (_builtin_comp  f [b])
-  [=I.I=] successfully defined whiskl3.
+  [=I.I=] successfully defined whiskl.
   [=^.^=] let nat_whiskl3 = (whiskl3  [c] m)
-  [=I.I=] successfully defined term (whiskl3 [c] m) of type (!2builtin_comp2 (!1builtin_comp2 (whiskl3 f m) (builtin_comp2 [c] h)) (builtin_comp2 [c] [b])) -> (!2builtin_comp2 (builtin_comp2 [c] [a]) (!1builtin_comp2 (builtin_comp2 [c] g) (whiskl3 f' m))).
+  [=I.I=] successfully defined term (whiskl [c] [m]) of type (!2builtin_comp2 (!1builtin_comp2 [(whiskl f [m])] (builtin_comp2 [c] h)) (whiskl [c] b)) -> (!2builtin_comp2 (whiskl [c] a) (!1builtin_comp2 (builtin_comp2 [c] g) [(whiskl f' [m])])).
   [=^.^=] coh whiskl4 = (_builtin_comp  f [[[p]]]) -> (_builtin_comp  f [[[p]]])
   [=I.I=] successfully defined whiskl4.
   [=^.^=] coh id2 = (_builtin_comp  (_builtin_id  x) (_builtin_id  x) (_builtin_id  x)) -> (_builtin_comp  (_builtin_id  x))
   [=I.I=] successfully defined id2.
   [=^.^=] let nat_id2 = (id2  [f])
-  [=I.I=] successfully defined term (id2 [f]) of type (!1builtin_comp2 (builtin_comp2 [(id2 x)] f) (!1builtin_comp3 (intch_src (builtin_id x) f) (builtin_comp1_red [(builtin_id [f])]) (intch_tgt f (builtin_id y)))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src (builtin_id x) (builtin_id x) (builtin_id x) f) (builtin_comp3_red [(!1builtin_comp7 (builtin_assc (builtin_id x) (builtin_id x) (builtin_id x) f) (builtin_comp3 (builtin_id x) (builtin_id x) [(builtin_id [f])]) (builtin_assc (builtin_id x) (builtin_id x) f (builtin_id y)) (builtin_comp3 (builtin_id x) [(builtin_id [f])] (builtin_id y)) (builtin_assc (builtin_id x) f (builtin_id y) (builtin_id y)) (builtin_comp3 [(builtin_id [f])] (builtin_id y) (builtin_id y)) (builtin_assc f (builtin_id y) (builtin_id y) (builtin_id y)))]) (intch_tgt f (builtin_id y) (builtin_id y) (builtin_id y))) (builtin_comp2 f [(id2 y)])).
+  [=I.I=] successfully defined term (id2 [f]) of type (!1builtin_comp2 (builtin_comp2 [(id2 x)] f) (!1builtin_comp3 (intch_src (builtin_id x) f) (builtin_comp1 [(builtin_id [f])]) (intch_tgt f (builtin_id y)))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src (builtin_id x) (builtin_id x) (builtin_id x) f) (builtin_comp1 [(!1builtin_comp7 (builtin_assc (builtin_id x) (builtin_id x) (builtin_id x) f) (builtin_comp3 (builtin_id x) (builtin_id x) [(builtin_id [f])]) (builtin_assc (builtin_id x) (builtin_id x) f (builtin_id y)) (builtin_comp3 (builtin_id x) [(builtin_id [f])] (builtin_id y)) (builtin_assc (builtin_id x) f (builtin_id y) (builtin_id y)) (builtin_comp3 [(builtin_id [f])] (builtin_id y) (builtin_id y)) (builtin_assc f (builtin_id y) (builtin_id y) (builtin_id y)))]) (intch_tgt f (builtin_id y) (builtin_id y) (builtin_id y))) (whiskl f (id2 y))).
   [=^.^=] coh vcompwhisk = (_builtin_comp  (_builtin_id  x) f g) -> (_builtin_comp  f (_builtin_id  y) k)
   [=I.I=] successfully defined vcompwhisk.
   [=^.^=] let vcompwhisk2 = (vcompwhisk  f (_builtin_id  g) (_builtin_id  g))
   [=I.I=] successfully defined term (vcompwhisk f (!1builtin_id g) (!1builtin_id g)) of type (builtin_comp3 (builtin_id x) f g) -> (builtin_comp3 f (builtin_id y) g).
   [=^.^=] let nat_vcompwhisk = (vcompwhisk2  [a] [c])
-  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src f a (!1builtin_id g) (!1builtin_id g) c) (vcompwhisk_red a [(!2builtin_comp5 (!1builtin_assc (!1builtin_id g) (!1builtin_id g) c) (!1builtin_comp2 (!1builtin_id g) (!1builtin_id [c])) (!1builtin_assc (!1builtin_id g) c (!1builtin_id g')) (!1builtin_comp2 (!1builtin_id [c]) (!1builtin_id g')) (!1builtin_assc c (!1builtin_id g') (!1builtin_id g')))]) (intch_tgt a c (!1builtin_id g') (!1builtin_id g'))) of type (!1builtin_comp2 (vcompwhisk f (!1builtin_id g) (!1builtin_id g)) (builtin_comp3 [a] (builtin_id y) [c])) -> (!1builtin_comp2 (builtin_comp3 (builtin_id x) [a] [c]) (vcompwhisk f' (!1builtin_id g') (!1builtin_id g'))).
+  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src f a (!1builtin_id g) (!1builtin_id g) c) (vcompwhisk_red a [(!2builtin_comp5 (!1builtin_assc (!1builtin_id g) (!1builtin_id g) c) (!1builtin_comp2 (!1builtin_id g) [(!1builtin_id [c])]) (!1builtin_assc (!1builtin_id g) c (!1builtin_id g')) (!1builtin_comp2 [(!1builtin_id [c])] (!1builtin_id g')) (!1builtin_assc c (!1builtin_id g') (!1builtin_id g')))]) (intch_tgt a c (!1builtin_id g') (!1builtin_id g'))) of type (!1builtin_comp2 (vcompwhisk f (!1builtin_id g) (!1builtin_id g)) (builtin_comp3 [a] (builtin_id y) [c])) -> (!1builtin_comp2 (builtin_comp3 (builtin_id x) [a] [c]) (vcompwhisk f' (!1builtin_id g') (!1builtin_id g'))).
   [=^.^=] let triangle1 = (_builtin_comp  x [ym] [fm] z [gm])
-  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g) (builtin_comp2_red [(!1builtin_comp3 (builtin_comp2 f [gm]) (builtin_assc f ym g') (builtin_comp2 [fm] g'))]) (intch_tgt x f' g')) of type (builtin_comp2 f g) -> (builtin_comp2 f' g').
+  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g) (builtin_comp1 [(!1builtin_comp3 (whiskl f gm) (builtin_assc f ym g') (builtin_comp2 [fm] g'))]) (intch_tgt x f' g')) of type (builtin_comp2 f g) -> (builtin_comp2 f' g').
   [=^.^=] let triangle2 = (_builtin_comp  [xm] y [fm] [zm] [gm])
-  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g zm) (builtin_comp2_red [(!1builtin_comp4 (builtin_assc f g zm) (builtin_comp2 f [gm]) (builtin_comp2 [fm] g') (builtin_assc xm f' g'))]) (intch_tgt xm f' g')) of type (builtin_comp2 (builtin_comp2 f g) zm) -> (builtin_comp2 xm (builtin_comp2 f' g')).
+  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g zm) (builtin_comp1 [(!1builtin_comp4 (builtin_assc f g zm) (whiskl f gm) (builtin_comp2 [fm] g') (builtin_assc xm f' g'))]) (intch_tgt xm f' g')) of type (builtin_comp2 (builtin_comp2 f g) zm) -> (builtin_comp2 xm (builtin_comp2 f' g')).
   [=^.^=] let triangle1_bis = (@_builtin_comp  _ [_] [fm] _ [gm])
-  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g) (builtin_comp2_red [(!1builtin_comp3 (builtin_comp2 f [gm]) (builtin_assc f ym g') (builtin_comp2 [fm] g'))]) (intch_tgt x f' g')) of type (builtin_comp2 f g) -> (builtin_comp2 f' g').
+  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g) (builtin_comp1 [(!1builtin_comp3 (whiskl f gm) (builtin_assc f ym g') (builtin_comp2 [fm] g'))]) (intch_tgt x f' g')) of type (builtin_comp2 f g) -> (builtin_comp2 f' g').
   [=^.^=] let triangle2_bis = (@_builtin_comp  [_] _ [fm] [_] [gm])
-  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g zm) (builtin_comp2_red [(!1builtin_comp4 (builtin_assc f g zm) (builtin_comp2 f [gm]) (builtin_comp2 [fm] g') (builtin_assc xm f' g'))]) (intch_tgt xm f' g')) of type (builtin_comp2 (builtin_comp2 f g) zm) -> (builtin_comp2 xm (builtin_comp2 f' g')).
+  [=I.I=] successfully defined term (!1builtin_comp3 (intch_src f g zm) (builtin_comp1 [(!1builtin_comp4 (builtin_assc f g zm) (whiskl f gm) (builtin_comp2 [fm] g') (builtin_assc xm f' g'))]) (intch_tgt xm f' g')) of type (builtin_comp2 (builtin_comp2 f g) zm) -> (builtin_comp2 xm (builtin_comp2 f' g')).
   [=^.^=] coh example = (_builtin_comp  f k (_builtin_id  z)) -> (_builtin_comp  h l)
   [=I.I=] successfully defined example.
   [=^.^=] let ex1 = (@example  _ _ _ [_] [am] [_] [bm] _ _ [_] [cm])
-  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src a b hm c lm) (example_red [(!2builtin_comp4 (!1builtin_assc a b hm) (!1builtin_comp2 a bm) (!1builtin_assc a gm b+) (!1builtin_comp2 am b+))] [cm]) (intch_tgt f a+ b+ k c+)) of type (!1builtin_comp2 (example a b c) (builtin_comp2 [hm] [lm])) -> (example a+ b+ c+).
+  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src a b hm c lm) (example_red [(!2builtin_comp4 (!1builtin_assc a b hm) (!1builtin_comp2 a [bm]) (!1builtin_assc a gm b+) (!1builtin_comp2 [am] b+))] [cm]) (intch_tgt f a+ b+ k c+)) of type (!1builtin_comp2 (example a b c) (builtin_comp2 [hm] [lm])) -> (example a+ b+ c+).
   [=^.^=] let ex2 = (@example  _ _ _ [_] [am] [_] [bm] _ [_] _ [cm])
-  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src a b hm c) (example_red [(!2builtin_comp4 (!1builtin_assc a b hm) (!1builtin_comp2 a bm) (!1builtin_assc a gm b+) (!1builtin_comp2 am b+))] [cm]) (intch_tgt f a+ b+ km c+)) of type (!1builtin_comp2 (example a b c) (builtin_comp2 [hm] l)) -> (!1builtin_comp2 (builtin_comp3 f [km] (builtin_id z)) (example a+ b+ c+)).
+  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src a b hm c) (example_red [(!2builtin_comp4 (!1builtin_assc a b hm) (!1builtin_comp2 a [bm]) (!1builtin_assc a gm b+) (!1builtin_comp2 [am] b+))] [cm]) (intch_tgt f a+ b+ km c+)) of type (!1builtin_comp2 (example a b c) (builtin_comp2 [hm] l)) -> (!1builtin_comp2 (builtin_comp3 f [km] (builtin_id z)) (example a+ b+ c+)).
   [=^.^=] let ex3 = (@example  _ _ _ [_] [am] [_] [bm] _ [_] [_] [cm])
-  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src a b hm c lm) (example_red [(!2builtin_comp4 (!1builtin_assc a b hm) (!1builtin_comp2 a bm) (!1builtin_assc a gm b+) (!1builtin_comp2 am b+))] [cm]) (intch_tgt f a+ b+ km c+)) of type (!1builtin_comp2 (example a b c) (builtin_comp2 [hm] [lm])) -> (!1builtin_comp2 (builtin_comp3 f [km] (builtin_id z)) (example a+ b+ c+)).
+  [=I.I=] successfully defined term (!2builtin_comp3 (intch_src a b hm c lm) (example_red [(!2builtin_comp4 (!1builtin_assc a b hm) (!1builtin_comp2 a [bm]) (!1builtin_assc a gm b+) (!1builtin_comp2 [am] b+))] [cm]) (intch_tgt f a+ b+ km c+)) of type (!1builtin_comp2 (example a b c) (builtin_comp2 [hm] [lm])) -> (!1builtin_comp2 (builtin_comp3 f [km] (builtin_id z)) (example a+ b+ c+)).
 
   $ catt --keep-going fails/notps.catt
   [=^.^=] coh fail1 = x -> x
@@ -306,13 +308,13 @@
   $ catt --keep-going fails/invalidcoherences.catt
   [=^.^=] coh fail1 = x -> x
   [=X.X=] The coherence fail1 is not valid for the following reason:
-  type .0 -> .0 not full in pasting scheme  {.0: *} {.1: *} (.2: .0 -> .1)
+  type .0 -> .0 not algebraic in pasting scheme  {.0: *} {.1: *} (.2: .0 -> .1)
   [=^.^=] coh fail2 = x -> z
   [=X.X=] The coherence fail2 is not valid for the following reason:
-  type .0 -> .5 not full in pasting scheme  {.0: *} {.1: *} {.2: .0 -> .1} {.3: .0 -> .1} (.4: .2 -> .3) {.5: *} {.6: .1 -> .5} {.7: .1 -> .5} (.8: .6 -> .7)
+  type .0 -> .5 not algebraic in pasting scheme  {.0: *} {.1: *} {.2: .0 -> .1} {.3: .0 -> .1} (.4: .2 -> .3) {.5: *} {.6: .1 -> .5} {.7: .1 -> .5} (.8: .6 -> .7)
   [=^.^=] coh fail3 = f -> g
   [=X.X=] The coherence fail3 is not valid for the following reason:
-  type .2 -> .3 not full in pasting scheme  {.0: *} {.1: *} {.2: .0 -> .1} {.3: .0 -> .1} (.4: .2 -> .3) {.5: *} {.6: .1 -> .5} {.7: .1 -> .5} (.8: .6 -> .7)
+  type .2 -> .3 not algebraic in pasting scheme  {.0: *} {.1: *} {.2: .0 -> .1} {.3: .0 -> .1} (.4: .2 -> .3) {.5: *} {.6: .1 -> .5} {.7: .1 -> .5} (.8: .6 -> .7)
 
   $ catt --keep-going fails/invalidtypes.catt
   [=^.^=] coh fail1 = x -> f
@@ -338,7 +340,7 @@
   [=X.X=] The constraints generated for the term: (whisk f b) could not be solved for the following reason:
   could not unify * and _tm13 -> _tm12
   [=^.^=] let fail3 = (_builtin_comp  [f] b)
-  [=X.X=] The constraints generated for the term: (builtin_comp2 [f] b) could not be solved for the following reason:
+  [=X.X=] The constraints generated for the term: (whisk f b) could not be solved for the following reason:
   could not unify * and _tm18 -> _tm17
   [=^.^=] let fail4 = (_builtin_comp  [f] g)
   [=X.X=] The constraints generated for the term: (builtin_comp2 [f] g) could not be solved for the following reason:
@@ -346,7 +348,7 @@
 
   $ catt --keep-going fails/invalidnaturality.catt
   [=^.^=] let fail1 = (@_builtin_comp  x [f] f x f)
-  [=X.X=] The constraints generated for the term: (!1builtin_comp3 (intch_src f f) (!-1builtin_comp2_red [(!1builtin_comp1 (builtin_assc f f f))]) (intch_tgt x f f)) could not be solved for the following reason:
+  [=X.X=] The constraints generated for the term: (!1builtin_comp3 (intch_src f f) (!-1builtin_comp2_red [(!1!-1builtin_comp2_red (builtin_assc f f f))]) (intch_tgt x f f)) could not be solved for the following reason:
   could not unify (builtin_comp2 f f) and f
   [=^.^=] coh whisk = (_builtin_comp  [a] h) -> (_builtin_comp  [b] h)
   [=I.I=] successfully defined whisk.
@@ -621,6 +623,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^-1_op{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) (!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)]) (!1builtin_comp3_func[1 1 1]_op{1}_op{3} (Ilsimp_op{1}^-1 x) (!2builtin_comp2_op{1}_op{3} (exch_op{1}^-1 b a) (!1builtin_comp3_func[1]_op{1}_op{3} (builtin_comp2_func[1]_op{1} b (builtin_id_op{1} x)) (!2builtin_comp2_op{1}_op{3} (unit_Unit_op{1}^-1 x) (!1builtin_comp2_func[1 1]_op{1}_op{3} (lsimp_op{1}^-1 x) (Ilsimp_op{1}_op{1}^-1 x))) (builtin_comp2_func[1]_op{1} (builtin_id_op{1} x) a))) (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) (!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)]) (!1builtin_comp3 [(Ilsimp_op{1}^-1 x)] [(!2builtin_comp2 (exch_op{1}^-1 b a) (!1builtin_comp3 (builtin_comp2_func[1]_op{1} b (builtin_id x)) [(!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[1]_op{1} (builtin_id x) a)))] [(lsimp_op{1}_op{1}^-1 x)]) (eh1_op{1}^-1 b a)) of type (!1builtin_comp2 a b) -> (!1builtin_comp2 b a).