aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2020-08-09 18:34:58 +0200
committerJosh Chen2020-08-09 18:34:58 +0200
commit8f4ff41d24dd8fa6844312456d47cad4be6cb239 (patch)
tree05cb7780daead07c4714daa7e1fc19c940283b02 /hott
parentc530305cbcafba9f66f1a55a1b5177a62f52535c (diff)
(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
Diffstat (limited to 'hott')
-rw-r--r--hott/Equivalence.thy13
1 files changed, 6 insertions, 7 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index d85e6de..7d1f2b1 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -162,8 +162,7 @@ Corollary (def) commute_homotopy':
rewrite at "_ = \<hole>" id_comp[symmetric])
have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
- by (rule left_whisker) (fact, rule
- ap_id[where ?A=A and ?x="f x" and ?y=x, simplified id_comp, symmetric])
+ by (rule left_whisker, transport eq: ap_id) (reduce+, 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
@@ -433,28 +432,28 @@ Lemma (def) equiv_if_equal:
\<^enum> vars A B
apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
using [[solve_side_conds=1]]
- apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
apply (rule transport, rule Ui_in_USi)
apply (rule lift_universe_codomain, rule Ui_in_USi)
apply (typechk, rule Ui_in_USi)
- done
+ by facts
\<^enum> vars A
using [[solve_side_conds=1]]
apply (subst transport_comp)
\<circ> by (rule Ui_in_USi)
\<circ> by reduce (rule in_USi_if_in_Ui)
- \<circ> by reduce (rule id_is_biinv)
+ \<circ> by reduce (rule id_is_biinv, fact)
done
done
\<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close>
apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
using [[solve_side_conds=1]]
- apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
apply (rule transport, rule Ui_in_USi)
apply (rule lift_universe_codomain, rule Ui_in_USi)
apply (typechk, rule Ui_in_USi)
- done
+ by facts
done
(*Uncomment this to see all implicits from here on.