From 306721649f0963ab225deb8d5670cfe196bb360d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 21 Jul 2020 16:28:05 +0200
Subject: 1. Bugfix: implicits now properly name schematic variables. Fixes
 problems caused by variable name clashes. 2. reduce method now more
 principled: restricts to repeating on first subgoal. 3. An example
 declarative proof in Equivalence.thy.

---
 hott/Equivalence.thy | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'hott/Equivalence.thy')

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