From c2dfffffb7586662c67e44a2d255a1a97ab0398b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 2 Apr 2020 17:57:48 +0200
Subject: Brand-spanking new version using Spartan infrastructure

---
 Univalence.thy | 66 ----------------------------------------------------------
 1 file changed, 66 deletions(-)
 delete mode 100644 Univalence.thy

(limited to 'Univalence.thy')

diff --git a/Univalence.thy b/Univalence.thy
deleted file mode 100644
index dd8a13c..0000000
--- a/Univalence.thy
+++ /dev/null
@@ -1,66 +0,0 @@
-(********
-Isabelle/HoTT: Univalence
-Feb 2019
-
-********)
-
-theory Univalence
-imports Equivalence
-
-begin
-
-
-schematic_goal type_eq_imp_equiv:
-  assumes [intro]: "A: U i" "B: U i"
-  shows "?prf: A =[U i] B \<rightarrow> A \<cong> B"
-unfolding equivalence_def
-apply (rule Prod_routine, rule Sum_routine)
-prefer 3 apply (derive lems: transport_biinv)
-done
-
-(* Copy-paste the derived proof term as the definition of idtoeqv for now;
-   should really have some automatic export of proof terms, though.
-*)
-definition idtoeqv :: "[ord, t, t] \<Rightarrow> t"  ("(2idtoeqv[_, _, _])") where "
-idtoeqv[i, A, B] \<equiv>
-  \<lambda>p: A =[U i] B.
-  < transport[U i, Id, A, B]`p, <
-      < transport[U i, Id, B, A]`(inv[U i, A, B]`p),
-        happly[x: A. A]
-          ((transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p)
-          (id A)
-          (indEq
-            (\<lambda>A B p.
-              (transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p
-                =[A \<rightarrow> A] id A)
-            (\<lambda>x. refl (id x)) A B p)
-      >,
-      < transport[U i, Id, B, A]`(inv[U i, A, B]`p),
-        happly[x: B. B]
-          ((transport[U i, Id, A, B]`p) o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p)))
-          (id B)
-          (indEq
-            (\<lambda>A B p.
-              transport[U i, Id, A, B]`p o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p))
-                =[B \<rightarrow> B] id B)
-            (\<lambda>x. refl (id x)) A B p)
-      >
-    >
-  >
-"
-
-corollary idtoeqv_type:
-  assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B"
-  shows "idtoeqv[i, A, B]: A =[U i] B \<rightarrow> A \<cong> B"
-unfolding idtoeqv_def by (routine add: type_eq_imp_equiv)
-
-declare idtoeqv_type [intro]
-
-
-text \<open>For now, we use bi-invertibility as our definition of equivalence.\<close>
-
-axiomatization univalance :: "[ord, t, t] \<Rightarrow> t"
-where univalence: "univalence i A B: biinv[A, B] idtoeqv[i, A, B]"
-
-
-end
-- 
cgit v1.2.3