From 77aa10763429d2ded040071fbf7bee331dd52f5e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 31 Jul 2020 18:10:10 +0200 Subject: (REF) Tweak attribute names in preparation for new logical introduction rule behavior --- hott/Equivalence.thy | 32 ++++++++++++++++---------------- hott/Identity.thy | 4 ++-- hott/Nat.thy | 6 +++--- 3 files changed, 21 insertions(+), 21 deletions(-) (limited to 'hott') 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" \ "CONST homotopy A B f g" -Lemma homotopy_type [typechk]: +Lemma homotopy_type [type]: assumes "A: U i" "\x. x: A \ B x: U i" @@ -161,7 +161,7 @@ subsection \Quasi-inverses\ definition "is_qinv A B f \ \g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A) \ homotopy B (fn _. B) (f \\<^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 \ B" shows "is_qinv A B f: U i" unfolding is_qinv_def @@ -193,12 +193,12 @@ Lemma is_qinvI: show "g \ f ~ id A \ f \ 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 \ B" "pf: is_qinv f" shows - fst_of_is_qinv: "fst pf: B \ A" and - p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \ f ~ id A" and - p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \ fst pf ~ id B" + qinv_of_is_qinv: "fst pf: B \ A" and + ret_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \ f ~ id A" and + sec_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \ fst pf ~ id B" using assms unfolding is_qinv_def by typechk+ @@ -211,8 +211,8 @@ using [[debug_typechk]] back \ \Typechecking/inference goes too far here. Problem would likely be solved with definitional unfolding\ \<^item> by (fact \f:_\) - \<^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 \ (\g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A)) \ (\g: B \ A. homotopy B (fn _. B) (f \\<^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 \ B" shows "is_biinv A B f: U i" unfolding is_biinv_def by typechk @@ -273,13 +273,13 @@ Lemma is_biinvI: show ": {}" by typechk qed -Lemma is_biinv_components [typechk]: +Lemma is_biinv_components [type]: assumes "A: U i" "B: U i" "f: A \ B" "pf: is_biinv f" shows - p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \ A" and - p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \ A" and - p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \ f ~ id A" and - p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \ p\<^sub>2\<^sub>1 pf ~ id B" + section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \ A" and + retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \ A" and + ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \ f ~ id A" and + sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \ p\<^sub>2\<^sub>1 pf ~ id B" using assms unfolding is_biinv_def by typechk+ @@ -350,7 +350,7 @@ text \ definition equivalence (infix "\" 110) where "A \ B \ \f: A \ B. Equivalence.is_biinv A B f" -lemma equivalence_type [typechk]: +lemma equivalence_type [type]: assumes "A: U i" "B: U i" shows "A \ 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 \2: notation \2.horiz_pathcomp (infix "\" 121) notation \2.horiz_pathcomp' (infix "\''" 121) -Lemma [typechk]: +Lemma [type]: assumes "\: \2 A a" and "\: \2 A a" shows horiz_pathcomp_type: "\ \ \: \2 A a" and horiz_pathcomp'_type: "\ \' \: \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 \Addition\ definition add (infixl "+" 120) where "m + n \ 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 \Multiplication\ definition mul (infixl "*" 121) where "m * n \ 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 -- cgit v1.2.3