diff options
author | Josh Chen | 2020-05-25 15:24:20 +0200 |
---|---|---|
committer | Josh Chen | 2020-05-25 15:24:20 +0200 |
commit | 8f47d9f3ca38a3fc2c3c462d1157866081102ce1 (patch) | |
tree | 460181389821f3286fc7082214629817d6ad3427 /spartan/theories/Equivalence.thy | |
parent | 3de65af4b59e6d3cc8e74acecf704beccd54b774 (diff) |
1. equality method now uses general elimination tactic. 2. New constant `` refers to rhs of equalities.
Diffstat (limited to 'spartan/theories/Equivalence.thy')
-rw-r--r-- | spartan/theories/Equivalence.thy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy index 73f1e0d..3415249 100644 --- a/spartan/theories/Equivalence.thy +++ b/spartan/theories/Equivalence.thy @@ -86,7 +86,7 @@ Lemma (derive) commute_homotopy: shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)" \<comment> \<open>Need this assumption unfolded for typechecking:\<close> supply assms(8)[unfolded homotopy_def] - apply (equality \<open>p:_\<close>) + apply (eq p) focus vars x apply reduce \<comment> \<open>Here it would really be nice to have automation for transport and @@ -366,7 +366,7 @@ Lemma assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" shows "A \<simeq> B" - by (equality \<open>p:_\<close>) (rule equivalence_refl) + by (eq p) (rule equivalence_refl) text \<open> The following proof is wordy because (1) the typechecker doesn't rewrite, and @@ -383,7 +383,7 @@ Lemma (derive) id_imp_equiv: \<comment> \<open>Switch off auto-typechecking, which messes with universe levels\<close> supply [[auto_typechk=false]] - \<guillemotright> apply (equality \<open>p:_\<close>) + \<guillemotright> apply (eq p, typechk) \<^item> prems vars A B apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric]) apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric]) |