From 39c898847f28267846cf131558babfbee548c627 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Mon, 5 Apr 2021 10:58:07 +0100
Subject: [PATCH 01/14] First attempt at insertion operation

---
 lib/eval.ml  | 99 ++++++++++++++++++++++++++++++++++++++++++++++++++--
 lib/pd.ml    | 38 ++++++++++++++++++++
 lib/suite.ml | 31 ++++++++++++++++
 lib/value.ml | 16 +++++++++
 4 files changed, 182 insertions(+), 2 deletions(-)

diff --git a/lib/eval.ml b/lib/eval.ml
index f972704..e11936e 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -11,6 +11,7 @@ open Value
 open Suite
 open Syntax
 open Cylinder
+open Pd
 
 (*****************************************************************************)
 (*                                 Evaluation                                *)
@@ -83,10 +84,104 @@ and appV t u ict =
   | LamV (_,_,cl) -> cl $$ u
   | UCompV (ucd,cohv,sp) -> UCompV (ucd,appV cohv u ict,AppSp(sp,u,ict))
   | CohV (cn,pd,c,s,t,sp) ->
-    CohV (cn,pd,c,s,t,AppSp(sp,u,ict))
-
+     let sp' = AppSp(sp,u,ict) in
+     let x = CohV (cn,pd,c,s,t,sp') in
+     if sp_length sp' = pd_length pd + 1 then
+       (match redCoh cn pd c s t sp' with
+       | Error _ -> x
+       | Ok y -> y) else x
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
 
+and redCoh cn pd c s t sp =
+
+  let rec dim_ty ty =
+    match ty with
+    | HomV (c,_,_) -> dim_ty c + 1
+    | _ -> 0 in
+
+  let rec type_linearity v =
+    match force_meta v with
+    | HomV(c, RigidV _, RigidV _) -> dim_ty c
+    | HomV(c, _, _) -> type_linearity c
+    | _ -> -1 in
+
+  let rec get_redex xs =
+    match xs with
+    | Emp -> Error "No redex found"
+    | Ext (xs, ((_,_,_,_,CohV (cn', pd', c', s', t', sp')), redex_path)) ->
+       let args = sp_to_suite sp' in
+       let pda = map_pd_lvls pd' 0 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (false, n , nm , ict, v)) in
+       if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
+    | _ -> get_redex xs in
+
+  let get_internal_substitution pd =
+    let l = Pd.labels pd in
+    let fl = filter (zip_with_idx l) (fun (_,(b,_,_,_,_)) -> not b) in
+    map_suite_m (range_r 0 (length fl)) ~f:(fun n ->
+        let* (x,(_,_,_,icit,_)) = find fl ~p:(fun (_,(_,i,_,_,_)) -> i = n) in
+        Ok ((RigidV (x,EmpSp),icit))) in
+
+  let path_from_term_type tm ty path =
+    let pl = length path in
+    let ty_dim = dim_ty ty in
+    let b = (last path = 1) in
+    let d = ty_dim - pl in
+    let rec go d ty =
+      match ty with
+      | HomV (c,s,t) -> if d > 0 then go (d-1) c else if b then Ok t else Ok s
+      | _ -> Error "Internal error: path_from_term_type" in
+    if pl > ty_dim then Ok tm else go d ty in
+
+  let rec subtract_path path1 path2 =
+    match (path1, path2) with
+    | (Emp, _) -> Emp
+    | (Ext (xs, x), Emp) -> Ext (xs, x)
+    | (Ext (xs, x), Ext (ys, y)) -> Ext (subtract_path xs ys, x - y) in
+
+  let get_external_substitution pd redex_path all_paths internal_tm internal_ty =
+    let l = Pd.labels pd in
+    let fl = filter (zip_with_idx l) (fun (_,(b,_,_,_,_)) -> b) in
+    map_suite_m (range 0 (length all_paths)) ~f:(fun n ->
+        match find fl ~p:(fun (_,(_,i,_,_,_)) -> i = n) with
+        | Error _ ->
+           let path = subtract_path (db_get n all_paths) redex_path in
+           let* t = path_from_term_type internal_tm internal_ty path in
+           Ok (t)
+        | Ok (x,_) -> Ok (RigidV (x,EmpSp))) in
+
+  let ctx_length = pd_length pd + 1 in
+  let (cat_arg, args) = split_suite 1 (sp_to_suite sp) in
+  let pd_with_args = map_pd_lvls pd 0 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (true, n, nm, ict, v)) in
+
+  match loc_max_bh pd_with_args with
+  | Error _ -> Error "Pd is linear"
+  | Ok xs ->
+     let* (cni,pdi,ci,si,ti,redex_pd,redex_path) = get_redex xs in
+     let internal_ctx_length = pd_length pdi + 1 in
+     let internal_term = CohV(cni,pdi,ci,si,ti,EmpSp) in
+     let* pd_insert = insertion pd_with_args redex_path redex_pd in
+     let pd_final = map_pd pd_insert ~f:(fun (_,_,nm,icit,_) -> (nm,icit)) in
+     let final_args = labels (map_pd pd_insert ~f:(fun (_,_,_,icit,v) -> (v,icit))) in
+     let final_spine = suite_to_sp (append cat_arg final_args) in
+     let inserted_ctx_length = pd_length pd_insert + 1 in
+     let* internal_sub_no_append = get_internal_substitution pd_insert in
+     let internal_sub = append (singleton (RigidV (inserted_ctx_length, EmpSp), (snd cni))) internal_sub_no_append in
+     let internal_term_subbed = runSpV internal_term (suite_to_sp internal_sub) in
+     let internal_sub_no_icit = map_suite internal_sub ~f:fst in
+     let civ = applySubstitution internal_ctx_length ci internal_sub_no_icit in
+     let siv = applySubstitution internal_ctx_length si internal_sub_no_icit in
+     let tiv = applySubstitution internal_ctx_length ti internal_sub_no_icit in
+     let* external_sub_no_append = get_external_substitution pd_insert redex_path (get_all_paths pd) internal_term_subbed (HomV (civ,siv,tiv)) in
+     let external_sub = append (singleton (RigidV (inserted_ctx_length,EmpSp))) external_sub_no_append in
+     let cv = applySubstitution ctx_length c external_sub in
+     let sv = applySubstitution ctx_length s external_sub in
+     let tv = applySubstitution ctx_length t external_sub in
+     Ok (runSpV (CohV(cn,pd_final,cv,sv,tv,EmpSp)) final_spine)
+
+and applySubstitution k v sub =
+  let t = quote true k v in
+  eval Emp sub t
+
 and baseV v =
   match v with
   | FlexV (m,sp) -> FlexV (m,BaseSp sp)
diff --git a/lib/pd.ml b/lib/pd.ml
index 439cd1e..eeec329 100644
--- a/lib/pd.ml
+++ b/lib/pd.ml
@@ -105,6 +105,44 @@ let rec zip_with_addr_lcl addr pd =
 let zip_with_addr pd =
   zip_with_addr_lcl Emp pd
 
+let rec loc_max_bh pd =
+  match pd with
+  | Br (x , Emp) -> Error x
+  | Br (_ , Ext (Emp , (_ , p))) ->
+     (match loc_max_bh p with
+      | Error x -> Error x
+      | Ok xs -> Ok (map_suite xs ~f:(fun (x,xs) -> (x, Ext (xs,0)))))
+  | Br (_ , brs) ->
+     let rs = map_with_lvl brs ~f:(fun i (_,p) ->
+                  match loc_max_bh p with
+                  | Error x -> Ext (Emp, (x,Ext (Emp, i)))
+                  | Ok xs -> map_suite xs ~f:(fun (x,xs) -> (x, Ext (xs,i)))) in
+     Ok (join rs)
+
+let rec insertion pd path pd2 =
+  let replace l xs l2 =
+    match xs with
+    | Emp -> (l2, Emp)
+    | Ext (ys, (_,y)) -> (l, Ext (ys, (l2,y))) in
+  match (pd, pd2, path) with
+  | (Br (l, brs), Br (l2,brs2), Ext (Emp, n)) ->
+     let (xs, ys) = split_suite n brs in
+     let* (_, xsd) = drop xs in
+     let (l', xsr) = replace l xsd l2 in
+     Ok (Br (l', append (append xsr brs2) ys))
+  | (Br (l, brs), Br (l2, Ext (Emp, (_, p2))), Ext(ns, n)) ->
+     let (xs, ys) = split_suite n brs in
+     let* ((t,br), xsd) = drop xs in
+     let (l', xsr) = replace l xsd l2 in
+     let* pdr = insertion br ns p2 in
+     Ok (Br (l', append (Ext (xsr, (t, pdr))) ys))
+  | (_,_,_) -> Error "Insertion failed"
+
+let rec get_all_paths pd =
+  match pd with
+  | Br (_, brs) ->
+     fold_left (map_suite (zip_with_idx brs) ~f:(fun (i,(_,p)) -> append (singleton (singleton i)) (map_suite (get_all_paths p) ~f:(fun xs -> Ext (xs, i))))) (singleton (singleton (length brs))) append
+
 (*****************************************************************************)
 (*                             Discs and Spheres                             *)
 (*****************************************************************************)
diff --git a/lib/suite.ml b/lib/suite.ml
index 3b9efc9..4d36520 100644
--- a/lib/suite.ml
+++ b/lib/suite.ml
@@ -53,6 +53,15 @@ let rec map_suite s ~f =
   | Emp -> Emp
   | Ext (s',x) -> map_suite s' ~f |> f x
 
+let rec map_suite_m s ~f =
+  let open Base.Result.Monad_infix in
+  match s with
+  | Emp -> Ok Emp
+  | Ext (s', x) ->
+     map_suite_m s' ~f >>= fun sm' ->
+     f x >>= fun xm ->
+     Ok (Ext (sm', xm))
+
 let map_with_lvl s ~f =
   let rec go s =
     match s with
@@ -150,6 +159,14 @@ let rec range i j =
   if (i > j) then Emp
   else Ext (range i (j-1), j)
 
+let rec range_r a b =
+  if a >= b then Emp else Ext (range_r (a+1) b, a)
+
+let rec find xs ~p =
+  match xs with
+  | Emp -> Error "Find did not find"
+  | Ext(ys, y) -> if p y then Ok y else find ys ~p
+
 let rec repeat n x =
   if (n = 0) then
     Emp
@@ -208,6 +225,20 @@ let nth n s =
   let l = length s in
   db_get (l-n-1) s
 
+let drop s =
+  match s with
+  | Emp -> Error "Nothing to drop"
+  | Ext (xs, x) -> Ok (x, xs)
+
+let split_suite n s =
+  let rec go n s =
+    match s with
+    | Emp -> (Emp,Emp,n)
+    | Ext(xs,x) ->
+       let (a, b, m) = go n xs in
+       if m = 0 then (a, Ext(b,x),m) else (Ext(a,x),b,m - 1) in
+  let (a, b, _) = go n s in (a, b)
+
 let rec grab k s =
   if (k<=0) then (s,[]) else
   let (s',r) = grab (k-1) s in
diff --git a/lib/value.ml b/lib/value.ml
index 85f26a2..5279248 100644
--- a/lib/value.ml
+++ b/lib/value.ml
@@ -112,3 +112,19 @@ and pp_spine ppf sp =
 
 let pp_top_env = hovbox (pp_suite (parens (pair ~sep:(any " : ") string pp_value)))
 let pp_loc_env = hovbox (pp_suite ~sep:comma pp_value)
+
+let rec sp_to_suite sp =
+  match sp with
+  | EmpSp -> Emp
+  | AppSp (s,v,i) -> Ext(sp_to_suite s, (v,i))
+  | BaseSp s -> sp_to_suite s
+  | LidSp s -> sp_to_suite s
+  | CoreSp s -> sp_to_suite s
+
+let sp_length sp =
+  length (sp_to_suite sp)
+
+let rec suite_to_sp s =
+  match s with
+  | Emp -> EmpSp
+  | Ext(s, (v,i)) -> AppSp (suite_to_sp s,v,i)

From 1fe6f09596ea42a4d5971fb423c211c8eef21c6c Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Tue, 6 Apr 2021 17:47:30 +0100
Subject: [PATCH 02/14] Fixed some bugs, at least working in 1 dimension

---
 examples/reduct-test.catt | 39 +++++++++++++++++++++++++++++++
 lib/eval.ml               | 48 +++++++++++++++++++++++++++------------
 lib/pd.ml                 |  6 ++---
 lib/suite.ml              |  2 +-
 lib/typecheck.ml          | 12 ++++++----
 lib/value.ml              |  2 +-
 6 files changed, 85 insertions(+), 24 deletions(-)
 create mode 100644 examples/reduct-test.catt

diff --git a/examples/reduct-test.catt b/examples/reduct-test.catt
new file mode 100644
index 0000000..b649e69
--- /dev/null
+++ b/examples/reduct-test.catt
@@ -0,0 +1,39 @@
+coh id {C : Cat} (x :: C)
+  : x => x
+
+coh comp {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+  : x => z
+
+coh comp2 {C2 : Cat}
+    {x2 :: C2}
+    {y2 :: C2} (f2 :: x2 => y2)
+    {z2 :: C2} (g2 :: y2 => z2)
+  : x2 => z2
+
+coh comp3 {C3 : Cat}
+    {x3 :: C3}
+    {y3 :: C3} (f3 :: x3 => y3)
+    {z3 :: C3} (g3 :: y3 => z3)
+  : x3 => z3
+
+let reduce-assoc {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+    {w :: C} (h :: z => w) : [ x => w ] = comp f (comp2 g h)
+
+let reduce-assoc-2 {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+    {w :: C} (h :: z => w) : [ x => w ] = comp (comp2 f g) h
+
+let reduce-assoc-3 {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+    {w :: C} (h :: z => w)
+    {v :: C} (i :: w => v) : [ x => v ] = comp (comp2 f g) (comp3 h i)
diff --git a/lib/eval.ml b/lib/eval.ml
index e11936e..2d4497d 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -86,9 +86,13 @@ and appV t u ict =
   | CohV (cn,pd,c,s,t,sp) ->
      let sp' = AppSp(sp,u,ict) in
      let x = CohV (cn,pd,c,s,t,sp') in
+     (* pr "Current: %a" pp_value x ;
+      * print_newline (); *)
      if sp_length sp' = pd_length pd + 1 then
        (match redCoh cn pd c s t sp' with
-       | Error _ -> x
+        | Error _ ->
+           (* pr "Attempted reduction: %s\n" y; *)
+           x
        | Ok y -> y) else x
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
 
@@ -110,16 +114,16 @@ and redCoh cn pd c s t sp =
     | Emp -> Error "No redex found"
     | Ext (xs, ((_,_,_,_,CohV (cn', pd', c', s', t', sp')), redex_path)) ->
        let args = sp_to_suite sp' in
-       let pda = map_pd_lvls pd' 0 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (false, n , nm , ict, v)) in
+       let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (false, n , nm , ict, v)) in
        if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
-    | _ -> get_redex xs in
+    | Ext (xs, _) -> get_redex xs in
 
   let get_internal_substitution pd =
     let l = Pd.labels pd in
     let fl = filter (zip_with_idx l) (fun (_,(b,_,_,_,_)) -> not b) in
-    map_suite_m (range_r 0 (length fl)) ~f:(fun n ->
+    map_suite_m (range 1 (length fl)) ~f:(fun n ->
         let* (x,(_,_,_,icit,_)) = find fl ~p:(fun (_,(_,i,_,_,_)) -> i = n) in
-        Ok ((RigidV (x,EmpSp),icit))) in
+        Ok ((RigidV (x + 1,EmpSp),icit))) in
 
   let path_from_term_type tm ty path =
     let pl = length path in
@@ -141,38 +145,52 @@ and redCoh cn pd c s t sp =
   let get_external_substitution pd redex_path all_paths internal_tm internal_ty =
     let l = Pd.labels pd in
     let fl = filter (zip_with_idx l) (fun (_,(b,_,_,_,_)) -> b) in
-    map_suite_m (range 0 (length all_paths)) ~f:(fun n ->
+    (* pr "filtered labels: %a\n" (pp_suite int) (map_suite fl ~f:fst); *)
+    map_suite_m (range 1 (length all_paths)) ~f:(fun n ->
         match find fl ~p:(fun (_,(_,i,_,_,_)) -> i = n) with
         | Error _ ->
-           let path = subtract_path (db_get n all_paths) redex_path in
+           (* pr "Number: %d\n" n; *)
+           (* pr "Pre substract: %a\n" (pp_suite int) (nth (n - 1) all_paths); *)
+           let path = subtract_path (nth (n - 1) all_paths) redex_path in
+           (* pr "Substracted path: %a\n" (pp_suite int) path; *)
            let* t = path_from_term_type internal_tm internal_ty path in
-           Ok (t)
-        | Ok (x,_) -> Ok (RigidV (x,EmpSp))) in
+           Ok t
+        | Ok (x,_) -> Ok (RigidV (x + 1,EmpSp))) in
 
   let ctx_length = pd_length pd + 1 in
-  let (cat_arg, args) = split_suite 1 (sp_to_suite sp) in
-  let pd_with_args = map_pd_lvls pd 0 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (true, n, nm, ict, v)) in
+  let args = sp_to_suite sp in
+  let pd_with_args = map_pd_lvls pd 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (true, n, nm, ict, v)) in
 
   match loc_max_bh pd_with_args with
   | Error _ -> Error "Pd is linear"
   | Ok xs ->
+     (* pr "Loc Max: %a\n" (pp_suite (fun ppf ((a,b,c,d,e),_) -> pf ppf "(%a,%d,%s,%a,%a)" bool a b c pp_ict d pp_value e)) xs; *)
      let* (cni,pdi,ci,si,ti,redex_pd,redex_path) = get_redex xs in
+     (* pr "Pd with args: %a\n" (pp_pd (fun ppf (_,_,_,_,v) -> pf ppf "%a" pp_value v)) pd_with_args; *)
+     (* pr "redex pd: %a\n" (pp_pd (fun ppf (b,n,_,_,v) -> pf ppf "(%a,%d,%a)" bool b n pp_value v)) redex_pd; *)
+     (* pr "Path: %a\n" (pp_suite int) redex_path; *)
      let internal_ctx_length = pd_length pdi + 1 in
      let internal_term = CohV(cni,pdi,ci,si,ti,EmpSp) in
+     (* pr "Internal term: %a\n" pp_value internal_term; *)
      let* pd_insert = insertion pd_with_args redex_path redex_pd in
+     (* pr "Inserted pd: %a\n" (pp_pd (fun ppf (b,n,_,_,v) -> pf ppf "(%a,%d,%a)" bool b n pp_value v)) pd_insert; *)
      let pd_final = map_pd pd_insert ~f:(fun (_,_,nm,icit,_) -> (nm,icit)) in
      let final_args = labels (map_pd pd_insert ~f:(fun (_,_,_,icit,v) -> (v,icit))) in
-     let final_spine = suite_to_sp (append cat_arg final_args) in
-     let inserted_ctx_length = pd_length pd_insert + 1 in
+     let final_spine = suite_to_sp (append (singleton (first args)) final_args) in
      let* internal_sub_no_append = get_internal_substitution pd_insert in
-     let internal_sub = append (singleton (RigidV (inserted_ctx_length, EmpSp), (snd cni))) internal_sub_no_append in
+     (* pr "Internal sub: %a\n" (pp_suite pp_value) (map_suite internal_sub_no_append ~f:fst); *)
+     let internal_sub = append (singleton (RigidV (0, EmpSp), (snd cni))) internal_sub_no_append in
      let internal_term_subbed = runSpV internal_term (suite_to_sp internal_sub) in
+     (* pr "Internal term subbed %a\n" pp_value internal_term_subbed; *)
      let internal_sub_no_icit = map_suite internal_sub ~f:fst in
      let civ = applySubstitution internal_ctx_length ci internal_sub_no_icit in
      let siv = applySubstitution internal_ctx_length si internal_sub_no_icit in
      let tiv = applySubstitution internal_ctx_length ti internal_sub_no_icit in
+     (* pr "Internal type subbed %a\n" pp_value (HomV(civ,siv,tiv)); *)
+     (* pr "All paths %a\n" (pp_suite ~sep:comma (pp_suite int)) (get_all_paths pd); *)
      let* external_sub_no_append = get_external_substitution pd_insert redex_path (get_all_paths pd) internal_term_subbed (HomV (civ,siv,tiv)) in
-     let external_sub = append (singleton (RigidV (inserted_ctx_length,EmpSp))) external_sub_no_append in
+     let external_sub = append (singleton (RigidV (0,EmpSp))) external_sub_no_append in
+     (* pr "External sub %a\n" (pp_suite pp_value) external_sub; *)
      let cv = applySubstitution ctx_length c external_sub in
      let sv = applySubstitution ctx_length s external_sub in
      let tv = applySubstitution ctx_length t external_sub in
diff --git a/lib/pd.ml b/lib/pd.ml
index eeec329..8f2c66a 100644
--- a/lib/pd.ml
+++ b/lib/pd.ml
@@ -126,12 +126,12 @@ let rec insertion pd path pd2 =
     | Ext (ys, (_,y)) -> (l, Ext (ys, (l2,y))) in
   match (pd, pd2, path) with
   | (Br (l, brs), Br (l2,brs2), Ext (Emp, n)) ->
-     let (xs, ys) = split_suite n brs in
+     let (xs, ys) = split_suite (n + 1) brs in
      let* (_, xsd) = drop xs in
      let (l', xsr) = replace l xsd l2 in
      Ok (Br (l', append (append xsr brs2) ys))
   | (Br (l, brs), Br (l2, Ext (Emp, (_, p2))), Ext(ns, n)) ->
-     let (xs, ys) = split_suite n brs in
+     let (xs, ys) = split_suite (n + 1) brs in
      let* ((t,br), xsd) = drop xs in
      let (l', xsr) = replace l xsd l2 in
      let* pdr = insertion br ns p2 in
@@ -141,7 +141,7 @@ let rec insertion pd path pd2 =
 let rec get_all_paths pd =
   match pd with
   | Br (_, brs) ->
-     fold_left (map_suite (zip_with_idx brs) ~f:(fun (i,(_,p)) -> append (singleton (singleton i)) (map_suite (get_all_paths p) ~f:(fun xs -> Ext (xs, i))))) (singleton (singleton (length brs))) append
+     fold_left (map_with_lvl brs ~f:(fun i (_,p) -> append (singleton (singleton (i + 1))) (map_suite (get_all_paths p) ~f:(fun xs -> Ext (xs, i))))) (singleton (singleton 0)) append
 
 (*****************************************************************************)
 (*                             Discs and Spheres                             *)
diff --git a/lib/suite.ml b/lib/suite.ml
index 4d36520..25b2f5a 100644
--- a/lib/suite.ml
+++ b/lib/suite.ml
@@ -160,7 +160,7 @@ let rec range i j =
   else Ext (range i (j-1), j)
 
 let rec range_r a b =
-  if a >= b then Emp else Ext (range_r (a+1) b, a)
+  if a > b then Emp else Ext (range_r (a+1) b, a)
 
 let rec find xs ~p =
   match xs with
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index c6762f8..eb9445e 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -585,10 +585,14 @@ let rec check_defs gma defs =
     let* tm_tm = check gma abs_tm ty_val in
     let tm_val = eval gma.top gma.loc tm_tm in
     pr "Checking complete for %s@," id;
-    (* let tm_nf = term_to_expr Emp (quote (gma.lvl) tm_val false) in
-     * let ty_nf = term_to_expr Emp (quote (gma.lvl) ty_val false) in *)
-    (* pr "Type: @[%a@]@," pp_expr ty_nf; *)
-    (* pr "Term: @[%a@]@," pp_expr tm_nf; *)
+    let tm_nf = term_to_expr Emp (quote false (gma.lvl) tm_val) in
+    let ty_nf = term_to_expr Emp (quote false (gma.lvl) ty_val) in
+    pr "Type: @[%a@]@," pp_expr ty_nf;
+    pr "Term: @[%a@]@," pp_expr tm_nf;
+    let tm_unfolded_nf = term_to_expr Emp (quote false (gma.lvl) (eval gma.top gma.loc (quote true (gma.lvl) tm_val))) in
+    let ty_unfolded_nf = term_to_expr Emp (quote false (gma.lvl) (eval gma.top gma.loc (quote true (gma.lvl) ty_val))) in
+    pr "Type unfolded: @[%a@]@," pp_expr ty_unfolded_nf;
+    pr "Term unfolded: @[%a@]@," pp_expr tm_unfolded_nf;
     check_defs (define gma id tm_val ty_val) ds
   | (CohDef (id,g,c,s,t))::ds ->
     pr "----------------@,";
diff --git a/lib/value.ml b/lib/value.ml
index 5279248..1ca43d5 100644
--- a/lib/value.ml
+++ b/lib/value.ml
@@ -91,7 +91,7 @@ let rec pp_value ppf v =
     pf ppf "@[coh [ %s @[%a@] :@;@[%a@]@;|> @[@[%a@] =>@;@[%a@]@] @[%a] ]@]" cn
       (pp_pd string) (map_pd pd ~f:fst)
       pp_value c pp_value s pp_value t pp_spine sp
-      
+
   | CylV (b,l,c) ->
     pf ppf "[| %a | %a | %a |]"
       pp_value b pp_value l pp_value c

From 38b40504c27b08c4aa97312f674fa0976cd18053 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Tue, 6 Apr 2021 18:01:33 +0100
Subject: [PATCH 03/14] Small fix and more test cases

---
 examples/reduct-test.catt | 13 +++++++++++++
 lib/eval.ml               |  2 +-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/examples/reduct-test.catt b/examples/reduct-test.catt
index b649e69..7ce5585 100644
--- a/examples/reduct-test.catt
+++ b/examples/reduct-test.catt
@@ -37,3 +37,16 @@ let reduce-assoc-3 {C : Cat}
     {z :: C} (g :: y => z)
     {w :: C} (h :: z => w)
     {v :: C} (i :: w => v) : [ x => v ] = comp (comp2 f g) (comp3 h i)
+
+coh horiz C (x(f(a)g)y(h(b)i)z) : comp f h => comp g i
+coh horiz2 C (x2(f2(a2)g2)y2(h2(b2)i2)z2) : comp2 f2 h2 => comp2 g2 i2
+
+let reduce-test {C : Cat}
+  {x :: C}
+  {y :: C} {f :: x => y}
+     	   {f2 :: x => y} (a :: f => f2)
+  {z :: C} {g :: y => z}
+     	   {g2 :: y => z} (b :: g => g2)
+  {w :: C} {h :: z => w}
+     	   {h2 :: z => w} (c :: h => h2) : [ comp f (comp2 g h) => comp f2 (comp2 g2 h2) ]
+   = horiz a (horiz2 b c)
diff --git a/lib/eval.ml b/lib/eval.ml
index 2d4497d..409634d 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -128,7 +128,7 @@ and redCoh cn pd c s t sp =
   let path_from_term_type tm ty path =
     let pl = length path in
     let ty_dim = dim_ty ty in
-    let b = (last path = 1) in
+    let b = (first path = 1) in
     let d = ty_dim - pl in
     let rec go d ty =
       match ty with

From 220b129d098d25db7f4dd4f4b5314d248380d565 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Wed, 7 Apr 2021 15:30:13 +0100
Subject: [PATCH 04/14] Disc removal

---
 examples/reduct-test.catt | 13 +++++++++++++
 lib/eval.ml               | 19 +++++++++++++++++--
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/examples/reduct-test.catt b/examples/reduct-test.catt
index 7ce5585..89f03c7 100644
--- a/examples/reduct-test.catt
+++ b/examples/reduct-test.catt
@@ -50,3 +50,16 @@ let reduce-test {C : Cat}
   {w :: C} {h :: z => w}
      	   {h2 :: z => w} (c :: h => h2) : [ comp f (comp2 g h) => comp f2 (comp2 g2 h2) ]
    = horiz a (horiz2 b c)
+
+let test {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y) : [ x => y ] = comp f (id y)
+
+coh unitor C (x(f)y) : comp f (id y) => f
+coh comp-v C (x(f(a)g(b)h)y) : f => h
+
+let test2 {C : Cat}
+  {x :: C}
+  {y :: C} { f :: x => y }
+     	   { g :: x => y } (a :: f => g) : [ f => g ]
+	   = comp-v a (unitor g)
diff --git a/lib/eval.ml b/lib/eval.ml
index 409634d..cc37036 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -76,6 +76,12 @@ and ($$) c v =
   match c with
   | Closure (top,loc,tm) -> eval top (Ext (loc,v)) tm
 
+(* This must be somewhere already *)
+and alt a b =
+  match a with
+  | Error _ -> b
+  | Ok x -> Ok x
+
 and appV t u ict =
   match t with
   | FlexV (m,sp) -> FlexV (m,AppSp(sp,u,ict))
@@ -89,14 +95,14 @@ and appV t u ict =
      (* pr "Current: %a" pp_value x ;
       * print_newline (); *)
      if sp_length sp' = pd_length pd + 1 then
-       (match redCoh cn pd c s t sp' with
+       (match alt (insertionCoh cn pd c s t sp') (disc_removal pd c s t u) with
         | Error _ ->
            (* pr "Attempted reduction: %s\n" y; *)
            x
        | Ok y -> y) else x
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
 
-and redCoh cn pd c s t sp =
+and insertionCoh cn pd c s t sp =
 
   let rec dim_ty ty =
     match ty with
@@ -200,6 +206,15 @@ and applySubstitution k v sub =
   let t = quote true k v in
   eval Emp sub t
 
+and disc_removal pd c s t u =
+  let rec construct_disc_type n =
+    if n = 0 then RigidV (0, EmpSp) else HomV(construct_disc_type (n-1), RigidV (2*n - 1, EmpSp), RigidV (2*n,EmpSp) ) in
+
+  if not (is_disc pd) then Error "Not disc"
+  else
+    if HomV(c,s,t) = construct_disc_type (dim_pd pd) then Ok u
+    else Error "Disc is not unbiased"
+
 and baseV v =
   match v with
   | FlexV (m,sp) -> FlexV (m,BaseSp sp)

From 84f6b375bbec0414330f492a6676f76d2812e11d Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Wed, 7 Apr 2021 15:49:34 +0100
Subject: [PATCH 05/14] Make normalisation not happen on cylinders

---
 lib/eval.ml  | 17 ++++++++---------
 lib/value.ml | 12 ++++--------
 2 files changed, 12 insertions(+), 17 deletions(-)

diff --git a/lib/eval.ml b/lib/eval.ml
index cc37036..c2289f3 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -92,17 +92,17 @@ and appV t u ict =
   | CohV (cn,pd,c,s,t,sp) ->
      let sp' = AppSp(sp,u,ict) in
      let x = CohV (cn,pd,c,s,t,sp') in
-     (* pr "Current: %a" pp_value x ;
-      * print_newline (); *)
-     if sp_length sp' = pd_length pd + 1 then
-       (match alt (insertionCoh cn pd c s t sp') (disc_removal pd c s t u) with
+     (match sp_to_suite sp' with
+     | Error _ -> x
+     | Ok (sp_list) -> if length sp_list = pd_length pd + 1 then
+       (match alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u) with
         | Error _ ->
            (* pr "Attempted reduction: %s\n" y; *)
            x
-       | Ok y -> y) else x
+       | Ok y -> y) else x)
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
 
-and insertionCoh cn pd c s t sp =
+and insertionCoh cn pd c s t args =
 
   let rec dim_ty ty =
     match ty with
@@ -119,8 +119,8 @@ and insertionCoh cn pd c s t sp =
     match xs with
     | Emp -> Error "No redex found"
     | Ext (xs, ((_,_,_,_,CohV (cn', pd', c', s', t', sp')), redex_path)) ->
-       let args = sp_to_suite sp' in
-       let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (false, n , nm , ict, v)) in
+       let* args_inner = sp_to_suite sp' in
+       let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
        if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
     | Ext (xs, _) -> get_redex xs in
 
@@ -164,7 +164,6 @@ and insertionCoh cn pd c s t sp =
         | Ok (x,_) -> Ok (RigidV (x + 1,EmpSp))) in
 
   let ctx_length = pd_length pd + 1 in
-  let args = sp_to_suite sp in
   let pd_with_args = map_pd_lvls pd 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args in (true, n, nm, ict, v)) in
 
   match loc_max_bh pd_with_args with
diff --git a/lib/value.ml b/lib/value.ml
index 1ca43d5..bab76dc 100644
--- a/lib/value.ml
+++ b/lib/value.ml
@@ -114,15 +114,11 @@ let pp_top_env = hovbox (pp_suite (parens (pair ~sep:(any " : ") string pp_value
 let pp_loc_env = hovbox (pp_suite ~sep:comma pp_value)
 
 let rec sp_to_suite sp =
+  let open Base.Result.Monad_infix in
   match sp with
-  | EmpSp -> Emp
-  | AppSp (s,v,i) -> Ext(sp_to_suite s, (v,i))
-  | BaseSp s -> sp_to_suite s
-  | LidSp s -> sp_to_suite s
-  | CoreSp s -> sp_to_suite s
-
-let sp_length sp =
-  length (sp_to_suite sp)
+  | EmpSp -> Ok (Emp)
+  | AppSp (s,v,i) -> sp_to_suite s >>= fun s' -> Ok (Ext(s', (v,i)))
+  | _ -> Error "Tried to normalise cylinder"
 
 let rec suite_to_sp s =
   match s with

From cb85f8e31712e58fda3828b867c3f01e5bd01904 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Wed, 7 Apr 2021 16:38:25 +0100
Subject: [PATCH 06/14] Endo coherence removal

---
 examples/reduct-test.catt | 17 ++++++++++----
 lib/eval.ml               | 48 ++++++++++++++++++++++++++++++++-------
 2 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/examples/reduct-test.catt b/examples/reduct-test.catt
index 89f03c7..af29266 100644
--- a/examples/reduct-test.catt
+++ b/examples/reduct-test.catt
@@ -58,8 +58,15 @@ let test {C : Cat}
 coh unitor C (x(f)y) : comp f (id y) => f
 coh comp-v C (x(f(a)g(b)h)y) : f => h
 
-let test2 {C : Cat}
-  {x :: C}
-  {y :: C} { f :: x => y }
-     	   { g :: x => y } (a :: f => g) : [ f => g ]
-	   = comp-v a (unitor g)
+# let test2 {C : Cat}
+#   {x :: C}
+#   {y :: C} { f :: x => y }
+#      	   { g :: x => y } (a :: f => g) : [ f => g ]
+# 	   = comp-v a (unitor g)
+
+coh fake-id C (x(f)y(g)z) : comp f g => comp f g
+
+let endo-coherence {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z) : [ comp f g => comp f g ] = fake-id f g
diff --git a/lib/eval.ml b/lib/eval.ml
index c2289f3..6d43a13 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -94,20 +94,22 @@ and appV t u ict =
      let x = CohV (cn,pd,c,s,t,sp') in
      (match sp_to_suite sp' with
      | Error _ -> x
-     | Ok (sp_list) -> if length sp_list = pd_length pd + 1 then
-       (match alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u) with
+     | Ok (sp_list) ->
+        let k = length sp_list in
+        if k = pd_length pd + 1 then
+       (match alt (alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u)) (endo_coherence_removal cn pd k c s t sp_list) with
         | Error _ ->
            (* pr "Attempted reduction: %s\n" y; *)
            x
        | Ok y -> y) else x)
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
 
-and insertionCoh cn pd c s t args =
-
-  let rec dim_ty ty =
+and dim_ty ty =
     match ty with
     | HomV (c,_,_) -> dim_ty c + 1
-    | _ -> 0 in
+    | _ -> 0
+
+and insertionCoh cn pd c s t args =
 
   let rec type_linearity v =
     match force_meta v with
@@ -205,15 +207,45 @@ and applySubstitution k v sub =
   let t = quote true k v in
   eval Emp sub t
 
+and construct_disc_type n =
+  if n = 0 then RigidV (0, EmpSp) else HomV(construct_disc_type (n-1), RigidV (2*n - 1, EmpSp), RigidV (2*n,EmpSp) )
+
 and disc_removal pd c s t u =
-  let rec construct_disc_type n =
-    if n = 0 then RigidV (0, EmpSp) else HomV(construct_disc_type (n-1), RigidV (2*n - 1, EmpSp), RigidV (2*n,EmpSp) ) in
+
 
   if not (is_disc pd) then Error "Not disc"
   else
     if HomV(c,s,t) = construct_disc_type (dim_pd pd) then Ok u
     else Error "Disc is not unbiased"
 
+and endo_coherence_removal cn pd k c s t sp_list =
+  (* Can't open syntax here: Must be a way to fix this *)
+  let fresh_pd pd =
+    let nm_lvl l = Fmt.str "x%d" l in
+    Pd.map_pd_lf_nd_lvl pd
+      ~lf:(fun lvl _ -> (nm_lvl lvl,Expl))
+      ~nd:(fun lvl _ -> (nm_lvl lvl,Impl)) in
+  let rec type_to_suite ty =
+    match ty with
+    | HomV(a,b,c) -> Ext(Ext(type_to_suite a, (b,Impl)), (c,Impl))
+    | _ -> Emp in
+  if not (s = t) then Error "Not an endo coherence"
+  else
+    let dim = dim_ty c in
+    let new_pd = fresh_pd (unit_disc_pd dim) in
+    let coh_ty = construct_disc_type dim in
+    let coh_ty_tm = RigidV(2*dim + 1,EmpSp) in
+    if is_disc pd && c = coh_ty && s = coh_ty_tm then Error "Already identity"
+    else
+    let args_not_subbed = Ext(type_to_suite c, (s, Expl)) in
+    let sp_list_no_icit = map_suite sp_list ~f:fst in
+    let args_subbed = map_suite args_not_subbed ~f:(fun (v,i) -> (applySubstitution k v (sp_list_no_icit), i)) in
+    let args_final = suite_to_sp (append (singleton (first sp_list)) args_subbed) in
+    Ok (runSpV (CohV (cn,new_pd,coh_ty,coh_ty_tm,coh_ty_tm,EmpSp)) args_final)
+
+
+
+
 and baseV v =
   match v with
   | FlexV (m,sp) -> FlexV (m,BaseSp sp)

From a5270ca916584bbddeeca016f6f0abed138d0247 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Thu, 8 Apr 2021 11:58:34 +0100
Subject: [PATCH 07/14] Normalise top level definitions

---
 lib/eval.ml      | 4 ++++
 lib/typecheck.ml | 4 ++--
 lib/unify.ml     | 7 +++++++
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/lib/eval.ml b/lib/eval.ml
index 6d43a13..14f5c3c 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -124,6 +124,10 @@ and insertionCoh cn pd c s t args =
        let* args_inner = sp_to_suite sp' in
        let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
        if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
+    | Ext (xs, ((_,_,_,_,TopV (_, _, CohV (cn', pd', c', s', t', sp'))), redex_path)) ->
+       let* args_inner = sp_to_suite sp' in
+       let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
+       if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
     | Ext (xs, _) -> get_redex xs in
 
   let get_internal_substitution pd =
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index eb9445e..f0e1eba 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -589,8 +589,8 @@ let rec check_defs gma defs =
     let ty_nf = term_to_expr Emp (quote false (gma.lvl) ty_val) in
     pr "Type: @[%a@]@," pp_expr ty_nf;
     pr "Term: @[%a@]@," pp_expr tm_nf;
-    let tm_unfolded_nf = term_to_expr Emp (quote false (gma.lvl) (eval gma.top gma.loc (quote true (gma.lvl) tm_val))) in
-    let ty_unfolded_nf = term_to_expr Emp (quote false (gma.lvl) (eval gma.top gma.loc (quote true (gma.lvl) ty_val))) in
+    let tm_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) tm_val) in
+    let ty_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) ty_val) in
     pr "Type unfolded: @[%a@]@," pp_expr ty_unfolded_nf;
     pr "Term unfolded: @[%a@]@," pp_expr tm_unfolded_nf;
     check_defs (define gma id tm_val ty_val) ds
diff --git a/lib/unify.ml b/lib/unify.ml
index cd2e2ff..9427724 100644
--- a/lib/unify.ml
+++ b/lib/unify.ml
@@ -128,6 +128,12 @@ type strategy =
   | UnfoldNone
   | OneShot
 
+let pp_strat ppf stgy =
+  match stgy with
+  | UnfoldAll -> pf ppf "unfold all"
+  | UnfoldNone -> pf ppf "unfold none"
+  | OneShot -> pf ppf "one shot"
+
 let isUnfoldAll s =
   match s with
   | UnfoldAll -> true
@@ -144,6 +150,7 @@ let isOneShot s =
   | _ -> false
 
 let rec unify stgy top l t u =
+  (* pr "Unifying (strategy %a) %a with %a@," pp_strat stgy pp_value t pp_value u; *)
   match (force_meta t , force_meta u) with
   | (TypV , TypV) -> ()
   | (CatV , CatV) -> ()

From 00ea902b1f9ba8908c9b70145f1774f07a0255e4 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Thu, 8 Apr 2021 12:54:09 +0100
Subject: [PATCH 08/14] Potential fix to unification problem

---
 examples/reduct-test.catt |  7 +++++++
 lib/unify.ml              |  8 +++++++-
 lib/value.ml              | 10 +++++++++-
 3 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/examples/reduct-test.catt b/examples/reduct-test.catt
index af29266..b036cc5 100644
--- a/examples/reduct-test.catt
+++ b/examples/reduct-test.catt
@@ -41,6 +41,13 @@ let reduce-assoc-3 {C : Cat}
 coh horiz C (x(f(a)g)y(h(b)i)z) : comp f h => comp g i
 coh horiz2 C (x2(f2(a2)g2)y2(h2(b2)i2)z2) : comp2 f2 h2 => comp2 g2 i2
 
+let this-should-reduce {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+    {w :: C} (h :: z => w)
+    : [ x => w ] = comp f ((coh [ C2 (x2(f2)y2(g2)z2) : C2 |> x2 => z2]) g h)
+
 let reduce-test {C : Cat}
   {x :: C}
   {y :: C} {f :: x => y}
diff --git a/lib/unify.ml b/lib/unify.ml
index 9427724..8a3dd4f 100644
--- a/lib/unify.ml
+++ b/lib/unify.ml
@@ -149,9 +149,15 @@ let isOneShot s =
   | OneShot -> true
   | _ -> false
 
+let resolve_coh tm =
+  match tm with
+  | CohV (cn,pd,c,s,t,sp) -> runSpV (CohV(cn,pd,c,s,t,EmpSp)) (map_sp sp ~f:force_meta)
+  | TopV (nm,sp,CohV(cn,pd,c,s,t,sp')) -> TopV(nm,sp,runSpV (CohV(cn,pd,c,s,t,EmpSp)) (map_sp sp' ~f:force_meta))
+  | _ -> tm
+
 let rec unify stgy top l t u =
   (* pr "Unifying (strategy %a) %a with %a@," pp_strat stgy pp_value t pp_value u; *)
-  match (force_meta t , force_meta u) with
+  match (resolve_coh (force_meta t) , resolve_coh (force_meta u)) with
   | (TypV , TypV) -> ()
   | (CatV , CatV) -> ()
 
diff --git a/lib/value.ml b/lib/value.ml
index bab76dc..6e0767c 100644
--- a/lib/value.ml
+++ b/lib/value.ml
@@ -100,7 +100,7 @@ and pp_spine ppf sp =
   match sp with
   | EmpSp -> ()
   | AppSp (sp',v,Expl) ->
-    pf ppf "%a %a" pp_spine sp' pp_value v
+    pf ppf "%a %a" pp_spine sp' (parens pp_value) v
   | AppSp (sp',v,Impl) ->
     pf ppf "%a {%a}" pp_spine sp' pp_value v
   | BaseSp sp' ->
@@ -124,3 +124,11 @@ let rec suite_to_sp s =
   match s with
   | Emp -> EmpSp
   | Ext(s, (v,i)) -> AppSp (suite_to_sp s,v,i)
+
+let rec map_sp sp ~f =
+  match sp with
+  | EmpSp -> EmpSp
+  | AppSp (s,v,i) -> AppSp (map_sp s ~f, f v, i)
+  | BaseSp s -> BaseSp (map_sp s ~f)
+  | LidSp s -> LidSp (map_sp s ~f)
+  | CoreSp s -> CoreSp (map_sp s ~f)

From 749bb09b3efba6c29501ccf319ddec8aff2309f5 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Fri, 9 Apr 2021 10:31:17 +0100
Subject: [PATCH 09/14] Minor change to meta forcing

---
 lib/eval.ml  | 20 +++++++++++---------
 lib/unify.ml |  4 ++--
 2 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/lib/eval.ml b/lib/eval.ml
index 14f5c3c..1420cfd 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -120,15 +120,17 @@ and insertionCoh cn pd c s t args =
   let rec get_redex xs =
     match xs with
     | Emp -> Error "No redex found"
-    | Ext (xs, ((_,_,_,_,CohV (cn', pd', c', s', t', sp')), redex_path)) ->
-       let* args_inner = sp_to_suite sp' in
-       let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
-       if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
-    | Ext (xs, ((_,_,_,_,TopV (_, _, CohV (cn', pd', c', s', t', sp'))), redex_path)) ->
-       let* args_inner = sp_to_suite sp' in
-       let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
-       if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
-    | Ext (xs, _) -> get_redex xs in
+    | Ext (xs, ((_,_,_,_,t), redex_path)) ->
+       match (force_meta t) with
+       | CohV (cn', pd', c', s', t', sp') ->
+          let* args_inner = sp_to_suite sp' in
+          let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
+          if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
+       | TopV (_,_, CohV (cn', pd', c', s', t', sp')) ->
+          let* args_inner = sp_to_suite sp' in
+          let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
+          if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
+       | _ -> get_redex xs in
 
   let get_internal_substitution pd =
     let l = Pd.labels pd in
diff --git a/lib/unify.ml b/lib/unify.ml
index 8a3dd4f..d66d05c 100644
--- a/lib/unify.ml
+++ b/lib/unify.ml
@@ -151,8 +151,8 @@ let isOneShot s =
 
 let resolve_coh tm =
   match tm with
-  | CohV (cn,pd,c,s,t,sp) -> runSpV (CohV(cn,pd,c,s,t,EmpSp)) (map_sp sp ~f:force_meta)
-  | TopV (nm,sp,CohV(cn,pd,c,s,t,sp')) -> TopV(nm,sp,runSpV (CohV(cn,pd,c,s,t,EmpSp)) (map_sp sp' ~f:force_meta))
+  | CohV (cn,pd,c,s,t,sp) -> runSpV (CohV(cn,pd,c,s,t,EmpSp)) sp
+  | TopV (nm,sp,CohV(cn,pd,c,s,t,sp')) -> TopV(nm,sp,runSpV (CohV(cn,pd,c,s,t,EmpSp)) sp')
   | _ -> tm
 
 let rec unify stgy top l t u =

From 4bf69e7cce7b8ef9c69c6def9c3e01c17ddecb23 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Mon, 12 Apr 2021 13:33:05 +0100
Subject: [PATCH 10/14] Fix major bug in higher dimensional insertion

---
 examples/reduct-test.catt | 25 +++++++++++++++--------
 lib/eval.ml               | 43 +++++++++++++++------------------------
 lib/pd.ml                 |  6 +++---
 3 files changed, 35 insertions(+), 39 deletions(-)

diff --git a/examples/reduct-test.catt b/examples/reduct-test.catt
index b036cc5..42cc9da 100644
--- a/examples/reduct-test.catt
+++ b/examples/reduct-test.catt
@@ -65,15 +65,22 @@ let test {C : Cat}
 coh unitor C (x(f)y) : comp f (id y) => f
 coh comp-v C (x(f(a)g(b)h)y) : f => h
 
-# let test2 {C : Cat}
-#   {x :: C}
-#   {y :: C} { f :: x => y }
-#      	   { g :: x => y } (a :: f => g) : [ f => g ]
-# 	   = comp-v a (unitor g)
+let test2 {C : Cat}
+  {x :: C}
+  {y :: C} { f :: x => y }
+     	   { g :: x => y } (a :: f => g) : [ f => g ]
+	   = comp-v a (unitor g)
+
+# coh fake-id C (x(f)y(g)z) : comp f g => comp f g
 
-coh fake-id C (x(f)y(g)z) : comp f g => comp f g
+# let endo-coherence {C : Cat}
+#     {x :: C}
+#     {y :: C} (f :: x => y)
+#     {z :: C} (g :: y => z) : [ comp f g => comp f g ] = fake-id f g
 
-let endo-coherence {C : Cat}
+coh idv C (x(f)y) : f => f
+
+let test2d {C : Cat}
     {x :: C}
-    {y :: C} (f :: x => y)
-    {z :: C} (g :: y => z) : [ comp f g => comp f g ] = fake-id f g
+    {y :: C} {f :: x => y}
+       	     {g :: x => y} (a :: f => g) : [ f => g ] = comp-v a (idv g)
diff --git a/lib/eval.ml b/lib/eval.ml
index 1420cfd..8a4b599 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -79,7 +79,9 @@ and ($$) c v =
 (* This must be somewhere already *)
 and alt a b =
   match a with
-  | Error _ -> b
+  | Error x -> (match b with
+                | Ok y -> Ok y
+                | Error y -> Error (Printf.sprintf "%s | %s" x y))
   | Ok x -> Ok x
 
 and appV t u ict =
@@ -99,7 +101,7 @@ and appV t u ict =
         if k = pd_length pd + 1 then
        (match alt (alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u)) (endo_coherence_removal cn pd k c s t sp_list) with
         | Error _ ->
-           (* pr "Attempted reduction: %s\n" y; *)
+           (* pr "Attempted reduction on %a: %s\n" pp_value x y; *)
            x
        | Ok y -> y) else x)
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
@@ -111,25 +113,27 @@ and dim_ty ty =
 
 and insertionCoh cn pd c s t args =
 
-  let rec type_linearity v =
+  let unfold v =
     match force_meta v with
-    | HomV(c, RigidV _, RigidV _) -> dim_ty c
-    | HomV(c, _, _) -> type_linearity c
-    | _ -> -1 in
+    | TopV (_,_,x) -> x
+    | y -> y in
+
+  let rec type_linearity c s t =
+    match (unfold s, unfold t) with
+    | (RigidV _, RigidV _) -> dim_ty c
+    | _ -> match c with
+           | HomV(c',s',t') -> type_linearity c' s' t'
+           | _ -> -1 in
 
   let rec get_redex xs =
     match xs with
     | Emp -> Error "No redex found"
     | Ext (xs, ((_,_,_,_,t), redex_path)) ->
-       match (force_meta t) with
+       match (unfold t) with
        | CohV (cn', pd', c', s', t', sp') ->
           let* args_inner = sp_to_suite sp' in
           let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
-          if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
-       | TopV (_,_, CohV (cn', pd', c', s', t', sp')) ->
-          let* args_inner = sp_to_suite sp' in
-          let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
-          if type_linearity (HomV (c', s', t')) >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
+          if type_linearity c' s' t' >= length redex_path - 1 then Ok (cn', pd' ,c',s',t',pda ,redex_path) else get_redex xs
        | _ -> get_redex xs in
 
   let get_internal_substitution pd =
@@ -159,14 +163,10 @@ and insertionCoh cn pd c s t args =
   let get_external_substitution pd redex_path all_paths internal_tm internal_ty =
     let l = Pd.labels pd in
     let fl = filter (zip_with_idx l) (fun (_,(b,_,_,_,_)) -> b) in
-    (* pr "filtered labels: %a\n" (pp_suite int) (map_suite fl ~f:fst); *)
     map_suite_m (range 1 (length all_paths)) ~f:(fun n ->
         match find fl ~p:(fun (_,(_,i,_,_,_)) -> i = n) with
         | Error _ ->
-           (* pr "Number: %d\n" n; *)
-           (* pr "Pre substract: %a\n" (pp_suite int) (nth (n - 1) all_paths); *)
            let path = subtract_path (nth (n - 1) all_paths) redex_path in
-           (* pr "Substracted path: %a\n" (pp_suite int) path; *)
            let* t = path_from_term_type internal_tm internal_ty path in
            Ok t
         | Ok (x,_) -> Ok (RigidV (x + 1,EmpSp))) in
@@ -177,33 +177,22 @@ and insertionCoh cn pd c s t args =
   match loc_max_bh pd_with_args with
   | Error _ -> Error "Pd is linear"
   | Ok xs ->
-     (* pr "Loc Max: %a\n" (pp_suite (fun ppf ((a,b,c,d,e),_) -> pf ppf "(%a,%d,%s,%a,%a)" bool a b c pp_ict d pp_value e)) xs; *)
      let* (cni,pdi,ci,si,ti,redex_pd,redex_path) = get_redex xs in
-     (* pr "Pd with args: %a\n" (pp_pd (fun ppf (_,_,_,_,v) -> pf ppf "%a" pp_value v)) pd_with_args; *)
-     (* pr "redex pd: %a\n" (pp_pd (fun ppf (b,n,_,_,v) -> pf ppf "(%a,%d,%a)" bool b n pp_value v)) redex_pd; *)
-     (* pr "Path: %a\n" (pp_suite int) redex_path; *)
      let internal_ctx_length = pd_length pdi + 1 in
      let internal_term = CohV(cni,pdi,ci,si,ti,EmpSp) in
-     (* pr "Internal term: %a\n" pp_value internal_term; *)
      let* pd_insert = insertion pd_with_args redex_path redex_pd in
-     (* pr "Inserted pd: %a\n" (pp_pd (fun ppf (b,n,_,_,v) -> pf ppf "(%a,%d,%a)" bool b n pp_value v)) pd_insert; *)
      let pd_final = map_pd pd_insert ~f:(fun (_,_,nm,icit,_) -> (nm,icit)) in
      let final_args = labels (map_pd pd_insert ~f:(fun (_,_,_,icit,v) -> (v,icit))) in
      let final_spine = suite_to_sp (append (singleton (first args)) final_args) in
      let* internal_sub_no_append = get_internal_substitution pd_insert in
-     (* pr "Internal sub: %a\n" (pp_suite pp_value) (map_suite internal_sub_no_append ~f:fst); *)
      let internal_sub = append (singleton (RigidV (0, EmpSp), (snd cni))) internal_sub_no_append in
      let internal_term_subbed = runSpV internal_term (suite_to_sp internal_sub) in
-     (* pr "Internal term subbed %a\n" pp_value internal_term_subbed; *)
      let internal_sub_no_icit = map_suite internal_sub ~f:fst in
      let civ = applySubstitution internal_ctx_length ci internal_sub_no_icit in
      let siv = applySubstitution internal_ctx_length si internal_sub_no_icit in
      let tiv = applySubstitution internal_ctx_length ti internal_sub_no_icit in
-     (* pr "Internal type subbed %a\n" pp_value (HomV(civ,siv,tiv)); *)
-     (* pr "All paths %a\n" (pp_suite ~sep:comma (pp_suite int)) (get_all_paths pd); *)
      let* external_sub_no_append = get_external_substitution pd_insert redex_path (get_all_paths pd) internal_term_subbed (HomV (civ,siv,tiv)) in
      let external_sub = append (singleton (RigidV (0,EmpSp))) external_sub_no_append in
-     (* pr "External sub %a\n" (pp_suite pp_value) external_sub; *)
      let cv = applySubstitution ctx_length c external_sub in
      let sv = applySubstitution ctx_length s external_sub in
      let tv = applySubstitution ctx_length t external_sub in
diff --git a/lib/pd.ml b/lib/pd.ml
index 8f2c66a..ce39dab 100644
--- a/lib/pd.ml
+++ b/lib/pd.ml
@@ -130,12 +130,12 @@ let rec insertion pd path pd2 =
      let* (_, xsd) = drop xs in
      let (l', xsr) = replace l xsd l2 in
      Ok (Br (l', append (append xsr brs2) ys))
-  | (Br (l, brs), Br (l2, Ext (Emp, (_, p2))), Ext(ns, n)) ->
+  | (Br (l, brs), Br (l2, Ext (Emp, (l3, p2))), Ext(ns, n)) ->
      let (xs, ys) = split_suite (n + 1) brs in
-     let* ((t,br), xsd) = drop xs in
+     let* ((_,br), xsd) = drop xs in
      let (l', xsr) = replace l xsd l2 in
      let* pdr = insertion br ns p2 in
-     Ok (Br (l', append (Ext (xsr, (t, pdr))) ys))
+     Ok (Br (l', append (Ext (xsr, (l3, pdr))) ys))
   | (_,_,_) -> Error "Insertion failed"
 
 let rec get_all_paths pd =

From 8543dcc441ada71118090825999a1b826d52735c Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Mon, 26 Apr 2021 09:08:13 +0100
Subject: [PATCH 11/14] Get EH and syllepsis working

---
 examples/eh-catt.catt      | 353 ++++++++++++++
 examples/eh.catt           |  24 +
 examples/ehtree.txt        |   1 +
 examples/endo.catt         |  10 +
 examples/syllepsis.catt    | 360 ++++++++++++++
 examples/syllepsisterm.txt | 948 +++++++++++++++++++++++++++++++++++++
 examples/syllepsistree.txt |   1 +
 lib/eval.ml                |  87 +++-
 lib/typecheck.ml           |   7 +-
 9 files changed, 1774 insertions(+), 17 deletions(-)
 create mode 100644 examples/eh-catt.catt
 create mode 100644 examples/eh.catt
 create mode 100644 examples/ehtree.txt
 create mode 100644 examples/endo.catt
 create mode 100644 examples/syllepsis.catt
 create mode 100644 examples/syllepsisterm.txt
 create mode 100644 examples/syllepsistree.txt

diff --git a/examples/eh-catt.catt b/examples/eh-catt.catt
new file mode 100644
index 0000000..b0d4b7f
--- /dev/null
+++ b/examples/eh-catt.catt
@@ -0,0 +1,353 @@
+#
+#  eh.catt - Eckmann-Hilton
+#
+
+coh id C (x) : x => x
+
+coh id2
+    (x : *)
+    (y : *) (f : x -> y)
+  : f -> f
+
+coh comp
+    (x : *)
+    (y : *) (f : x -> y)
+    (z : *) (g : y -> z)
+  : x -> z
+
+coh unit_r
+    (x : *)
+    (y : *) (f : x -> y)
+  : comp(f,id(y)) -> f
+
+coh unit_r_inv
+    (x : *)
+    (y : *) (f : x -> y)
+  : f -> comp(f,id(y))
+
+coh unit_l
+    (x : *)
+    (y : *) (f : x -> y)
+  : comp(id(x),f) -> f
+
+coh unit_l_inv
+    (x : *)
+    (y : *) (f : x -> y)
+  : f -> comp(id(x),f)
+
+coh vert
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+  : f -> h
+
+coh vert3
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+  : f -> i
+
+coh vert4
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+  : f -> j
+
+coh vert5
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+            (k : x -> y) (e : j -> k)
+  : f -> k
+
+coh whisk_r
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+    (z : *) (h : y -> z)
+  : comp(f,h) -> comp(g,h)
+
+coh whisk_r_unit_r
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+  : a -> vert3(unit_r_inv(f),whisk_r(a,id(y)),unit_r(g))
+
+coh whisk_r_unit_r_inv
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+  : vert3(unit_r_inv(f),whisk_r(a,id(y)),unit_r(g)) -> a
+
+coh whisk_l
+    (x : *)
+    (y : *) (f : x -> y)
+    (z : *) (g : y -> z)
+            (h : y -> z) (a : g -> h)
+  : comp(f,g) -> comp(f,h)
+
+coh whisk_l_unit_l
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+  : a -> vert3(unit_l_inv(f),whisk_l(id(x),a),unit_l(g))
+
+coh whisk_l_unit_l_inv
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+  : vert3(unit_l_inv(f),whisk_l(id(x),a),unit_l(g)) -> a
+
+coh swap
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+    (z : *) (h : y -> z)
+            (k : y -> z) (b : h -> k)
+  : vert(whisk_r(a,h),whisk_l(g,b)) ->
+    vert(whisk_l(f,b),whisk_r(a,k))
+
+coh unit_lr_cancel
+    (x : *)
+  : vert(unit_r(id(x)),unit_l_inv(id(x))) -> id2(comp(id(x),id(x)))
+
+coh unit_lr_insert
+    (x : *)
+  : id2(comp(id(x),id(x))) -> vert(unit_l(id(x)),unit_r_inv(id(x)))
+
+coh vert_cong
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+                         (c : f -> g) (A : a -> c)
+            (h : x -> y) (b : g -> h)
+                         (d : g -> h) (B : b -> d)
+  : vert(a,b) -> vert(c,d)
+
+coh vert_redistrib
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+            (k : x -> y) (e : j -> k)
+            (l : x -> y) (m : k -> l)
+  : vert(vert3(a,b,c),vert3(d,e,m)) ->
+    vert5(a,b,vert(c,d),e,m)
+
+coh vert_redistrib_inv
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+            (k : x -> y) (e : j -> k)
+            (l : x -> y) (m : k -> l)
+  : vert5(a,b,vert(c,d),e,m) ->
+    vert(vert3(a,b,c),vert3(d,e,m))
+
+coh vert5_cong_mid
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c0 : h -> i)
+                         (c1 : h -> i) (A : c0 -> c1)
+            (j : x -> y) (d : i -> j)
+            (k : x -> y) (e : j -> k)
+  : vert5(a,b,c0,d,e) -> vert5(a,b,c1,d,e)
+
+coh vert5_unit_mid
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+  : vert5(a,b,id2(h),c,d) -> vert4(a,b,c,d)
+
+coh vert5_unit_mid_inv
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+  : vert4(a,b,c,d) -> vert5(a,b,id2(h),c,d)
+
+coh vert_redistrib2
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+  : vert4(a,b,c,d) -> vert3(a,vert(b,c),d)
+
+coh vert_redistrib2_inv
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+            (h : x -> y) (b : g -> h)
+            (i : x -> y) (c : h -> i)
+            (j : x -> y) (d : i -> j)
+  : vert3(a,vert(b,c),d) -> vert4(a,b,c,d)
+
+coh vert3_cong3
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a0 : f -> g)
+                         (a1 : f -> g) (A : a0 -> a1)
+            (h : x -> y) (b0 : g -> h)
+                         (b1 : g -> h) (B : b0 -> b1)
+            (i : x -> y) (c0 : h -> i)
+                         (c1 : h -> i) (C : c0 -> c1)
+  : vert3(a0,b0,c0) -> vert3(a1,b1,c1)
+
+coh unit_l_is_unit_r
+    (x : *)
+  : unit_l(id(x)) -> unit_r(id(x))
+
+coh unit_r_inv_is_univ_l_inv
+    (x : *)
+  : unit_r_inv(id(x)) -> unit_l_inv(id(x))
+
+coh 3vert
+    (x : *)
+    (y : *) (f : x -> y)
+            (g : x -> y) (a : f -> g)
+                         (b : f -> g) (A : a -> b)
+                         (c : f -> g) (B : b -> c)
+  : a -> c
+
+section (x : *) (a : id(x) -> id(x)) (b : id(x) -> id(x)) where
+
+  let step1 : vert(a,b) ->
+              vert(vert3(unit_r_inv(id(x)),whisk_r(a,id(x)),unit_r(id(x))),vert3(unit_l_inv(id(x)),whisk_l(id(x),b),unit_l(id(x))))
+            = vert_cong(whisk_r_unit_r(a),whisk_l_unit_l(b))
+
+  let step2 : vert(vert3(unit_r_inv(id(x)),whisk_r(a,id(x)),unit_r(id(x))),vert3(unit_l_inv(id(x)),whisk_l(id(x),b),unit_l(id(x)))) ->
+              vert5(unit_r_inv(id(x)),whisk_r(a,id(x)),vert(unit_r(id(x)),unit_l_inv(id(x))),whisk_l(id(x),b),unit_l(id(x)))
+            = vert_redistrib(
+                unit_r_inv(id(x)),
+                whisk_r(a,id(x)),
+                unit_r(id(x)),
+                unit_l_inv(id(x)),
+                whisk_l(id(x),b),
+                unit_l(id(x))
+              )
+
+  let step3 : vert5(unit_r_inv(id(x)),whisk_r(a,id(x)),vert(unit_r(id(x)),unit_l_inv(id(x))),whisk_l(id(x),b),unit_l(id(x))) ->
+              vert5(unit_r_inv(id(x)),whisk_r(a,id(x)),id2(comp(id(x),id(x))),whisk_l(id(x),b),unit_l(id(x)))
+            = vert5_cong_mid(
+                unit_r_inv(id(x)),
+                whisk_r(a,id(x)),
+                unit_lr_cancel(x),
+                whisk_l(id(x),b),
+                unit_l(id(x))
+              )
+
+  let step4 : vert5(unit_r_inv(id(x)),whisk_r(a,id(x)),id2(comp(id(x),id(x))),whisk_l(id(x),b),unit_l(id(x))) ->
+              vert4(unit_r_inv(id(x)),whisk_r(a,id(x)),whisk_l(id(x),b),unit_l(id(x)))
+            = vert5_unit_mid(
+                unit_r_inv(id(x)),
+                whisk_r(a,id(x)),
+                whisk_l(id(x),b),
+                unit_l(id(x))
+              )
+
+  let step5 : vert4(unit_r_inv(id(x)),whisk_r(a,id(x)),whisk_l(id(x),b),unit_l(id(x))) ->
+              vert3(unit_r_inv(id(x)),vert(whisk_r(a,id(x)),whisk_l(id(x),b)),unit_l(id(x)))
+            = vert_redistrib2(
+                unit_r_inv(id(x)),
+                whisk_r(a,id(x)),
+                whisk_l(id(x),b),
+                unit_l(id(x))
+              )
+
+  let step6 : vert3(unit_r_inv(id(x)),vert(whisk_r(a,id(x)),whisk_l(id(x),b)),unit_l(id(x))) ->
+              vert3(unit_l_inv(id(x)),vert(whisk_l(id(x),b),whisk_r(a,id(x))),unit_r(id(x)))
+            = vert3_cong3(
+                unit_r_inv_is_univ_l_inv(x),
+                swap(a,b),
+                unit_l_is_unit_r(x)
+              )
+
+  let step7 : vert3(unit_l_inv(id(x)),vert(whisk_l(id(x),b),whisk_r(a,id(x))),unit_r(id(x))) ->
+              vert4(unit_l_inv(id(x)),whisk_l(id(x),b),whisk_r(a,id(x)),unit_r(id(x)))
+            = vert_redistrib2_inv(
+                unit_l_inv(id(x)),
+                whisk_l(id(x),b),
+                whisk_r(a,id(x)),
+                unit_r(id(x))
+              )
+
+  let step8 : vert4(unit_l_inv(id(x)),whisk_l(id(x),b),whisk_r(a,id(x)),unit_r(id(x))) ->
+              vert5(unit_l_inv(id(x)),whisk_l(id(x),b),id2(comp(id(x),id(x))),whisk_r(a,id(x)),unit_r(id(x)))
+            = vert5_unit_mid_inv(
+                unit_l_inv(id(x)),
+                whisk_l(id(x),b),
+                whisk_r(a,id(x)),
+                unit_r(id(x))
+              )
+
+  let step9 : vert5(unit_l_inv(id(x)),whisk_l(id(x),b),id2(comp(id(x),id(x))),whisk_r(a,id(x)),unit_r(id(x))) ->
+              vert5(unit_l_inv(id(x)),whisk_l(id(x),b),vert(unit_l(id(x)),unit_r_inv(id(x))),whisk_r(a,id(x)),unit_r(id(x)))
+            = vert5_cong_mid(
+                unit_l_inv(id(x)),
+                whisk_l(id(x),b),
+                unit_lr_insert(x),
+                whisk_r(a,id(x)),
+                unit_r(id(x))
+              )
+
+  let step10 : vert5(unit_l_inv(id(x)),whisk_l(id(x),b),vert(unit_l(id(x)),unit_r_inv(id(x))),whisk_r(a,id(x)),unit_r(id(x))) ->
+               vert(vert3(unit_l_inv(id(x)),whisk_l(id(x),b),unit_l(id(x))),vert3(unit_r_inv(id(x)),whisk_r(a,id(x)),unit_r(id(x))))
+            = vert_redistrib_inv(
+                unit_l_inv(id(x)),
+                whisk_l(id(x),b),
+                unit_l(id(x)),
+                unit_r_inv(id(x)),
+                whisk_r(a,id(x)),
+                unit_r(id(x))
+              )
+
+  let step11 : vert(vert3(unit_l_inv(id(x)),whisk_l(id(x),b),unit_l(id(x))),vert3(unit_r_inv(id(x)),whisk_r(a,id(x)),unit_r(id(x)))) ->
+               vert(b,a)
+             = vert_cong(whisk_l_unit_l_inv(b),whisk_r_unit_r_inv(a))
+
+  let eh : vert(a,b) -> vert(b,a)
+         = 3vert(step1(),
+           3vert(step2(),
+           3vert(step3(),
+           3vert(step4(),
+           3vert(step5(),
+           3vert(step6(),
+           3vert(step7(),
+           3vert(step8(),
+           3vert(step9(),
+           3vert(step10(),step11()))))))))))
+
+end
+
+#
+#  These terms indeed have the same normal form in CattSu
+#
+
+eqnf (x : *) (a : id(x) -> id(x)) (b : id(x) -> id(x))
+  | eh(x,a,b)
+  | swap(a,b)
+
+normalize (x : *) (a : id(x) -> id(x)) (b : id(x) -> id(x))
+  | eh(x,a,b)
diff --git a/examples/eh.catt b/examples/eh.catt
new file mode 100644
index 0000000..461f0df
--- /dev/null
+++ b/examples/eh.catt
@@ -0,0 +1,24 @@
+#
+#  eh.catt - Eckmann-Hilton
+#
+
+coh id C (x) : x => x
+
+coh comp C (x(f)y(g)z) : x => z
+
+coh vert C (x(f(a)g(b)h)y) : f => h
+
+coh whisk_r C (x(f(a)g)y(h)z) : comp f h => comp g h
+
+coh whisk_l C (x(f)y(g(a)h)z) : comp f g => comp f h
+
+coh swap3 C (x(f(a)g)y(h(b)k)z)
+  : vert (whisk_r a h) (whisk_l g b) =>
+    vert (whisk_l f b) (whisk_r a k)
+
+let eh {C : Cat}
+  {x :: C}
+  (a :: id x => id x)
+  (b :: id x => id x)
+  : [ vert a b => vert b a ]
+  = swap3 a b
diff --git a/examples/ehtree.txt b/examples/ehtree.txt
new file mode 100644
index 0000000..9bcbd9b
--- /dev/null
+++ b/examples/ehtree.txt
@@ -0,0 +1 @@
+[[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]
diff --git a/examples/endo.catt b/examples/endo.catt
new file mode 100644
index 0000000..28cc299
--- /dev/null
+++ b/examples/endo.catt
@@ -0,0 +1,10 @@
+coh comp C (x(f)y(g)z) : x => z
+coh comp2 C (x2(f2)y2(g2)z2) : x2 => z2
+
+coh testcoh C (x(f)y(g)z) : comp f g => comp2 f g
+
+let test {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+    : _ = testcoh f g
diff --git a/examples/syllepsis.catt b/examples/syllepsis.catt
new file mode 100644
index 0000000..516e947
--- /dev/null
+++ b/examples/syllepsis.catt
@@ -0,0 +1,360 @@
+############################################
+#
+#  syllepsis.catt - the syllepsis
+#
+############################################
+
+############################################
+#
+#  prelude.catt - some basic coherences
+#
+############################################
+
+#
+#  Identities
+#
+
+coh id C (x) : x => x
+
+coh id1 C (x(f)y)
+  : f => f
+
+coh id2 C (x(f(a)g)y)
+  : a => a
+
+#
+#  1d compositions
+#
+
+coh comp110 C (x(f)y(g)z)
+  : x => z
+
+#
+#  2d compositions
+#
+
+coh comp221 C (x(f(a)g(b)h)y)
+  : f => h
+
+coh comp22211 C (x(f(a)g(b)h(c)i)y)
+  : f => i
+
+coh comp2222111 C (x(f(a)g(b)h(c)i(d)j)y)
+  : f => j
+
+coh comp220 C (x(f(a)g)y(h(b)k)z)
+  : comp110 f h => comp110 g k
+
+coh comp210 C (x(f(a)g)y(h)z)
+  : comp110 f h => comp110 g h
+
+coh comp120 C (x(f)y(g(a)h)z)
+  : comp110 f g => comp110 f h
+
+#
+#  3d Compositions
+#
+
+coh comp330 C (x(f(a(m)b)g)y(h(c(n)d)k)z)
+  : comp220 a c => comp220 b d
+
+coh comp331 C (x(f(a(m)b)g(c(n)d)h)y)
+  : comp221 a c => comp221 b d
+
+coh comp332 C (x(f(a(m)b(n)c)g)y)
+  : a => c
+
+coh comp321 C (x(f(a(m)b)g(c)h)y)
+  : comp221 a c => comp221 b c
+
+coh comp32211 C (x(f(a(m)b)g(c)h(d)i)y)
+  : comp22211 a c d => comp22211 b c d
+
+coh comp23211 C (x(f(a)g(b(m)c)h(d)i)y)
+  : comp22211 a b d => comp22211 a c d
+
+coh comp2322111 C (x(f(a)g(b(m)c)h(d)i(e)j)y)
+  : comp2222111 a b d e => comp2222111 a c d e
+
+coh comp33322 C (x(f(a(m)b(n)c(o)d)g)y)
+  : a => d
+
+coh comp231 C (x(f(a)g(c(n)d)h)y)
+  : comp221 a c => comp221 a d
+
+coh comp310 C (x(f(a(m)b)g)y(h)z)
+  : comp210 a h => comp210 b h
+
+coh comp130 C (x(f)y(h(c(n)d)k)z)
+  : comp120 f c => comp120 f d
+
+
+coh comp230 C (x(f(a)g)y(h(c(n)d)k)z)
+  : comp220 a c => comp220 a d
+
+coh comp320 C (x(f(a(m)b)g)y(h(c)k)z)
+  : comp220 a c => comp220 b c
+
+coh assoc3 C (x(f(a(m)b(n)c(o)d)g)y)
+  : comp332 (comp332 m n) o =>
+    comp332 m (comp332 n o)
+
+coh assoc3inv C (x(f(a(m)b(n)c(o)d)g)y)
+  : comp332 m (comp332 n o) =>
+    comp332 (comp332 m n) o
+
+#
+#  4d compositions
+#
+
+coh comp140 C (x(f)y(h(c(n(q)m)d)k)z)
+  : comp130 f n => comp130 f m
+
+coh comp432 C (x(f(a(m(q)o)b(n)c)g)y)
+  : comp332 m n => comp332 o n
+
+coh comp342 C (x(f(a(m)b(n(q)o)c)g)y)
+  : comp332 m n => comp332 m o
+
+coh comp443 C (x(f(a(m(p)n(q)o)b)g)y)
+  : m => o
+
+coh comp340 C (x(f(a(m)b)g)y(h(c(n(p)o)d)i)z)
+  : comp330 m n => comp330 m o
+
+coh comp44433 C (x(f(a(b0(t1)b1(t2)b2(t3)b3)b)g)y)
+  : b0 => b3
+
+coh comp444443333 C (x(f(a(b0(t1)b1(t2)b2(t3)b3(t4)b4(t5)b5)b)g)y)
+  : b0 => b5
+
+#
+#  Simple coherences
+#
+
+coh unitl C (x(f)y)
+  : f => comp110 (id x) f
+
+coh unitr C (x(f)y)
+  : comp110 (id x) f => f
+
+coh assoc_r C (x(f)y(g)z(h)w)
+  : comp110 (comp110 f g) h => comp110 f (comp110 g h)
+
+coh assoc_l C (x(f)y(g)z(h)w)
+  : comp110 f (comp110 g h) => comp110 (comp110 f g) h
+
+
+#
+#  Eckman-Hilton coherence 3-cell
+#
+
+coh swap3 C (x(f(a)g)y(h(b)k)z)
+  : comp221 (comp210 a h) (comp120 g b) =>
+    comp221 (comp120 f b) (comp210 a k)
+
+coh swap3inv C (x(f(a)g)y(h(b)k)z)
+  : comp221 (comp120 f b) (comp210 a k) =>
+    comp221 (comp210 a h) (comp120 g b)
+
+#
+#  Suspended Eckman-Hilton coherence 4-cell
+#
+
+coh swap4 C (u(x(f(a)g)y(h(b)k)z)v)
+  : comp332 (comp321 a h) (comp231 g b) =>
+    comp332 (comp231 f b) (comp321 a k)
+
+coh swap4inv C (u(x(f(a)g)y(h(b)k)z)v)
+  : comp332 (comp231 f b) (comp321 a k) =>
+    comp332 (comp321 a h) (comp231 g b)
+
+#
+#  Left vertical coherence
+#
+
+let step1l {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (comp321 (comp310 a s) (comp120 y h)) (comp231 (comp210 g s) (comp130 y b))) (swap3 g k) =>
+    comp332 (comp321(comp310 a s) (comp120 y h)) (comp332 (comp231 (comp210 g s) (comp130 y b)) (swap3 g k)) ]
+  = assoc3 (comp321(comp310 a s) (comp120 y h)) (comp231 (comp210 g s) (comp130 y b)) (swap3 g k)
+
+coh step2lcoh C (u(x(g)y)v(s(h(b)k)t)w)
+  : comp332 (comp231 (comp210 g s) (comp130 y b)) (swap3 g k) =>
+    comp332 (swap3 g h) (comp321 (comp130 x b) (comp210 g t))
+
+let step2l {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp321 (comp310 a s) (comp120 y h)) (comp332 (comp231 (comp210 g s) (comp130 y b)) (swap3 g k)) =>
+    comp332 (comp321 (comp310 a s) (comp120 y h)) (comp332 (swap3 g h) (comp321(comp130 x b) (comp210 g t))) ]
+  = comp342 (comp321 (comp310 a s) (comp120 y h)) (step2lcoh g b)
+
+let step3l {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp321 (comp310 a s) (comp120 y h)) (comp332 (swap3 g h) (comp321 (comp130 x b) (comp210 g t))) =>
+    comp332 (comp332 (comp321 (comp310 a s) (comp120 y h)) (swap3 g h)) (comp321 (comp130 x b) (comp210 g t)) ]
+  = assoc3inv (comp321 (comp310 a s) (comp120 y h)) (swap3 g h) (comp321 (comp130 x b) (comp210 g t))
+
+coh step4lcoh C (u(x(f(a)g)y)v(s(h)t)w)
+  : comp332 (comp321 (comp310 a s) (comp120 y h)) (swap3 g h) =>
+    comp332 (swap3 f h) (comp231 (comp120 x h) (comp310 a t))
+
+let step4l {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (comp321 (comp310 a s) (comp120 y h)) (swap3 g h)) (comp321 (comp130 x b) (comp210 g t)) =>
+    comp332 (comp332 (swap3 f h) (comp231 (comp120 x h) (comp310 a t))) (comp321 (comp130 x b) (comp210 g t)) ]
+  = comp432 (step4lcoh a h) (comp321 (comp130 x b) (comp210 g t))
+
+let step5l {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (swap3 f h) (comp231 (comp120 x h) (comp310 a t))) (comp321 (comp130 x b) (comp210 g t)) =>
+    comp332 (swap3 f h) (comp332 (comp231 (comp120 x h) (comp310 a t)) (comp321 (comp130 x b) (comp210 g t))) ]
+  = assoc3 (swap3 f h) (comp231 (comp120 x h) (comp310 a t)) (comp321 (comp130 x b) (comp210 g t))
+
+let vert_left {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (comp321 (comp310 a s) (comp120 y h)) (comp231 (comp210 g s) (comp130 y b))) (swap3 g k) =>
+    comp332 (swap3 f h) (comp332 (comp231 (comp120 x h) (comp310 a t)) (comp321 (comp130 x b) (comp210 g t))) ]
+  = comp444443333 (step1l a b) (step2l a b) (step3l a b) (step4l a b) (step5l a b)
+
+#
+#  Right vertical coherence
+#
+
+let step1r {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (comp231 (comp210 f s) (comp130 y b)) (comp321 (comp310 a s) (comp120 y k))) (swap3 g k) =>
+    comp332 (comp231 (comp210 f s) (comp130 y b)) (comp332 (comp321 (comp310 a s) (comp120 y k)) (swap3 g k)) ]
+  = assoc3 (comp231 (comp210 f s) (comp130 y b)) (comp321 (comp310 a s) (comp120 y k)) (swap3 g k)
+
+coh step2rcoh C (u(x(f(a)g)y)v(s(k)t)w)
+  : comp332 (comp321 (comp310 a s) (comp120 y k)) (swap3 g k) =>
+    comp332 (swap3 f k) (comp231 (comp120 x k) (comp310 a t))
+
+let step2r {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp231 (comp210 f s) (comp130 y b)) (comp332 (comp321 (comp310 a s) (comp120 y k)) (swap3 g k)) =>
+    comp332 (comp231 (comp210 f s) (comp130 y b)) (comp332 (swap3 f k) (comp231 (comp120 x k) (comp310 a t))) ]
+  = comp342 (comp231 (comp210 f s) (comp130 y b)) (step2rcoh a k)
+
+let step3r {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp231 (comp210 f s) (comp130 y b)) (comp332 (swap3 f k) (comp231 (comp120 x k) (comp310 a t))) =>
+    comp332 (comp332 (comp231 (comp210 f s) (comp130 y b)) (swap3 f k)) (comp231 (comp120 x k) (comp310 a t)) ]
+  = assoc3inv (comp231(comp210 f s) (comp130 y b)) (swap3 f k) (comp231 (comp120 x k) (comp310 a t))
+
+coh step4rcoh C (u(x(f)y)v(s(h(b)k)t)w)
+  : comp332 (comp231 (comp210 f s) (comp130 y b)) (swap3 f k) =>
+    comp332 (swap3 f h) (comp321 (comp130 x b) (comp210 f t))
+
+let step4r {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (comp231 (comp210 f s) (comp130 y b)) (swap3 f k)) (comp231 (comp120 x k) (comp310 a t)) =>
+    comp332 (comp332 (swap3 f h) (comp321 (comp130 x b) (comp210 f t))) (comp231 (comp120 x k) (comp310 a t)) ]
+  = comp432 (step4rcoh f b) (comp231 (comp120 x k) (comp310 a t))
+
+let step5r {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (swap3 f h) (comp321 (comp130 x b) (comp210 f t))) (comp231 (comp120 x k) (comp310 a t)) =>
+    comp332 (swap3 f h) (comp332 (comp321 (comp130 x b) (comp210 f t)) (comp231 (comp120 x k) (comp310 a t))) ]
+  = assoc3 (swap3 f h) (comp321 (comp130 x b) (comp210 f t)) (comp231 (comp120 x k) (comp310 a t))
+
+let vert_right {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : [ comp332 (comp332 (comp231 (comp210 f s) (comp130 y b)) (comp321 (comp310 a s) (comp120 y k))) (swap3 g k) =>
+    comp332 (swap3 f h) (comp332 (comp321 (comp130 x b) (comp210 f t)) (comp231 (comp120 x k) (comp310 a t))) ]
+  = comp444443333 (step1r a b) (step2r a b) (step3r a b) (step4r a b) (step5r a b)
+
+#
+#  The Syllepsis
+#
+
+coh five_cell {C : Cat}
+    {u :: C}
+    {v :: C} {x :: u => v}
+             {y :: u => v} {f :: x => y}
+                           {g :: x => y} (a :: f => g)
+    {w :: C} {s :: v => w}
+             {t :: v => w} {h :: s => t}
+                           {k :: s => t} (b :: h => k)
+  : comp443 (comp432 (swap4 (comp310 a s) (comp130 y b)) (swap3 g k)) (vert_right a b) =>
+    comp443 (vert_left a b) (comp342 (swap3 f h) (swap4inv (comp130 x b) (comp310 a t)))
+
+let syllepsis {C : Cat}
+    {x :: C}
+    (a :: id1(id x) => id1(id x))
+    (b :: id1(id x) => id1(id x))
+  : [ swap4 a b => swap4inv b a ]
+  = five_cell a b
diff --git a/examples/syllepsisterm.txt b/examples/syllepsisterm.txt
new file mode 100644
index 0000000..8f009fd
--- /dev/null
+++ b/examples/syllepsisterm.txt
@@ -0,0 +1,948 @@
+\{C}. \{x}. \a. \b. coh [ C (u(x(f(a)g)y)v(s(h(b)k)t)w) :
+                          coh [ C (x1(x3(x5(m(p)x7(t2)x7(t4)x7)x6)x4)x2) :
+                               m => x7]
+                           (coh [ C (x(f(a(m)b(n)c(n)c)g)y) : a => c]
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 f s)
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 y b))
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a s)
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 y k))
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               g k))
+                           (coh [ C (x(f(a(m(q)o)b(n)c)g)y) :
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m n =>
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] o n]
+                             (coh [ C (u(x(f(a)g)y(h(b)k)z)v) :
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      a h)
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      g b) =>
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      f b)
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      a k)]
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a s)
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 y b))
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               g k))
+                           (coh [ C (x(f(a(m)a(m)b(n)c)g)y) : a => c]
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 f s)
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 y b))
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               f k)
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 x k)
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a t)))
+                           (coh [ C (x(f(a(m)b(n(q)o)c)g)y) :
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m n =>
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m o]
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 f s)
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 y b))
+                             (coh [ C (u(x(f(a)g)y)v(s(k)t)w) :
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h =>
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             b h]
+                                        a s)
+                                      (coh [ C (x(f)y(g(a)h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f g =>
+                                            coh [ C (x(f)y(g)z) : x => z] f h]
+                                        y k))
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      g k) =>
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      f k)
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      (coh [ C (x(f)y(g(a)h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f g =>
+                                            coh [ C (x(f)y(g)z) : x => z] f h]
+                                        x k)
+                                      (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h =>
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             b h]
+                                        a t))]
+                               a k))
+                           (coh [ C (x(f(a(m)b(n)c(n)c)g)y) : a => c]
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               f h)
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 x b)
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 f t))
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 x k)
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a t)))
+                           (coh [ C (x(f(a(m(q)o)b(n)c)g)y) :
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m n =>
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] o n]
+                             (coh [ C (u(x(f)y)v(s(h(b)k)t)w) :
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      (coh [ C (x(f(a)g)y(h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f h =>
+                                            coh [ C (x(f)y(g)z) : x => z] g h]
+                                        f s)
+                                      (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f c =>
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f d]
+                                        y b))
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      f k) =>
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      f h)
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f c =>
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f d]
+                                        x b)
+                                      (coh [ C (x(f(a)g)y(h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f h =>
+                                            coh [ C (x(f)y(g)z) : x => z] g h]
+                                        f t))]
+                               f b)
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 x k)
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a t))) =>
+                          coh [ C (x1(x3(x5(x7(t2)x7(t4)x7(q)o)x6)x4)x2) :
+                               x7 => o]
+                           (coh [ C (x(f(a(m)b(n)c(n)c)g)y) : a => c]
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a s)
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 y h))
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 g s)
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 y b))
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               g k))
+                           (coh [ C (x(f(a(m)a(m)b(n)c)g)y) : a => c]
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a s)
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 y h))
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               g h)
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 x b)
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 g t)))
+                           (coh [ C (x(f(a(m)b(n(q)o)c)g)y) :
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m n =>
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m o]
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a s)
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 y h))
+                             (coh [ C (u(x(g)y)v(s(h(b)k)t)w) :
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      (coh [ C (x(f(a)g)y(h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f h =>
+                                            coh [ C (x(f)y(g)z) : x => z] g h]
+                                        g s)
+                                      (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f c =>
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f d]
+                                        y b))
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      g k) =>
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      g h)
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f c =>
+                                            coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f d]
+                                        x b)
+                                      (coh [ C (x(f(a)g)y(h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f h =>
+                                            coh [ C (x(f)y(g)z) : x => z] g h]
+                                        g t))]
+                               g b))
+                           (coh [ C (x(f(a(m)b(n)c(n)c)g)y) : a => c]
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               f h)
+                             (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                               (coh [ C (x(f)y(g(a)h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f g =>
+                                     coh [ C (x(f)y(g)z) : x => z] f h]
+                                 x h)
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a t))
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 x b)
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 g t)))
+                           (coh [ C (x(f(a(m(q)o)b(n)c)g)y) :
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m n =>
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] o n]
+                             (coh [ C (u(x(f(a)g)y)v(s(h)t)w) :
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h =>
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             b h]
+                                        a s)
+                                      (coh [ C (x(f)y(g(a)h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f g =>
+                                            coh [ C (x(f)y(g)z) : x => z] f h]
+                                        y h))
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      g h) =>
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h)
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             g b) =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h]
+                                           (coh [ C (x(f)y(g(a)h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f g =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h]
+                                             f b)
+                                           (coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a k)]
+                                      f h)
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      (coh [ C (x(f)y(g(a)h)z) :
+                                            coh [ C (x(f)y(g)z) : x => z] f g =>
+                                            coh [ C (x(f)y(g)z) : x => z] f h]
+                                        x h)
+                                      (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             a h =>
+                                            coh [ C (x(f(a)g)y(h)z) :
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  f h =>
+                                                 coh [ C (x(f)y(g)z) : x => z]
+                                                  g h]
+                                             b h]
+                                        a t))]
+                               a h)
+                             (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 x b)
+                               (coh [ C (x(f(a)g)y(h)z) :
+                                     coh [ C (x(f)y(g)z) : x => z] f h =>
+                                     coh [ C (x(f)y(g)z) : x => z] g h]
+                                 g t)))
+                           (coh [ C (x(f(a(m)b(n(q)o)c)g)y) :
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m n =>
+                                 coh [ C (x(f(a(m)b(n)c)g)y) : a => c] m o]
+                             (coh [ C (x(f(a)g)y(h(b)k)z) :
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h)
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      g b) =>
+                                   coh [ C (x(f(a)g(b)h)y) : f => h]
+                                    (coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f b)
+                                    (coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a k)]
+                               f h)
+                             (coh [ C (u(x(f(a)g)y(h(b)k)z)v) :
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      f b)
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      a k) =>
+                                   coh [ C (x(f(a(m)b(n)c)g)y) : a => c]
+                                    (coh [ C (x(f(a(m)b)g(c)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] b c]
+                                      a h)
+                                    (coh [ C (x(f(a)g(c(n)d)h)y) :
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a c =>
+                                          coh [ C (x(f(a)g(b)h)y) : f => h] a d]
+                                      g b)]
+                               (coh [ C (x(f)y(h(c(n)d)k)z) :
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f c =>
+                                     coh [ C (x(f)y(g(a)h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f g =>
+                                          coh [ C (x(f)y(g)z) : x => z] f h]
+                                      f d]
+                                 x b)
+                               (coh [ C (x(f(a(m)b)g)y(h)z) :
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      a h =>
+                                     coh [ C (x(f(a)g)y(h)z) :
+                                          coh [ C (x(f)y(g)z) : x => z] f h =>
+                                          coh [ C (x(f)y(g)z) : x => z] g h]
+                                      b h]
+                                 a t)))]
+  a b
diff --git a/examples/syllepsistree.txt b/examples/syllepsistree.txt
new file mode 100644
index 0000000..ae4fc09
--- /dev/null
+++ b/examples/syllepsistree.txt
@@ -0,0 +1 @@
+[[[][][[][][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][[[][][][]][[][][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]]][[][][[][][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][[[][][][]][[][][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]]][][]]
diff --git a/lib/eval.ml b/lib/eval.ml
index 8a4b599..509692c 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -88,35 +88,46 @@ and appV t u ict =
   match t with
   | FlexV (m,sp) -> FlexV (m,AppSp(sp,u,ict))
   | RigidV (i,sp) -> RigidV (i,AppSp(sp,u,ict))
+  | TopV (nm,sp,CohV (cn,pd,c,s,t,spc)) ->
+     let sp' = AppSp (spc,u,ict) in
+     let x = CohV (cn,pd,c,s,t,sp') in
+     (match cohReduction cn pd c s t sp' u with
+      | Error s when s = "Not applied all arguments yet" -> TopV (nm,AppSp(sp,u,ict),x)
+      | Error _ -> (* pr "No reduction: %a because %s\n\n" pp_value x y; *) TopV (nm,AppSp(sp,u,ict),x)
+      | Ok y -> (* pr "Successful reduction %a to %a@," pp_value x pp_value y; *) y)
+  | TopV (_,_,LamV(_,_,cl)) -> cl $$ u
   | TopV (nm,sp,tv) -> TopV (nm,AppSp(sp,u,ict),appV tv u ict)
   | LamV (_,_,cl) -> cl $$ u
   | UCompV (ucd,cohv,sp) -> UCompV (ucd,appV cohv u ict,AppSp(sp,u,ict))
   | CohV (cn,pd,c,s,t,sp) ->
      let sp' = AppSp(sp,u,ict) in
      let x = CohV (cn,pd,c,s,t,sp') in
-     (match sp_to_suite sp' with
-     | Error _ -> x
-     | Ok (sp_list) ->
-        let k = length sp_list in
-        if k = pd_length pd + 1 then
-       (match alt (alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u)) (endo_coherence_removal cn pd k c s t sp_list) with
-        | Error _ ->
-           (* pr "Attempted reduction on %a: %s\n" pp_value x y; *)
-           x
-       | Ok y -> y) else x)
+     (match cohReduction cn pd c s t sp' u with
+      | Error s when s = "Not applied all arguments yet" -> x
+      | Error _ -> (* pr "No reduction: %a because %s\n\n" pp_value x y; *) x
+      | Ok y -> y)
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
 
+and cohReduction cn pd c s t sp' u =
+  let* sp_list = sp_to_suite sp' in
+  let k = length sp_list in
+  if k = pd_length pd + 1 then
+    alt (alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u)) (endo_coherence_removal cn pd k c s t sp_list) else Error "Not applied all arguments yet"
+
 and dim_ty ty =
     match ty with
     | HomV (c,_,_) -> dim_ty c + 1
     | _ -> 0
 
-and insertionCoh cn pd c s t args =
-
-  let unfold v =
+and unfold v =
     match force_meta v with
     | TopV (_,_,x) -> x
-    | y -> y in
+
+    | y -> y
+
+and insertionCoh cn pd c s t args =
+
+
 
   let rec type_linearity c s t =
     match (unfold s, unfold t) with
@@ -213,6 +224,31 @@ and disc_removal pd c s t u =
     if HomV(c,s,t) = construct_disc_type (dim_pd pd) then Ok u
     else Error "Disc is not unbiased"
 
+(* Can this somehow bu merged with unify? *)
+and is_same l a b =
+  match (unfold a, unfold b) with
+  | (TypV , TypV) -> true
+  | (CatV , CatV) -> true
+  | (LamV (_,_,a) , LamV (_,_,a')) -> is_same (l + 1) (a $$ varV l) (a' $$ varV l)
+  | (PiV (_,_,a,b), PiV (_,_,a',b')) -> is_same l a a' && is_same (l+1) (b $$ varV l) (b' $$ varV l)
+  | (RigidV(i,sp), RigidV (i',sp')) when i = i' -> is_same_sp l sp sp'
+  | (FlexV(m,sp), FlexV(m',sp')) when m = m' -> is_same_sp l sp sp'
+  | (ObjV c, ObjV c') -> is_same l c c'
+  | (HomV (c,s,t), HomV (c',s',t')) -> is_same l c c' && is_same l s s' && is_same l t t'
+  | (ArrV c, ArrV c') -> is_same l c c'
+  | (CohV (_,pd,c,s,t,sp), CohV (_,pd',c',s',t',sp')) when Pd.shape_eq pd pd' ->
+     is_same l (HomV(c,s,t)) (HomV(c',s',t')) && is_same_sp l sp sp'
+  | _ -> a = b
+
+and is_same_sp l sp sp' =
+  match (sp, sp') with
+  | (EmpSp,EmpSp) -> true
+  | (AppSp (s,u,_), AppSp (s', u', _)) -> is_same_sp l s s' && is_same l u u'
+  | (BaseSp s, BaseSp s') -> is_same_sp l s s'
+  | (LidSp s, LidSp s') -> is_same_sp l s s'
+  | (CoreSp s, CoreSp s') -> is_same_sp l s s'
+  | _ -> false
+
 and endo_coherence_removal cn pd k c s t sp_list =
   (* Can't open syntax here: Must be a way to fix this *)
   let fresh_pd pd =
@@ -224,7 +260,7 @@ and endo_coherence_removal cn pd k c s t sp_list =
     match ty with
     | HomV(a,b,c) -> Ext(Ext(type_to_suite a, (b,Impl)), (c,Impl))
     | _ -> Emp in
-  if not (s = t) then Error "Not an endo coherence"
+  if not (is_same 0 s t) then Error "Not an endo coherence"
   else
     let dim = dim_ty c in
     let new_pd = fresh_pd (unit_disc_pd dim) in
@@ -484,3 +520,24 @@ let rec value_to_cyl_typ (cat : value) : (value * value cyl_typ , string) Result
     Ok (bc, ct |> ((baseV s, lidV s, coreV s),
                    (baseV t, lidV t, coreV t)))
   | _ -> Error "Not a cylinder type"
+
+let rec syntax_tree k v =
+  match force_meta v with
+  | FlexV _ -> Ok "[]"
+  | RigidV _ -> Ok "[]"
+  | TopV (_,_,tv) -> syntax_tree k tv
+  | LamV (_,_,cl) -> syntax_tree (k+1) (cl $$ varV k)
+  | PiV (_,_,_,_) -> Error "No implementation"
+  | ObjV c -> syntax_tree k c
+  | HomV (_,s,t) ->
+     let* s' = syntax_tree k s in
+     let* t' = syntax_tree k t in
+     Ok (String.concat "" [s';t'])
+  | UCompV _ -> Error "No implementation"
+  | CohV (_,_,_,s,t,sp) ->
+     let* sp_suite = sp_to_suite sp in
+     let* s' = syntax_tree k s in
+     let* t' = syntax_tree k t in
+     let* sp' = map_suite_m sp_suite ~f:(fun (v,ict) -> if ict = Expl then syntax_tree k v else Ok "") in
+     Ok (Printf.sprintf "[%s%s%s]" s' t' (String.concat "" (to_list sp')))
+  | _ -> Error "No implementaiton"
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index f0e1eba..9820031 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -591,8 +591,11 @@ let rec check_defs gma defs =
     pr "Term: @[%a@]@," pp_expr tm_nf;
     let tm_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) tm_val) in
     let ty_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) ty_val) in
-    pr "Type unfolded: @[%a@]@," pp_expr ty_unfolded_nf;
-    pr "Term unfolded: @[%a@]@," pp_expr tm_unfolded_nf;
+    (match syntax_tree 0 tm_val with
+     | Ok s -> pr "Term syntax tree: @[%s@]@," s
+     | Error y -> pr "Could not print syntax tree: %s" y);
+    pr "Type unfolded:@, @[%a@]@," pp_expr ty_unfolded_nf;
+    pr "Term unfolded:@, @[%a@]@," pp_expr tm_unfolded_nf;
     check_defs (define gma id tm_val ty_val) ds
   | (CohDef (id,g,c,s,t))::ds ->
     pr "----------------@,";

From ba3454c45d01dfadb6c839bab505524efb0b9a4f Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Mon, 26 Apr 2021 17:00:02 +0100
Subject: [PATCH 12/14] UComp seems to be working with reduction now

---
 examples/syllepsis.catt |  2 +-
 lib/eval.ml             | 18 ++++++++++++++----
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/examples/syllepsis.catt b/examples/syllepsis.catt
index 516e947..a1f115a 100644
--- a/examples/syllepsis.catt
+++ b/examples/syllepsis.catt
@@ -349,7 +349,7 @@ coh five_cell {C : Cat}
     {w :: C} {s :: v => w}
              {t :: v => w} {h :: s => t}
                            {k :: s => t} (b :: h => k)
-  : comp443 (comp432 (swap4 (comp310 a s) (comp130 y b)) (swap3 g k)) (vert_right a b) =>
+  : ucomp [ 4 3 4 ] (comp432 (swap4 (comp310 a s) (comp130 y b)) (swap3 g k)) (vert_right a b) =>
     comp443 (vert_left a b) (comp342 (swap3 f h) (swap4inv (comp130 x b) (comp310 a t)))
 
 let syllepsis {C : Cat}
diff --git a/lib/eval.ml b/lib/eval.ml
index 509692c..d6f78e9 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -92,13 +92,23 @@ and appV t u ict =
      let sp' = AppSp (spc,u,ict) in
      let x = CohV (cn,pd,c,s,t,sp') in
      (match cohReduction cn pd c s t sp' u with
-      | Error s when s = "Not applied all arguments yet" -> TopV (nm,AppSp(sp,u,ict),x)
       | Error _ -> (* pr "No reduction: %a because %s\n\n" pp_value x y; *) TopV (nm,AppSp(sp,u,ict),x)
       | Ok y -> (* pr "Successful reduction %a to %a@," pp_value x pp_value y; *) y)
   | TopV (_,_,LamV(_,_,cl)) -> cl $$ u
+  | TopV (nm,sp2,UCompV(ucd, CohV (cn,pd,c,s,t,spc), sp)) ->
+     let sp' = AppSp (spc,u,ict) in
+     (match cohReduction cn pd c s t sp' u with
+      | Error _ -> TopV (nm, AppSp(sp2,u,ict), UCompV (ucd, CohV(cn,pd,c,s,t,sp'), AppSp(sp,u,ict)))
+      | Ok y -> y
+     )
   | TopV (nm,sp,tv) -> TopV (nm,AppSp(sp,u,ict),appV tv u ict)
   | LamV (_,_,cl) -> cl $$ u
-  | UCompV (ucd,cohv,sp) -> UCompV (ucd,appV cohv u ict,AppSp(sp,u,ict))
+  | UCompV (ucd,CohV (cn,pd,c,s,t,spc),sp) ->
+     let sp' = AppSp (spc,u,ict) in
+     let x = CohV (cn,pd,c,s,t,sp') in
+     (match cohReduction cn pd c s t sp' u with
+      | Error _ -> UCompV(ucd, x, AppSp(sp,u,ict))
+      | Ok y -> y)
   | CohV (cn,pd,c,s,t,sp) ->
      let sp' = AppSp(sp,u,ict) in
      let x = CohV (cn,pd,c,s,t,sp') in
@@ -121,8 +131,8 @@ and dim_ty ty =
 
 and unfold v =
     match force_meta v with
-    | TopV (_,_,x) -> x
-
+    | TopV (_,_,x) -> unfold x
+    | UCompV (_,cohv,_) -> cohv
     | y -> y
 
 and insertionCoh cn pd c s t args =

From 001068699de6d9692825650311e2a4bfc58d8f3d Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Tue, 18 May 2021 17:11:24 +0100
Subject: [PATCH 13/14] Add restriction to pruning

---
 examples/reduct-pruning.catt    | 13 +++++++++++++
 examples/syllepsistreeprune.txt |  1 +
 lib/eval.ml                     | 24 ++++++++++++++++++------
 lib/pd.ml                       |  2 +-
 lib/typecheck.ml                | 22 +++++++++++-----------
 5 files changed, 44 insertions(+), 18 deletions(-)
 create mode 100644 examples/reduct-pruning.catt
 create mode 100644 examples/syllepsistreeprune.txt

diff --git a/examples/reduct-pruning.catt b/examples/reduct-pruning.catt
new file mode 100644
index 0000000..02e2404
--- /dev/null
+++ b/examples/reduct-pruning.catt
@@ -0,0 +1,13 @@
+coh id {C : Cat} (x :: C)
+  : x => x
+
+coh comp {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+    {z :: C} (g :: y => z)
+  : x => z
+
+let prune_l {C : Cat}
+    {x :: C}
+    {y :: C} (f :: x => y)
+  : [ x => y ] = comp (id x) f
diff --git a/examples/syllepsistreeprune.txt b/examples/syllepsistreeprune.txt
new file mode 100644
index 0000000..4bb19e4
--- /dev/null
+++ b/examples/syllepsistreeprune.txt
@@ -0,0 +1 @@
+[[[][][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[][][][]][]][[][][][[][][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][][]]][[[][][][[][][][]]][[][][[][][][]][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][[[][][[][][][]][]][[][][][[][][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]]]][[][][[][][[[][][[][][][]][]][[][][][[][][][]]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[[][][][]][[][][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][][]]][[[][][][[][][][]]][[][][[][][][]][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]]][[][][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]][][]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]][[[][][[][][][]][]][[][][][[][][][]]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][][]][[][][][]][[[][][][]][[][][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]][[[][][][]][[][][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[][][][]][[][][][]][][]]]]][[[][][][]][[][][][]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][][]][[[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[][][[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]][[[[][][][]][[][][][]][][]][[[][][][]][[][][][]][][]][][]]]]][][]]
diff --git a/lib/eval.ml b/lib/eval.ml
index d6f78e9..9f76f16 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -122,7 +122,7 @@ and cohReduction cn pd c s t sp' u =
   let* sp_list = sp_to_suite sp' in
   let k = length sp_list in
   if k = pd_length pd + 1 then
-    alt (alt (insertionCoh cn pd c s t sp_list) (disc_removal pd c s t u)) (endo_coherence_removal cn pd k c s t sp_list) else Error "Not applied all arguments yet"
+    alt (alt (insertionCoh cn pd c s t sp_list false) (disc_removal pd c s t u)) (endo_coherence_removal cn pd k c s t sp_list) else Error "Not applied all arguments yet"
 
 and dim_ty ty =
     match ty with
@@ -135,9 +135,7 @@ and unfold v =
     | UCompV (_,cohv,_) -> cohv
     | y -> y
 
-and insertionCoh cn pd c s t args =
-
-
+and insertionCoh cn pd c s t args only_prune =
 
   let rec type_linearity c s t =
     match (unfold s, unfold t) with
@@ -149,6 +147,20 @@ and insertionCoh cn pd c s t args =
   let rec get_redex xs =
     match xs with
     | Emp -> Error "No redex found"
+    | Ext (xs, ((_,_,_,_,t), redex_path)) when only_prune ->
+       (match (unfold t) with
+        | CohV (cn', pd', c', s', t', sp') ->
+           let* args_inner = sp_to_suite sp' in
+           let pda = map_pd_lvls pd' 1 ~f:(fun _ n _ (nm, ict) -> let (v,_) = nth n args_inner in (false, n , nm , ict, v)) in
+           let dim = dim_pd pd' in
+           let cond1 = is_disc pd' in
+           let cond2 = is_same 0
+                  (HomV (construct_disc_type dim, RigidV (2*dim + 1,EmpSp), RigidV (2*dim + 1,EmpSp)))
+                  (HomV (c', s', t')) in
+           if cond1 && cond2
+           then Ok (cn', pd', c', s', t', pda, redex_path)
+           else get_redex xs
+        | _ -> get_redex xs)
     | Ext (xs, ((_,_,_,_,t), redex_path)) ->
        match (unfold t) with
        | CohV (cn', pd', c', s', t', sp') ->
@@ -231,7 +243,7 @@ and disc_removal pd c s t u =
 
   if not (is_disc pd) then Error "Not disc"
   else
-    if HomV(c,s,t) = construct_disc_type (dim_pd pd) then Ok u
+    if is_same 0 (HomV(c,s,t)) (construct_disc_type (dim_pd pd)) then Ok u
     else Error "Disc is not unbiased"
 
 (* Can this somehow bu merged with unify? *)
@@ -532,7 +544,7 @@ let rec value_to_cyl_typ (cat : value) : (value * value cyl_typ , string) Result
   | _ -> Error "Not a cylinder type"
 
 let rec syntax_tree k v =
-  match force_meta v with
+  match unfold v with
   | FlexV _ -> Ok "[]"
   | RigidV _ -> Ok "[]"
   | TopV (_,_,tv) -> syntax_tree k tv
diff --git a/lib/pd.ml b/lib/pd.ml
index ce39dab..0c52a07 100644
--- a/lib/pd.ml
+++ b/lib/pd.ml
@@ -444,7 +444,7 @@ let fold_pd_with_type pd init f =
     | Br (x,brs) ->
       let ct = if (is_empty brs)
         then LocMaxCell d
-        else SrcCell d in 
+        else SrcCell d in
       let b' = f x ct b in
       fold_pd_with_type_brs true d brs b'
 
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index 9820031..0a7a297 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -141,13 +141,13 @@ type typing_error = [
 let pp_error ppf e =
   match e with
   | `NameNotInScope nm -> Fmt.pf ppf "Name not in scope: %s" nm
-  | `TypeMismatch msg -> Fmt.pf ppf "%s" msg  
+  | `TypeMismatch msg -> Fmt.pf ppf "%s" msg
   | `PastingError msg -> Fmt.pf ppf "Error while checking pasting context: %s" msg
-  | `FullnessError msg -> Fmt.pf ppf "Fullness error: %s" msg 
+  | `FullnessError msg -> Fmt.pf ppf "Fullness error: %s" msg
   | `IcityMismatch (_, _) -> Fmt.pf ppf "Icity mismatch"
-  | `BadCohQuot msg -> Fmt.pf ppf "%s" msg 
+  | `BadCohQuot msg -> Fmt.pf ppf "%s" msg
   | `NotImplemented f -> Fmt.pf ppf "Feature not implemented: %s" f
-  | `InvalidCylinder msg -> Fmt.pf ppf "Invalid cylinder: %s" msg 
+  | `InvalidCylinder msg -> Fmt.pf ppf "Invalid cylinder: %s" msg
   | `InternalError -> Fmt.pf ppf "Internal Error"
 
 let rec check gma expr typ =
@@ -196,7 +196,7 @@ let rec check gma expr typ =
 
        (* log_msg "checking cylinder";
         * log_val "bc" bc pp_value; *)
-       
+
        let btyp = ObjV (C.sph_to_cat bc (base_sph ct)) in
        let ltyp = ObjV (C.sph_to_cat bc (lid_sph ct)) in
 
@@ -211,7 +211,7 @@ let rec check gma expr typ =
 
        (* we "desuspend" so that all coherences are taken as low as
           possible *)
-       let (bbc,bsph) = C.match_homs bc in 
+       let (bbc,bsph) = C.match_homs bc in
        let ctyp = ObjV (C.sph_to_cat bbc
                           (C.core_sph bbc (bsph,to_list ct) bv lv)) in
 
@@ -467,11 +467,11 @@ and check_coh gma g c s t =
 
               if (not (Set.is_subset pd_src_vars ~of_:tot_src_vars)) then
                 let msg = Fmt.str "@[<v>Non-full source:@,pd: @[%a@]@,src: @[%a@]@,"
-                    (pp_tele pp_expr) g pp_expr s in 
+                    (pp_tele pp_expr) g pp_expr s in
                 Error (`FullnessError msg)
               else if (not (Set.is_subset pd_tgt_vars ~of_:tot_tgt_vars)) then
                 let msg = Fmt.str "@[<v>Non-full target:@,pd: @[%a@]@,tgt: @[%a@]@,"
-                    (pp_tele pp_expr) g pp_expr t in 
+                    (pp_tele pp_expr) g pp_expr t in
                 Error (`FullnessError msg)
               else Ok (tl,cn,pd,c',s',t')
 
@@ -593,7 +593,7 @@ let rec check_defs gma defs =
     let ty_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) ty_val) in
     (match syntax_tree 0 tm_val with
      | Ok s -> pr "Term syntax tree: @[%s@]@," s
-     | Error y -> pr "Could not print syntax tree: %s" y);
+     | Error y -> pr "Could not print syntax tree: %s@," y);
     pr "Type unfolded:@, @[%a@]@," pp_expr ty_unfolded_nf;
     pr "Term unfolded:@, @[%a@]@," pp_expr tm_unfolded_nf;
     check_defs (define gma id tm_val ty_val) ds
@@ -623,13 +623,13 @@ let rec check_defs gma defs =
     pr "@[<v>Cylcoh type: @[%a@]@,@]" pp_expr_with_impl cyl_cty_nf;
     pr "@[<v>Cylcoh expr: @[%a@]@,@]" pp_expr cyl_nf;
     let* _ = check gma cyl_cty_nf TypV in
-    log_msg "Type is valid ..."; 
+    log_msg "Type is valid ...";
     let* _ = check gma cyl_nf cyl_cty in
     log_msg "Rechecking succeeded!";
     check_defs (define gma id cyl_ctm cyl_cty) ds
 
 let run_tc m =
-  match m with 
+  match m with
   | Ok _ ->
     Fmt.pr "@[<v>----------------@,Success!@,@,@]"
   | Error err ->

From 1f5b8c6f4871ac0b64e8ec8d3e4500f2c31152c2 Mon Sep 17 00:00:00 2001
From: Alex Rice <alexrice999@hotmail.co.uk>
Date: Mon, 2 Aug 2021 16:17:46 +0100
Subject: [PATCH 14/14] Add partial unfolding

---
 lib/eval.ml      | 48 ++++++++++++++++++++++++++++++++++++------------
 lib/typecheck.ml | 22 +++++++++++-----------
 lib/unify.ml     |  6 +++---
 3 files changed, 50 insertions(+), 26 deletions(-)

diff --git a/lib/eval.ml b/lib/eval.ml
index 9f76f16..ee7c4cd 100644
--- a/lib/eval.ml
+++ b/lib/eval.ml
@@ -19,6 +19,30 @@ open Pd
 
 exception Eval_error of string
 
+type unfolding = {
+  level : int option;
+  ufld_comp : bool;
+  }
+
+let decrease (ufld : unfolding) : unfolding = {
+    level = Option.bind ufld.level (fun n -> Option.some (max 0 (n - 1)));
+    ufld_comp = ufld.ufld_comp;
+  }
+
+let should_unfold (ufld: unfolding) : bool = not (Option.equal (=) ufld.level (Option.some 0))
+
+let ufld_build n = {
+    level = Option.some n;
+    ufld_comp = true;
+  }
+
+let ufld_true = {
+    level = Option.none;
+    ufld_comp = true;
+  }
+
+let ufld_false = ufld_build 0
+
 let rec eval top loc tm =
   (* pr "Evaluating: %a@," pp_term tm; *)
   match tm with
@@ -113,7 +137,6 @@ and appV t u ict =
      let sp' = AppSp(sp,u,ict) in
      let x = CohV (cn,pd,c,s,t,sp') in
      (match cohReduction cn pd c s t sp' u with
-      | Error s when s = "Not applied all arguments yet" -> x
       | Error _ -> (* pr "No reduction: %a because %s\n\n" pp_value x y; *) x
       | Ok y -> y)
   | _ -> raise (Eval_error (Fmt.str "malformed application: %a" pp_value t))
@@ -232,7 +255,7 @@ and insertionCoh cn pd c s t args only_prune =
      Ok (runSpV (CohV(cn,pd_final,cv,sv,tv,EmpSp)) final_spine)
 
 and applySubstitution k v sub =
-  let t = quote true k v in
+  let t = quote ufld_true k v in
   eval Emp sub t
 
 and construct_disc_type n =
@@ -359,29 +382,30 @@ and force_meta v =
 (*                                  Quoting                                  *)
 (*****************************************************************************)
 
-and quote ufld k v =
+and quote (ufld : unfolding) k v =
+  let dec_ufld = decrease ufld in
   let qc x = quote ufld k x in
-  let qcs x s = quote_sp ufld k x s in
+  let qcs x s = quote_sp dec_ufld k x s in
   match force_meta v with
   | FlexV (m,sp) -> qcs (MetaT m) sp
   | RigidV (l,sp) -> qcs (VarT (lvl_to_idx k l)) sp
-  | TopV (_,_,tv) when ufld -> qc tv
+  | TopV (_,_,tv) when should_unfold ufld -> qc tv
   | TopV (nm,sp,_) -> qcs (TopT nm) sp
   | LamV (nm,ict,cl) -> LamT (nm, ict, quote ufld (k+1) (cl $$ varV k))
   | PiV (nm,ict,u,cl) -> PiT (nm, ict, qc u, quote ufld (k+1) (cl $$ varV k))
   | ObjV c -> ObjT (qc c)
   | HomV (c,s,t) -> HomT (qc c, qc s, qc t)
 
-  | UCompV (_,cohv,_) when ufld ->
-     quote ufld k cohv
+  | UCompV (_,cohv,_) when should_unfold ufld && ufld.ufld_comp ->
+     qc cohv
   | UCompV (uc,_,sp) -> qcs (UCompT uc) sp
 
   | CohV (cn,pd,c,s,t,sp) ->
 
     let k' = length (Pd.labels pd) + 1 in
-    let c' = quote ufld k' c in
-    let s' = quote ufld k' s in
-    let t' = quote ufld k' t in
+    let c' = quote dec_ufld k' c in
+    let s' = quote dec_ufld k' s in
+    let t' = quote dec_ufld k' t in
 
     qcs (CohT (cn,pd,c',s',t')) sp
 
@@ -407,12 +431,12 @@ let quote_tele tl =
     | Emp -> (Emp,0)
     | Ext (typs',(nm,ict,typ)) ->
       let (r,k) = go typs' in
-      let ty_tm = quote true k typ in
+      let ty_tm = quote ufld_true k typ in
       (Ext (r,(nm,ict,ty_tm)),k+1)
   in fst (go tl)
 
 let nf top loc tm =
-  quote true (length loc) (eval top loc tm)
+  quote ufld_true (length loc) (eval top loc tm)
 
 (*****************************************************************************)
 (*                               Free Variables                              *)
diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index 0a7a297..e3ee2ac 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -165,8 +165,8 @@ let rec check gma expr typ =
       pr "Unification error: %s\n" msg;
       (* I guess the unification error will have more information .... *)
       let nms = names gma in
-      let inferred_nf = term_to_expr nms (quote false gma.lvl inferred) in
-      let expected_nf = term_to_expr nms (quote true gma.lvl expected) in
+      let inferred_nf = term_to_expr nms (quote ufld_false gma.lvl inferred) in
+      let expected_nf = term_to_expr nms (quote ufld_true gma.lvl expected) in
       let msg = String.concat [ str "@[<v>The expression: @,@, @[%a@]@,@,@]" pp_expr e;
                                 str "@[<v>has type: @,@,  @[%a@]@,@,@]" pp_expr inferred_nf;
                                 str "@[<v>but was expected to have type: @,@, @[%a@]@,@]"
@@ -244,7 +244,7 @@ and infer gma expr =
   | LamE (nm,ict,e) ->
     let a = eval gma.top gma.loc (fresh_meta ()) in
     let* (e', t) = insert gma (infer (bind gma nm a) e) in
-    let cl = Closure (gma.top,gma.loc,quote false (gma.lvl + 1) t) in
+    let cl = Closure (gma.top,gma.loc,quote ufld_false (gma.lvl + 1) t) in
     Ok (LamT (nm,ict,e') , PiV (nm,ict,a,cl))
 
   | AppE (u,v,ict) ->
@@ -585,12 +585,12 @@ let rec check_defs gma defs =
     let* tm_tm = check gma abs_tm ty_val in
     let tm_val = eval gma.top gma.loc tm_tm in
     pr "Checking complete for %s@," id;
-    let tm_nf = term_to_expr Emp (quote false (gma.lvl) tm_val) in
-    let ty_nf = term_to_expr Emp (quote false (gma.lvl) ty_val) in
+    let tm_nf = term_to_expr Emp (quote ufld_false (gma.lvl) tm_val) in
+    let ty_nf = term_to_expr Emp (quote ufld_false (gma.lvl) ty_val) in
     pr "Type: @[%a@]@," pp_expr ty_nf;
     pr "Term: @[%a@]@," pp_expr tm_nf;
-    let tm_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) tm_val) in
-    let ty_unfolded_nf = term_to_expr Emp (quote true (gma.lvl) ty_val) in
+    let tm_unfolded_nf = term_to_expr Emp (quote (ufld_build 1) (gma.lvl) tm_val) in
+    let ty_unfolded_nf = term_to_expr Emp (quote (ufld_build 1) (gma.lvl) ty_val) in
     (match syntax_tree 0 tm_val with
      | Ok s -> pr "Term syntax tree: @[%s@]@," s
      | Error y -> pr "Could not print syntax tree: %s@," y);
@@ -604,8 +604,8 @@ let rec check_defs gma defs =
     let coh_ty = eval gma.top gma.loc
         (tele_to_pi tl (ObjT (HomT (ct,st,tt)))) in
     let coh_tm = eval gma.top gma.loc (CohT (cn,pd,ct,st,tt)) in
-    let coh_ty_nf = term_to_expr Emp (quote false gma.lvl coh_ty) in
-    let coh_tm_nf = term_to_expr Emp (quote false gma.lvl coh_tm) in
+    let coh_ty_nf = term_to_expr Emp (quote ufld_false gma.lvl coh_ty) in
+    let coh_tm_nf = term_to_expr Emp (quote ufld_false gma.lvl coh_tm) in
     pr "@[<v>Coh type: @[%a@]@,@]" pp_expr coh_ty_nf;
     (* pr "@[<v>Coh term: @[%a@]@,@]" pp_term (CohT (cn,pd,ct,st,tt)); *)
     pr "@[<v>Coh expr: @[%a@]@,@]" pp_expr coh_tm_nf;
@@ -618,8 +618,8 @@ let rec check_defs gma defs =
     let cyl_ctm = eval gma.top gma.loc
         (CylCohT (cn,pd,ct,(ssph,s),(tsph,t))) in
     let cyl_cty = eval gma.top gma.loc cctt in
-    let cyl_cty_nf = term_to_expr Emp (quote false gma.lvl cyl_cty) in
-    let cyl_nf = term_to_expr Emp (quote false gma.lvl cyl_ctm) in
+    let cyl_cty_nf = term_to_expr Emp (quote ufld_false gma.lvl cyl_cty) in
+    let cyl_nf = term_to_expr Emp (quote ufld_false gma.lvl cyl_ctm) in
     pr "@[<v>Cylcoh type: @[%a@]@,@]" pp_expr_with_impl cyl_cty_nf;
     pr "@[<v>Cylcoh expr: @[%a@]@,@]" pp_expr cyl_nf;
     let* _ = check gma cyl_cty_nf TypV in
diff --git a/lib/unify.ml b/lib/unify.ml
index d66d05c..2df1464 100644
--- a/lib/unify.ml
+++ b/lib/unify.ml
@@ -84,9 +84,9 @@ let rename m pren v =
     | CohV (cn,pd,c,s,t,sp) ->
 
       let k' = Suite.length (Pd.labels pd) + 1 in
-      let c' = quote true k' c in
-      let s' = quote true k' s in
-      let t' = quote true k' t in
+      let c' = quote ufld_true k' c in
+      let s' = quote ufld_true k' s in
+      let t' = quote ufld_true k' t in
 
       goSp pr (CohT (cn,pd,c',s',t')) sp