From 4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Wed, 29 Jun 2022 01:28:53 +0200
Subject: (broken) update hott for Isabelle 2021-1

this just replaces all instance of `this` with instances of `infer`.
Unfortunately, it looks likes something else also broke, and I have
no idea what it is (but the proof for equiv_if_equal fails).

Sadly this means we can't get to univalence for now …
(but rn I'm too tired to try anything else with it)
---
 hott/Identity.thy | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'hott/Identity.thy')

diff --git a/hott/Identity.thy b/hott/Identity.thy
index ce0e0ec..6c044b4 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -203,6 +203,7 @@ Lemma (def) ap:
   shows "f x = f y"
   by (eq p) intro
 
+
 definition ap_i ("_[_]" [1000, 0])
   where [implicit]: "ap_i f p \<equiv> ap {} {} {} {} f p"
 
@@ -304,7 +305,7 @@ Lemma (def) pathcomp_cancel_left:
       by (rewr eq: pathcomp_assoc,
           rewr eq: inv_pathcomp,
           rewr eq: refl_pathcomp) refl
-    finally show "?" by this
+    finally show "?" by infer
   qed
 
 Lemma (def) pathcomp_cancel_right:
@@ -323,7 +324,7 @@ Lemma (def) pathcomp_cancel_right:
           rewr eq: pathcomp_assoc[symmetric],
           rewr eq: pathcomp_inv,
           rewr eq: pathcomp_refl) refl
-    finally show "?" by this
+    finally show "?" by infer
   qed
 
 method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7]
@@ -488,7 +489,7 @@ Lemma (def) right_whisker:
       have "s \<bullet> refl x = s" by (rule pathcomp_refl)
       also have ".. = t" by fact
       also have ".. = t \<bullet> refl x" by (rule pathcomp_refl[symmetric])
-      finally show "?" by this
+      finally show "?" by infer
     qed
   done
 
@@ -502,7 +503,7 @@ Lemma (def) left_whisker:
       have "refl x \<bullet> s = s" by (rule refl_pathcomp)
       also have ".. = t" by fact
       also have ".. = refl x \<bullet> t" by (rule refl_pathcomp[symmetric])
-      finally show "?" by this
+      finally show "?" by infer
     qed
   done
 
@@ -608,17 +609,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp:
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>"
       by (rule pathcomp_refl)
     also have ".. = \<alpha>" by (rule refl_pathcomp)
-    finally have eq\<alpha>: "? = \<alpha>" by this
+    finally have eq\<alpha>: "? = \<alpha>" by infer
 
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
       by (rule pathcomp_refl)
     also have ".. = \<beta>" by (rule refl_pathcomp)
-    finally have eq\<beta>: "? = \<beta>" by this
+    finally have eq\<beta>: "? = \<beta>" by infer
 
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a))
       = \<alpha> \<bullet> ?" by right_whisker (fact eq\<alpha>)
     also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (fact eq\<beta>)
-    finally show "? = \<alpha> \<bullet> \<beta>" by this
+    finally show "? = \<alpha> \<bullet> \<beta>" by infer
   qed
 
 Lemma (def) pathcomp_eq_horiz_pathcomp':
@@ -630,17 +631,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
       by (rule pathcomp_refl)
     also have ".. = \<beta>" by (rule refl_pathcomp)
-    finally have eq\<beta>: "? = \<beta>" by this
+    finally have eq\<beta>: "? = \<beta>" by infer
 
     have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>"
       by (rule pathcomp_refl)
     also have ".. = \<alpha>" by (rule refl_pathcomp)
-    finally have eq\<alpha>: "? = \<alpha>" by this
+    finally have eq\<alpha>: "? = \<alpha>" by infer
 
     have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a))
       = \<beta> \<bullet> ?" by right_whisker (fact eq\<beta>)
     also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (fact eq\<alpha>)
-    finally show "? = \<beta> \<bullet> \<alpha>" by this
+    finally show "? = \<beta> \<bullet> \<alpha>" by infer
   qed
 
 Lemma (def) eckmann_hilton:
@@ -657,7 +658,7 @@ Lemma (def) eckmann_hilton:
     also have ".. = \<beta> \<bullet> \<alpha>"
       by (rule pathcomp_eq_horiz_pathcomp')
     finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
-      by this
+      by infer
   qed
 
 end
-- 
cgit v1.2.3