Swapped notation for metas (now ?) and holes (now {}), other notation and name changes.

10 files changed, 143 insertions, 140 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 99300a0..379dc81 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -8,7 +8,7 @@ section \<open>Homotopy\<close>
 definition "homotopy A B f g \<equiv> \<Prod>x: A. f `x =\<^bsub>B x\<^esub> g `x"
 
 definition homotopy_i (infix "~" 100)
-  where [implicit]: "f ~ g \<equiv> homotopy ? ? f g"
+  where [implicit]: "f ~ g \<equiv> homotopy {} {} f g"
 
 translations "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
 
@@ -79,7 +79,7 @@ Lemma (def) htrans:
 
 section \<open>Rewriting homotopies\<close>
 
-congruence "f ~ g" rhs g
+calc "f ~ g" rhs g
 
 lemmas
   homotopy_sym [sym] = hsym[rotated 4] and
@@ -129,7 +129,6 @@ Lemma funcomp_right_htpy:
 method lhtpy = rule funcomp_left_htpy[rotated 6]
 method rhtpy = rule funcomp_right_htpy[rotated 6]
 
-
 Lemma (def) commute_homotopy:
   assumes
     "A: U i" "B: U i"
@@ -152,8 +151,16 @@ Corollary (def) commute_homotopy':
     "H: f ~ (id A)"
   shows "H (f x) = f [H x]"
   proof -
-    (*FIXME: Bug; if the following type declaration isn't made then bad things
-      happen on the next lines.*)
+    (* Rewrite the below proof
+    have *: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
+      using \<open>H:_\<close> unfolding homotopy_def by (rule commute_homotopy)
+
+    thus "H (f x) = f[H x]"
+      apply (pathcomp_cancelr)
+      ...
+    *)
+    (*FUTURE: Because we don't have very good normalization integrated into
+      things yet, we need to manually unfold the type of H.*)
     from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
       by (reduce add: homotopy_def)
 
@@ -161,7 +168,7 @@ Corollary (def) commute_homotopy':
       by (rule left_whisker, transport eq: ap_id, refl)
     also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
       by (rule commute_homotopy)
-    finally have "{}" by this
+    finally have "?" by this
 
     thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+)
   qed
@@ -181,7 +188,7 @@ Lemma is_qinv_type [type]:
   by typechk
 
 definition is_qinv_i ("is'_qinv")
-  where [implicit]: "is_qinv f \<equiv> Equivalence.is_qinv ? ? f"
+  where [implicit]: "is_qinv f \<equiv> Equivalence.is_qinv {} {} f"
 
 no_translations "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f"
 
@@ -241,7 +248,7 @@ Lemma (def) funcomp_is_qinv:
           have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl
           also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact
           also have ".. ~ id A" by reduce fact
-          finally show "{}" by this
+          finally show "?" by this
         qed
 
         show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C"
@@ -249,7 +256,7 @@ Lemma (def) funcomp_is_qinv:
           have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl
           also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact
           also have ".. ~ id C" by reduce fact
-          finally show "{}" by this
+          finally show "?" by this
         qed
       qed
     done
@@ -267,7 +274,7 @@ Lemma is_biinv_type [type]:
   unfolding is_biinv_def by typechk
 
 definition is_biinv_i ("is'_biinv")
-  where [implicit]: "is_biinv f \<equiv> Equivalence.is_biinv ? ? f"
+  where [implicit]: "is_biinv f \<equiv> Equivalence.is_biinv {} {} f"
 
 translations "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f"
 
@@ -279,8 +286,8 @@ Lemma is_biinvI:
   shows "is_biinv f"
   unfolding is_biinv_def
   proof intro
-    show "<g, H1>: {}" by typechk
-    show "<h, H2>: {}" by typechk
+    show "<g, H1>: \<Sum>g: B \<rightarrow> A. g \<circ> f ~ id A" by typechk
+    show "<h, H2>: \<Sum>g: B \<rightarrow> A. f \<circ> g ~ id B" by typechk
   qed
 
 Lemma is_biinv_components [type]:
@@ -408,7 +415,7 @@ text \<open>
 Lemma (def) equiv_if_equal:
   assumes
     "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
-  shows "<trans (id (U i)) p, ?isequiv>: A \<simeq> B"
+  shows "<transp (id (U i)) p, ?isequiv>: A \<simeq> B"
   unfolding equivalence_def
   apply intro defer
     \<^item> apply (eq p)
@@ -422,7 +429,7 @@ Lemma (def) equiv_if_equal:
         using [[solve_side_conds=1]]
         apply (rewrite transport_comp)
           \<circ> by (rule Ui_in_USi)
-          \<circ> by reduce (rule in_USi_if_in_Ui)
+          \<circ> by reduce (rule U_lift)
           \<circ> by reduce (rule id_is_biinv)
         done
       done
diff --git a/hott/Identity.thy b/hott/Identity.thy
index dc27ee8..0a31dc7 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -20,7 +20,7 @@ syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
 translations "a =\<^bsub>A\<^esub> b" \<rightleftharpoons> "CONST Id A a b"
 
 axiomatization where
-  \<comment> \<open>Here `A: U i` comes last because A is often implicit\<close>
+  \<comment> \<open>Here \<open>A: U i\<close> comes last because A is often implicit\<close>
   IdF: "\<lbrakk>a: A; b: A; A: U i\<rbrakk> \<Longrightarrow> a =\<^bsub>A\<^esub> b: U i" and
 
   IdI: "a: A \<Longrightarrow> refl a: a =\<^bsub>A\<^esub> a" and
@@ -49,8 +49,8 @@ lemmas
 
 section \<open>Path induction\<close>
 
-\<comment> \<open>With `p: x = y` in the context the invokation `eq p` is essentially
-  `elim p x y`, with some extra bits before and after.\<close>
+\<comment> \<open>With \<open>p: x = y\<close> in the context the invokation \<open>eq p\<close> is essentially
+  \<open>elim p x y\<close>, with some extra bits before and after.\<close>
 
 method_setup eq =
   \<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
@@ -109,13 +109,13 @@ method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q]
 section \<open>Notation\<close>
 
 definition Id_i (infix "=" 110)
-  where [implicit]: "Id_i x y \<equiv> x =\<^bsub>?\<^esub> y"
+  where [implicit]: "Id_i x y \<equiv> x =\<^bsub>{}\<^esub> y"
 
 definition pathinv_i ("_\<inverse>" [1000])
-  where [implicit]: "pathinv_i p \<equiv> pathinv ? ? ? p"
+  where [implicit]: "pathinv_i p \<equiv> pathinv {} {} {} p"
 
 definition pathcomp_i (infixl "\<bullet>" 121)
-  where [implicit]: "pathcomp_i p q \<equiv> pathcomp ? ? ? ? p q"
+  where [implicit]: "pathcomp_i p q \<equiv> pathcomp {} {} {} {} p q"
 
 translations
   "x = y" \<leftharpoondown> "x =\<^bsub>A\<^esub> y"
@@ -125,7 +125,7 @@ translations
 
 section \<open>Calculational reasoning\<close>
 
-congruence "x = y" rhs y
+calc "x = y" rhs y
 
 lemmas
   [sym] = pathinv[rotated 3] and
@@ -144,8 +144,8 @@ Lemma (def) pathcomp_refl:
   shows "p \<bullet> (refl y) = p"
   by (eq p) (reduce, refl)
 
-definition [implicit]: "lu p \<equiv> refl_pathcomp ? ? ? p"
-definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p"
+definition [implicit]: "lu p \<equiv> refl_pathcomp {} {} {} p"
+definition [implicit]: "ru p \<equiv> pathcomp_refl {} {} {} p"
 
 translations
   "CONST lu p" \<leftharpoondown> "CONST refl_pathcomp A x y p"
@@ -204,7 +204,7 @@ Lemma (def) ap:
   by (eq p) intro
 
 definition ap_i ("_[_]" [1000, 0])
-  where [implicit]: "ap_i f p \<equiv> ap ? ? ? ? f p"
+  where [implicit]: "ap_i f p \<equiv> ap {} {} {} {} f p"
 
 translations "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
 
@@ -265,17 +265,17 @@ Lemma (def) transport:
   shows "P x \<rightarrow> P y"
   by (eq p) intro
 
-definition transport_i ("trans")
-  where [implicit]: "trans P p \<equiv> transport ? P ? ? p"
+definition transport_i ("transp")
+  where [implicit]: "transp P p \<equiv> transport {} P {} {} p"
 
-translations "trans P p" \<leftharpoondown> "CONST transport A P x y p"
+translations "transp P p" \<leftharpoondown> "CONST transport A P x y p"
 
 Lemma transport_comp [comp]:
   assumes
     "a: A"
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> P x: U i"
-  shows "trans P (refl a) \<equiv> id (P a)"
+  shows "transp P (refl a) \<equiv> id (P a)"
   unfolding transport_def by reduce
 
 Lemma apply_transport:
@@ -284,7 +284,7 @@ Lemma apply_transport:
     "x: A" "y: A"
     "p: y =\<^bsub>A\<^esub> x"
     "u: P x"
-  shows "trans P p\<inverse> u: P y"
+  shows "transp P p\<inverse> u: P y"
   by typechk
 
 method transport uses eq = (rule apply_transport[OF _ _ _ _ eq])
@@ -304,7 +304,7 @@ Lemma (def) pathcomp_cancel_left:
       by (transport eq: pathcomp_assoc,
           transport eq: inv_pathcomp,
           transport eq: refl_pathcomp) refl
-    finally show "{}" by this
+    finally show "?" by this
   qed
 
 Lemma (def) pathcomp_cancel_right:
@@ -323,7 +323,7 @@ Lemma (def) pathcomp_cancel_right:
           transport eq: pathcomp_assoc[symmetric],
           transport eq: pathcomp_inv,
           transport eq: pathcomp_refl) refl
-    finally show "{}" by this
+    finally show "?" by this
   qed
 
 method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7]
@@ -335,7 +335,7 @@ Lemma (def) transport_left_inv:
     "\<And>x. x: A \<Longrightarrow> P x: U i"
     "x: A" "y: A"
     "p: x = y"
-  shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)"
+  shows "(transp P p\<inverse>) \<circ> (transp P p) = id (P x)"
   by (eq p) (reduce, refl)
 
 Lemma (def) transport_right_inv:
@@ -344,7 +344,7 @@ Lemma (def) transport_right_inv:
     "\<And>x. x: A \<Longrightarrow> P x: U i"
     "x: A" "y: A"
     "p: x = y"
-  shows "(trans P p) \<circ> (trans P p\<inverse>) = id (P y)"
+  shows "(transp P p) \<circ> (transp P p\<inverse>) = id (P y)"
   by (eq p) (reduce, refl)
 
 Lemma (def) transport_pathcomp:
@@ -354,11 +354,11 @@ Lemma (def) transport_pathcomp:
     "x: A" "y: A" "z: A"
     "u: P x"
     "p: x = y" "q: y = z"
-  shows "trans P q (trans P p u) = trans P (p \<bullet> q) u"
+  shows "transp P q (transp P p u) = transp P (p \<bullet> q) u"
 proof (eq p)
   fix x q u
   assuming "x: A" "q: x = z" "u: P x"
-  show "trans P q (trans P (refl x) u) = trans P ((refl x) \<bullet> q) u"
+  show "transp P q (transp P (refl x) u) = transp P ((refl x) \<bullet> q) u"
     by (eq q) (reduce, refl)
 qed
 
@@ -370,7 +370,7 @@ Lemma (def) transport_compose_typefam:
     "x: A" "y: A"
     "p: x = y"
     "u: P (f x)"
-  shows "trans (fn x. P (f x)) p u = trans P f[p] u"
+  shows "transp (fn x. P (f x)) p u = transp P f[p] u"
   by (eq p) (reduce, refl)
 
 Lemma (def) transport_function_family:
@@ -382,7 +382,7 @@ Lemma (def) transport_function_family:
     "x: A" "y: A"
     "u: P x"
     "p: x = y"
-  shows "trans Q p ((f x) u) = (f y) (trans P p u)"
+  shows "transp Q p ((f x) u) = (f y) (transp P p u)"
   by (eq p) (reduce, refl)
 
 Lemma (def) transport_const:
@@ -390,19 +390,19 @@ Lemma (def) transport_const:
     "A: U i" "B: U i"
     "x: A" "y: A"
     "p: x = y"
-  shows "\<Prod>b: B. trans (fn _. B) p b = b"
+  shows "\<Prod>b: B. transp (fn _. B) p b = b"
   by intro (eq p, reduce, refl)
 
-definition transport_const_i ("trans'_const")
-  where [implicit]: "trans_const B p \<equiv> transport_const ? B ? ? p"
+definition transport_const_i ("transp'_c")
+  where [implicit]: "transp_c B p \<equiv> transport_const {} B {} {} p"
 
-translations "trans_const B p" \<leftharpoondown> "CONST transport_const A B x y p"
+translations "transp_c B p" \<leftharpoondown> "CONST transport_const A B x y p"
 
 Lemma transport_const_comp [comp]:
   assumes
     "x: A" "b: B"
     "A: U i" "B: U i"
-  shows "trans_const B (refl x) b \<equiv> refl b"
+  shows "transp_c B (refl x) b \<equiv> refl b"
   unfolding transport_const_def by reduce
 
 Lemma (def) pathlift:
@@ -412,11 +412,11 @@ Lemma (def) pathlift:
     "x: A" "y: A"
     "p: x = y"
     "u: P x"
-  shows "<x, u> = <y, trans P p u>"
+  shows "<x, u> = <y, transp P p u>"
   by (eq p) (reduce, refl)
 
 definition pathlift_i ("lift")
-  where [implicit]: "lift P p u \<equiv> pathlift ? P ? ? p u"
+  where [implicit]: "lift P p u \<equiv> pathlift {} P {} {} p u"
 
 translations "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u"
 
@@ -449,11 +449,11 @@ Lemma (def) apd:
     "f: \<Prod>x: A. P x"
     "x: A" "y: A"
     "p: x = y"
-  shows "trans P p (f x) = f y"
+  shows "transp P p (f x) = f y"
   by (eq p) (reduce, refl)
 
 definition apd_i ("apd")
-  where [implicit]: "apd f p \<equiv> Identity.apd ? ? f ? ? p"
+  where [implicit]: "apd f p \<equiv> Identity.apd {} {} f {} {} p"
 
 translations "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p"
 
@@ -472,7 +472,7 @@ Lemma (def) apd_ap:
     "f: A \<rightarrow> B"
     "x: A" "y: A"
     "p: x = y"
-  shows "apd f p = trans_const B p (f x) \<bullet> f[p]"
+  shows "apd f p = transp_c B p (f x) \<bullet> f[p]"
   by (eq p) (reduce, refl)
 
 
@@ -488,7 +488,7 @@ Lemma (def) right_whisker:
       have "s \<bullet> refl x = s" by (rule pathcomp_refl)
       also have ".. = t" by fact
       also have ".. = t \<bullet> refl x" by (rule pathcomp_refl[symmetric])
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -502,15 +502,15 @@ Lemma (def) left_whisker:
       have "refl x \<bullet> s = s" by (rule refl_pathcomp)
       also have ".. = t" by fact
       also have ".. = refl x \<bullet> t" by (rule refl_pathcomp[symmetric])
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
 definition right_whisker_i (infix "\<bullet>\<^sub>r" 121)
-  where [implicit]: "\<alpha> \<bullet>\<^sub>r r \<equiv> right_whisker ? ? ? ? ? ? r \<alpha>"
+  where [implicit]: "\<alpha> \<bullet>\<^sub>r r \<equiv> right_whisker {} {} {} {} {} {} r \<alpha>"
 
 definition left_whisker_i (infix "\<bullet>\<^sub>l" 121)
-  where [implicit]: "r \<bullet>\<^sub>l \<alpha> \<equiv> left_whisker ? ? ? ? ? ? r \<alpha>"
+  where [implicit]: "r \<bullet>\<^sub>l \<alpha> \<equiv> left_whisker {} {} {} {} {} {} r \<alpha>"
 
 translations
   "\<alpha> \<bullet>\<^sub>r r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>"
@@ -532,8 +532,8 @@ method right_whisker = (rule right_whisker)
 
 section \<open>Horizontal path-composition\<close>
 
-text \<open>Conditions under which horizontal path-composition is defined.\<close>
 locale horiz_pathcomposable =
+\<comment> \<open>Conditions under which horizontal path-composition is defined.\<close>
 fixes
   i A a b c p q r s
 assumes [type]:
@@ -615,17 +615,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp:
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>"
       by (rule pathcomp_refl)
     also have ".. = \<alpha>" by (rule refl_pathcomp)
-    finally have eq\<alpha>: "{} = \<alpha>" by this
+    finally have eq\<alpha>: "? = \<alpha>" by this
 
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
       by (rule pathcomp_refl)
     also have ".. = \<beta>" by (rule refl_pathcomp)
-    finally have eq\<beta>: "{} = \<beta>" by this
+    finally have eq\<beta>: "? = \<beta>" by this
 
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))
-      = \<alpha> \<bullet> {}" by right_whisker (fact eq\<alpha>)
+      = \<alpha> \<bullet> ?" by right_whisker (fact eq\<alpha>)
     also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (fact eq\<beta>)
-    finally show "{} = \<alpha> \<bullet> \<beta>" by this
+    finally show "? = \<alpha> \<bullet> \<beta>" by this
   qed
 
 Lemma (def) pathcomp_eq_horiz_pathcomp':
@@ -637,17 +637,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
       by (rule pathcomp_refl)
     also have ".. = \<beta>" by (rule refl_pathcomp)
-    finally have eq\<beta>: "{} = \<beta>" by this
+    finally have eq\<beta>: "? = \<beta>" by this
 
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>"
       by (rule pathcomp_refl)
     also have ".. = \<alpha>" by (rule refl_pathcomp)
-    finally have eq\<alpha>: "{} = \<alpha>" by this
+    finally have eq\<alpha>: "? = \<alpha>" by this
 
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))
-      = \<beta> \<bullet> {}" by right_whisker (fact eq\<beta>)
+      = \<beta> \<bullet> ?" by right_whisker (fact eq\<beta>)
     also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (fact eq\<alpha>)
-    finally show "{} = \<beta> \<bullet> \<alpha>" by this
+    finally show "? = \<beta> \<bullet> \<alpha>" by this
   qed
 
 Lemma (def) eckmann_hilton:
diff --git a/hott/List+.thy b/hott/List_HoTT.thy
index 869d667..9bd1517 100644
--- a/hott/List+.thy
+++ b/hott/List_HoTT.thy
@@ -1,4 +1,4 @@
-theory "List+"
+theory List_HoTT
 imports
   Spartan.List
   Nat
@@ -7,7 +7,7 @@ begin
 
 section \<open>Length\<close>
 
-definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)"
+definition [implicit]: "len \<equiv> ListRec {} Nat 0 (fn _ _ rec. suc rec)"
 
 experiment begin
   Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)
diff --git a/hott/Nat.thy b/hott/Nat.thy
index f45387c..1aa7932 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -115,7 +115,7 @@ Lemma (def) add_comm:
       proof reduce
         have "suc (m + n) = suc (n + m)" by (eq ih) refl
         also have ".. = suc n + m" by (transport eq: suc_add) refl
-        finally show "{}" by this
+        finally show "?" by this
       qed
   done
 
@@ -152,7 +152,7 @@ Lemma (def) zero_mul:
     proof reduce
       have "0 + 0 * n = 0 + 0 " by (eq ih) refl
       also have ".. = 0" by reduce refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -163,9 +163,9 @@ Lemma (def) suc_mul:
   \<^item> by reduce refl
   \<^item> vars n ih
     proof (reduce, transport eq: \<open>ih:_\<close>)
-      have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add)
+      have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add)
       also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -180,7 +180,7 @@ Lemma (def) mul_dist_add:
       also have ".. = l + l * m + l * n" by (rule add_assoc)
       also have ".. = l * m + l + l * n" by (transport eq: add_comm) refl
       also have ".. = l * m + (l + l * n)" by (transport eq: add_assoc) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -193,7 +193,7 @@ Lemma (def) mul_assoc:
     proof reduce
       have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add)
       also have ".. = l * m + l * m * n" by (transport eq: \<open>ih:_\<close>) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
@@ -207,7 +207,7 @@ Lemma (def) mul_comm:
       have "suc n * m = n * m + m" by (rule suc_mul)
       also have ".. = m + m * n"
         by (transport eq: \<open>ih:_\<close>, transport eq: add_comm) refl
-      finally show "{}" by this
+      finally show "?" by this
     qed
   done
 
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 6b2ed58..ffe3778 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -9,23 +9,18 @@ keywords
   "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
   "assuming" :: prf_asm % "proof" and
   "focus" "\<^item>" "\<^enum>" "\<circ>" "\<diamondop>" "~" :: prf_script_goal % "proof" and
-  "congruence" "print_coercions" :: thy_decl and
+  "calc" "print_coercions" :: thy_decl and
   "rhs" "def" "vars" :: quasi_command
 
 begin
 
-
-section \<open>Prelude\<close>
-
-paragraph \<open>Set up the meta-logic just so.\<close>
-
-paragraph \<open>Notation.\<close>
+section \<open>Notation\<close>
 
 declare [[eta_contract=false]]
 
 text \<open>
-  Rebind notation for meta-lambdas since we want to use `\<lambda>` for the object
-  lambdas. Meta-functions now use the binder `fn`.
+Rebind notation for meta-lambdas since we want to use \<open>\<lambda>\<close> for the object
+lambdas. Metafunctions now use the binder \<open>fn\<close>.
 \<close>
 setup \<open>
 let
@@ -41,34 +36,31 @@ in
 end
 \<close>
 
-syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
+syntax "_app" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
 translations "a $ b" \<rightharpoonup> "a (b)"
 
 abbreviation (input) K where "K x \<equiv> fn _. x"
 
-paragraph \<open>
-  Deeply embed dependent type theory: meta-type of expressions, and typing
-  judgment.
+
+section \<open>Metalogic\<close>
+
+text \<open>
+HOAS embedding of dependent type theory: metatype of expressions, and typing
+judgment.
 \<close>
 
 typedecl o
 
 consts has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
 
-text \<open>Type annotations for type-checking and inference.\<close>
-
-definition anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_ : _')")
-  where "(a : A) \<equiv> a" if "a: A"
-
-lemma anno: "a: A \<Longrightarrow> (a : A): A"
-  by (unfold anno_def)
-
 
 section \<open>Axioms\<close>
 
 subsection \<open>Universes\<close>
 
-typedecl lvl \<comment> \<open>Universe levels\<close>
+text \<open>\<omega>-many cumulative Russell universes.\<close>
+
+typedecl lvl
 
 axiomatization
   O  :: \<open>lvl\<close> and
@@ -81,16 +73,15 @@ axiomatization
 
 axiomatization U :: \<open>lvl \<Rightarrow> o\<close> where
   Ui_in_Uj: "i < j \<Longrightarrow> U i: U j" and
-  in_Uj_if_in_Ui: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j"
+  U_cumul: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j"
 
 lemma Ui_in_USi:
   "U i: U (S i)"
   by (rule Ui_in_Uj, rule lt_S)
 
-lemma in_USi_if_in_Ui:
+lemma U_lift:
   "A: U i \<Longrightarrow> A: U (S i)"
-  by (erule in_Uj_if_in_Ui, rule lt_S)
-
+  by (erule U_cumul, rule lt_S)
 
 subsection \<open>\<Prod>-type\<close>
 
@@ -134,7 +125,6 @@ axiomatization where
 
   lam_cong: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x"
 
-
 subsection \<open>\<Sum>-type\<close>
 
 axiomatization
@@ -207,7 +197,7 @@ lemma sub:
   shows "a: A'"
   using assms by simp
 
-\<comment> \<open>Basic substitution of definitional equalities\<close>
+\<comment> \<open>Basic rewriting of computational equality\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
@@ -305,7 +295,7 @@ method_setup this =
 
 subsection \<open>Rewriting\<close>
 
-consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
+consts rewrite_hole :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
@@ -331,28 +321,28 @@ lemma imp_cong_eq:
 ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
 ML_file \<open>rewrite.ML\<close>
 
-\<comment> \<open>\<open>reduce\<close> computes terms via judgmental equalities\<close>
+\<comment> \<open>\<open>reduce\<close> simplifies terms via computational equalities\<close>
 method reduce uses add =
   changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
 
 
-subsection \<open>Congruence relations\<close>
+subsection \<open>Calculational reasoning\<close>
 
 consts "rhs" :: \<open>'a\<close> ("..")
 
-ML_file \<open>congruence.ML\<close>
+ML_file \<open>calc.ML\<close>
 
 
 section \<open>Implicits\<close>
 
 text \<open>
-  \<open>?\<close> is used to mark implicit arguments in definitions, while \<open>{}\<close> is expanded
+  \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
   immediately for elaboration in statements.
 \<close>
 
 consts
-  iarg :: \<open>'a\<close> ("?")
-  hole :: \<open>'b\<close> ("{}")
+  iarg :: \<open>'a\<close> ("{}")
+  hole :: \<open>'b\<close> ("?")
 
 ML_file \<open>implicits.ML\<close>
 
@@ -363,11 +353,12 @@ ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes
 text \<open>Automatically insert inhabitation judgments where needed:\<close>
 
 syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "inhabited A" \<rightharpoonup> "CONST has_type {} A"
+translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
+
 
-text \<open>Implicit lambdas\<close>
+subsection \<open>Implicit lambdas\<close>
 
-definition lam_i where [implicit]: "lam_i f \<equiv> lam ? f"
+definition lam_i where [implicit]: "lam_i f \<equiv> lam {} f"
 
 syntax
   "_lam_i"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_./ _)" 30)
@@ -410,7 +401,7 @@ Lemma refine_codomain:
 Lemma lift_universe_codomain:
   assumes "A: U i" "f: A \<rightarrow> U j"
   shows "f: A \<rightarrow> U (S j)"
-  using in_USi_if_in_Ui[of "f {}"]
+  using U_lift
   by (rule refine_codomain)
 
 subsection \<open>Function composition\<close>
@@ -460,10 +451,10 @@ Lemma funcomp_apply_comp [comp]:
   shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
   unfolding funcomp_def by reduce
 
-text \<open>Notation:\<close>
+subsection \<open>Notation\<close>
 
 definition funcomp_i (infixr "\<circ>" 120)
-  where [implicit]: "funcomp_i g f \<equiv> g \<circ>\<^bsub>?\<^esub> f"
+  where [implicit]: "funcomp_i g f \<equiv> g \<circ>\<^bsub>{}\<^esub> f"
 
 translations "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
 
@@ -520,10 +511,10 @@ Lemma snd_comp [comp]:
 subsection \<open>Notation\<close>
 
 definition fst_i ("fst")
-  where [implicit]: "fst \<equiv> Spartan.fst ? ?"
+  where [implicit]: "fst \<equiv> Spartan.fst {} {}"
 
 definition snd_i ("snd")
-  where [implicit]: "snd \<equiv> Spartan.snd ? ?"
+  where [implicit]: "snd \<equiv> Spartan.snd {} {}"
 
 translations
   "fst" \<leftharpoondown> "CONST Spartan.fst A B"
@@ -550,10 +541,10 @@ method snd for p::o = rule snd[where ?p=p]
 
 text \<open>Double projections:\<close>
 
-definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.fst ? ? p)"
-definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.fst ? ? p)"
-definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.snd ? ? p)"
-definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.snd ? ? p)"
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.fst {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.fst {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.snd {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.snd {} {} p)"
 
 translations
   "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
diff --git a/spartan/core/congruence.ML b/spartan/core/calc.ML
index d9f4ffa..67dc7fc 100644
--- a/spartan/core/congruence.ML
+++ b/spartan/core/calc.ML
@@ -1,6 +1,11 @@
-structure Congruence = struct
+structure Calc = struct
 
-(* Congruence context data *)
+(* Calculational type context data
+
+A "calculational" type is a type expressing some congruence relation. In
+particular, it has a notion of composition of terms that is often used to derive
+proofs equationally.
+*)
 
 structure RHS = Generic_Data (
   type T = (term * indexname) Termtab.table
@@ -17,23 +22,23 @@ fun register_rhs t var =
     RHS.map (Termtab.update (key, (t, idxname)))
   end
 
-fun lookup_congruence ctxt t =
+fun lookup_calc ctxt t =
   Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t)
 
 
-(* Congruence declarations *)
+(* Declaration *)
 
 local val Frees_to_Vars =
   map_aterms (fn tm =>
     case tm of
-      Free (name, T) => Var (("*!"^name, 0), T) (*Hacky naming!*)
+      Free (name, T) => Var (("*!"^name, 0), T) (*FIXME: Hacky naming!*)
     | _ => tm)
 in
 
-(*Declare the "right-hand side" of types that are congruences.
-  Does not handle bound variables, so no dependent RHS in declarations!*)
-val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>congruence\<close>
-  "declare right hand side of congruence"
+(*Declare the "right-hand side" of calculational types. Does not handle bound
+  variables, so no dependent RHS in declarations!*)
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>calc\<close>
+  "declare right hand side of calculational type"
   (Parse.term -- (\<^keyword>\<open>rhs\<close> |-- Parse.term) >>
     (fn (t_str, rhs_str) => fn lthy =>
     let
@@ -47,7 +52,7 @@ val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>congruence\<close>
 end
 
 
-(* Calculational reasoning: ".." setup *)
+(* Ditto "''" setup *)
 
 fun last_rhs ctxt = map_aterms (fn t =>
   case t of
@@ -62,7 +67,7 @@ fun last_rhs ctxt = map_aterms (fn t =>
             [prop] =>
               (let
                 val typ = Lib.type_of_typing (Logic.strip_assums_concl prop)
-                val (cong_pttrn, varname) = the (lookup_congruence ctxt typ)
+                val (cong_pttrn, varname) = the (lookup_calc ctxt typ)
                 val unif_res = Pattern.unify (Context.Proof ctxt)
                   (cong_pttrn, typ) Envir.init
                 val rhs = #2 (the
@@ -70,7 +75,7 @@ fun last_rhs ctxt = map_aterms (fn t =>
               in
                 rhs
               end handle Option =>
-                error (".. can't match right-hand side of congruence"))
+                error (".. can't match right-hand side of calculational type"))
           | _ => Term.dummy)
       in rhs end
   | _ => t)
diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML
index 99c21b5..af70cfc 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/rewrite.ML
@@ -72,13 +72,13 @@ fun mk_hole i T = Var ((holeN, i), T)
 fun is_hole (Var ((name, _), _)) = (name = holeN)
   | is_hole _ = false
 
-fun is_hole_const (Const (\<^const_name>\<open>rewrite_HOLE\<close>, _)) = true
+fun is_hole_const (Const (\<^const_name>\<open>rewrite_hole\<close>, _)) = true
   | is_hole_const _ = false
 
 val hole_syntax =
   let
     (* Modified variant of Term.replace_hole *)
-    fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_HOLE\<close>, T)) i =
+    fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_hole\<close>, T)) i =
           (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
       | replace_hole Ts (Abs (x, T, t)) i =
           let val (t', i') = replace_hole (T :: Ts) t i
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 83e5149..1501221 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -64,10 +64,10 @@ Lemma list_cases [cases]:
 section \<open>Notation\<close>
 
 definition nil_i ("[]")
-  where [implicit]: "[] \<equiv> nil ?"
+  where [implicit]: "[] \<equiv> nil {}"
 
 definition cons_i (infixr "#" 120)
-  where [implicit]: "x # xs \<equiv> cons ? x xs"
+  where [implicit]: "x # xs \<equiv> cons {} x xs"
 
 translations
   "[]" \<leftharpoondown> "CONST List.nil A"
@@ -99,8 +99,8 @@ proof (cases xs)
   show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
 qed
 
-definition head_i ("head") where [implicit]: "head xs \<equiv> List.head ? xs"
-definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail ? xs"
+definition head_i ("head") where [implicit]: "head xs \<equiv> List.head {} xs"
+definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail {} xs"
 
 translations
   "head" \<leftharpoondown> "CONST List.head A"
@@ -137,7 +137,7 @@ Definition app:
       proof - show "x # rec: List A" by typechk qed
   done
 
-definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
+definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app {} xs ys"
 
 translations "app" \<leftharpoondown> "CONST List.app A"
 
@@ -153,7 +153,7 @@ proof (elim xs)
   show "f x # ys: List B" by typechk
 qed
 
-definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?"
+definition map_i ("map") where [implicit]: "map \<equiv> List.map {} {}"
 
 translations "map" \<leftharpoondown> "CONST List.map A B"
 
@@ -173,7 +173,7 @@ Definition rev:
     \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
   done
 
-definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
+definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev {}"
 
 translations "rev" \<leftharpoondown> "CONST List.rev A"
 
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index da22a4e..e06a07b 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -64,8 +64,8 @@ lemmas
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
-definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?"
-definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a"
+definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none {}"
+definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some {} a"
 
 translations
   "none" \<leftharpoondown> "CONST Maybe.none A"
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index c0abf31..0043c1e 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -139,7 +139,7 @@ lemmas
 subsection \<open>Notation\<close>
 
 definition ifelse_i ("if _ then _ else _")
-  where [implicit]: "if x then a else b \<equiv> ifelse ? x a b"
+  where [implicit]: "if x then a else b \<equiv> ifelse {} x a b"
 
 translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"