diff options
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Equivalence.thy | 24 | ||||
| -rw-r--r-- | hott/Identity.thy | 17 |
2 files changed, 22 insertions, 19 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 88adc8b..d976677 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -338,18 +338,18 @@ Lemma (derive) equivalence_symmetric: Lemma (derive) equivalence_transitive: assumes "A: U i" "B: U i" "C: U i" shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C" - (* proof intros - fix AB BC assume "AB: A \<simeq> B" "BC: B \<simeq> C" - let "?f: {}" = "(fst AB) :: o" *) - apply intros - unfolding equivalence_def - focus vars p q apply (elim p, elim q) - focus vars f biinv\<^sub>f g biinv\<^sub>g apply intro - \<guillemotright> apply (rule funcompI) defer by assumption+ known - \<guillemotright> by (rule funcomp_biinv) - done - done - done + proof intros + fix AB BC assume *: "AB: A \<simeq> B" "BC: B \<simeq> C" + then have + "fst AB: A \<rightarrow> B" and 1: "snd AB: biinv (fst AB)" + "fst BC: B \<rightarrow> C" and 2: "snd BC: biinv (fst BC)" + unfolding equivalence_def by typechk+ + then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk + moreover have "biinv (fst BC \<circ> fst AB)" + using * unfolding equivalence_def by (rules funcomp_biinv 1 2) + ultimately show "A \<simeq> C" + unfolding equivalence_def by intro facts + qed text \<open> Equal types are equivalent. We give two proofs: the first by induction, and diff --git a/hott/Identity.thy b/hott/Identity.thy index 1cb3946..29ce26a 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -49,6 +49,9 @@ 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> + method_setup eq = \<open>Args.term >> (fn tm => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS ( @@ -155,12 +158,12 @@ translations Lemma lu_refl [comp]: assumes "A: U i" "x: A" shows "lu (refl x) \<equiv> refl (refl x)" - unfolding refl_pathcomp_def by reduce+ + unfolding refl_pathcomp_def by reduce Lemma ru_refl [comp]: assumes "A: U i" "x: A" shows "ru (refl x) \<equiv> refl (refl x)" - unfolding pathcomp_refl_def by reduce+ + unfolding pathcomp_refl_def by reduce Lemma (derive) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" @@ -374,7 +377,7 @@ Lemma transport_const_comp [comp]: "x: A" "b: B" "A: U i" "B: U i" shows "trans_const B (refl x) b\<equiv> refl b" - unfolding transport_const_def by reduce+ + unfolding transport_const_def by reduce Lemma (derive) pathlift: assumes @@ -398,7 +401,7 @@ Lemma pathlift_comp [comp]: "\<And>x. x: A \<Longrightarrow> P x: U i" "A: U i" shows "lift P (refl x) u \<equiv> refl <x, u>" - unfolding pathlift_def by reduce+ + unfolding pathlift_def by reduce Lemma (derive) pathlift_fst: assumes @@ -438,7 +441,7 @@ Lemma dependent_map_comp [comp]: "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" shows "apd f (refl x) \<equiv> refl (f x)" - unfolding apd_def by reduce+ + unfolding apd_def by reduce Lemma (derive) apd_ap: assumes @@ -495,13 +498,13 @@ Lemma whisker_refl [comp]: assumes "A: U i" "a: A" "b: A" shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> \<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>" - unfolding right_whisker_def by reduce+ + unfolding right_whisker_def by reduce Lemma refl_whisker [comp]: assumes "A: U i" "a: A" "b: A" shows "\<lbrakk>p: a = b; q: a = b; \<alpha>: p = q\<rbrakk> \<Longrightarrow> (refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>" - unfolding left_whisker_def by reduce+ + unfolding left_whisker_def by reduce method left_whisker = (rule left_whisker) method right_whisker = (rule right_whisker) |