Elaboration.

src/debug.cccatt

@@ -1,4 +1,4 @@
-coh I (a : .) : a → a
+# coh I (a : .) : a → a
 
 coh ap (a b : .) (t : a → b) (u : a) : b
 

src/lang.ml

@@ -39,7 +39,7 @@ let rec to_string e =
   | App (t, u) -> Printf.sprintf "%s %s" (to_string t) (to_string u)
   | Pi (x, a, t) -> Printf.sprintf "(%s : %s) => %s" x (to_string a) (to_string t)
   | Obj -> "."
-  | Hom (a, b) -> Printf.sprintf "(%s -> %s)" (to_string a) (to_string b)
+  | Hom (a, b) -> Printf.sprintf "(%s → %s)" (to_string a) (to_string b)
   | Prod (a, b) -> Printf.sprintf "(%s × %s)" (to_string a) (to_string b)
   | Id (a, t, u) ->
     let a =

src/test.cccatt

@@ -61,9 +61,9 @@ let id (a : .) (x : a) := ap a a (I a) x
 
 ## Testing holes
 
-# let id' (a : .) (x : a) := ap _ _ (I _) x
+let id' (a : .) (x : a) := ap _ _ (I _) x
 
-# let ap' (a b : .) (x : a) (f : a -> b) := ap _ _ f x
+let ap' (a b : .) (x : a) (f : a -> b) := ap _ _ f x
 
 ## Testing identities
 

src/value.ml

@@ -128,8 +128,10 @@ let rec unify k t t' =
   | Type, Type -> ()
   | Meta { value = Some t; _ }, t' -> unify k t t'
   | t, Meta { value = Some t'; _ } -> unify k t t'
+  | Meta m, Meta m' when m == m' -> ()
   | Meta m, t
   | t, Meta m ->
+    assert (not (List.memq m (metavariables t)));
     (* printf "... ?%d becomes %s\n" m.id (to_string t); *)
     m.value <- Some t
   | _ -> raise Unification