(REF) Tweak attribute names in preparation for new logical introduction rule behavior

3 files changed, 21 insertions, 21 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 66c64f6..619ed84 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -12,7 +12,7 @@ definition homotopy_i (infix "~" 100)
 
 translations "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
 
-Lemma homotopy_type [typechk]:
+Lemma homotopy_type [type]:
   assumes
     "A: U i"
     "\<And>x. x: A \<Longrightarrow> B x: U i"
@@ -161,7 +161,7 @@ subsection \<open>Quasi-inverses\<close>
 definition "is_qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
   homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)"
 
-lemma is_qinv_type [typechk]:
+lemma is_qinv_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "is_qinv A B f: U i"
   unfolding is_qinv_def
@@ -193,12 +193,12 @@ Lemma is_qinvI:
     show "g \<circ> f ~ id A \<and> f \<circ> g ~ id B" by (intro; fact)
   qed
 
-Lemma is_qinv_components [typechk]:
+Lemma is_qinv_components [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f"
   shows
-    fst_of_is_qinv: "fst pf: B \<rightarrow> A" and
-    p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and
-    p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B"
+    qinv_of_is_qinv: "fst pf: B \<rightarrow> A" and
+    ret_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and
+    sec_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B"
   using assms unfolding is_qinv_def
   by typechk+
 
@@ -211,8 +211,8 @@ using [[debug_typechk]]
   back \<comment> \<open>Typechecking/inference goes too far here. Problem would likely be
     solved with definitional unfolding\<close>
   \<^item> by (fact \<open>f:_\<close>)
-  \<^item> by (rule p\<^sub>2\<^sub>2_of_is_qinv)
-  \<^item> by (rule p\<^sub>2\<^sub>1_of_is_qinv)
+  \<^item> by (rule sec_of_is_qinv)
+  \<^item> by (rule ret_of_is_qinv)
   done
 
 Lemma (def) funcomp_is_qinv:
@@ -251,7 +251,7 @@ definition "is_biinv A B f \<equiv>
   (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
     \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"
 
-lemma is_biinv_type [typechk]:
+lemma is_biinv_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "is_biinv A B f: U i"
   unfolding is_biinv_def by typechk
@@ -273,13 +273,13 @@ Lemma is_biinvI:
     show "<h, H2>: {}" by typechk
   qed
 
-Lemma is_biinv_components [typechk]:
+Lemma is_biinv_components [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_biinv f"
   shows
-    p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
-    p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
-    p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
-    p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B"
+    section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
+    retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
+    ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
+    sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B"
   using assms unfolding is_biinv_def
   by typechk+
 
@@ -350,7 +350,7 @@ text \<open>
 definition equivalence (infix "\<simeq>" 110)
   where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f"
 
-lemma equivalence_type [typechk]:
+lemma equivalence_type [type]:
   assumes "A: U i" "B: U i"
   shows "A \<simeq> B: U i"
   unfolding equivalence_def by typechk
@@ -376,7 +376,7 @@ Lemma (def) equivalence_symmetric:
   apply elim
   apply (dest (4) is_biinv_imp_is_qinv)
   apply intro
-    \<^item> by (rule fst_of_is_qinv) facts
+    \<^item> by (rule qinv_of_is_qinv) facts
     \<^item> by (rule is_qinv_imp_is_biinv) (rule qinv_is_qinv)
   done
 
diff --git a/hott/Identity.thy b/hott/Identity.thy
index d6efbf8..b9ebafb 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -41,7 +41,7 @@ axiomatization where
 
 lemmas
   [form] = IdF and
-  [intro, intros] = IdI and
+  [intr, intro] = IdI and
   [elim ?p ?a ?b] = IdE and
   [comp] = Id_comp and
   [refl] = IdI
@@ -567,7 +567,7 @@ interpretation \<Omega>2:
 notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121)
 notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121)
 
-Lemma [typechk]:
+Lemma [type]:
   assumes "\<alpha>: \<Omega>2 A a" and "\<beta>: \<Omega>2 A a"
   shows horiz_pathcomp_type: "\<alpha> \<star> \<beta>: \<Omega>2 A a"
     and horiz_pathcomp'_type: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
diff --git a/hott/Nat.thy b/hott/Nat.thy
index fd567f3..716703a 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -39,7 +39,7 @@ where
 
 lemmas
   [form] = NatF and
-  [intro, intros] = Nat_zero Nat_suc and
+  [intr, intro] = Nat_zero Nat_suc and
   [elim "?n"] = NatE and
   [comp] = Nat_comp_zero Nat_comp_suc
 
@@ -62,7 +62,7 @@ subsection \<open>Addition\<close>
 
 definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat m (K suc) n"
 
-lemma add_type [typechk]:
+lemma add_type [type]:
   assumes "m: Nat" "n: Nat"
   shows "m + n: Nat"
   unfolding add_def by typechk
@@ -123,7 +123,7 @@ subsection \<open>Multiplication\<close>
 
 definition mul (infixl "*" 121) where "m * n \<equiv> NatRec Nat 0 (K $ add m) n"
 
-lemma mul_type [typechk]:
+lemma mul_type [type]:
   assumes "m: Nat" "n: Nat"
   shows "m * n: Nat"
   unfolding mul_def by typechk