diff options
| author | Josh Chen | 2020-08-09 18:34:58 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-08-09 18:34:58 +0200 |
| commit | 8f4ff41d24dd8fa6844312456d47cad4be6cb239 (patch) | |
| tree | 05cb7780daead07c4714daa7e1fc19c940283b02 /hott | |
| parent | c530305cbcafba9f66f1a55a1b5177a62f52535c (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.thy | 13 |
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. |