From 8f4ff41d24dd8fa6844312456d47cad4be6cb239 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 9 Aug 2020 18:34:58 +0200
Subject: (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

---
 hott/Equivalence.thy | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'hott/Equivalence.thy')

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.
-- 
cgit v1.2.3

