From fa413a91f73773c4cb9c83ed65837320b598e1d4 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 1 Mar 2019 20:44:02 +0100
Subject: finished proof of transport_biinv

---
 Univalence.thy | 37 +++++++++++++++++++++----------------
 1 file changed, 21 insertions(+), 16 deletions(-)

(limited to 'Univalence.thy')

diff --git a/Univalence.thy b/Univalence.thy
index 42e452e..d4c0909 100644
--- a/Univalence.thy
+++ b/Univalence.thy
@@ -163,34 +163,39 @@ prefer 2
 prefer 9
   apply (rule Sum_routine)
   prefer 3 apply (rule transport_invr_hom)
-\<comment> \<open>The remaining subgoals can now be handled relatively easily.\<close>
-proof -
-  show *: "U i: U (Suc i)" by derive
+proof - \<comment> \<open>The remaining subgoals can now be handled relatively easily.\<close>
+  show "U i: U (Suc i)" by derive
   show "U i: U (Suc i)" by fact
-
-  fix g assume [intro]: "g: (id U i)`B \<rightarrow> (id U i)`A"
-
-  have
-    "transport (id U i) A B p o[(id U i)`B] g: (id U i)`B \<rightarrow> (id U i)`B"
+  
+  have "\<And>g. g: (id U i)`B \<rightarrow> (id U i)`A \<Longrightarrow>
+    transport (id U i) A B p o[(id U i)`B] g: (id U i)`B \<rightarrow> (id U i)`B"
       proof show "(id U i)`A: U i" by derive qed derive
-  moreover have
-    "transport[id U i, A, B] p o[(id U i)`B] g ~[x: (id U i)`B. (id U i)`B] id (id U i)`B: U i"
+  have "\<And>g. g: (id U i)`B \<rightarrow> (id U i)`A \<Longrightarrow>
+    transport[id U i, A, B] p o[(id U i)`B] g ~[x: (id U i)`B. (id U i)`B] id (id U i)`B: U i"
       apply rule prefer 3 apply (fact, derive) done
-  then show
-    "(transport[id U i, A, B] p) o[(id U i)`B] g ~[x: (id U i)`B. (id U i)`B] id (id U i)`B: U i"
+  then show "\<And>g. g: (id U i)`B \<rightarrow> (id U i)`A \<Longrightarrow>
+    transport[id U i, A, B] p o[(id U i)`B] g ~[x: (id U i)`B. (id U i)`B] id (id U i)`B: U i"
   by routine
 
+  show "\<Sum>g: (id U i)`B \<rightarrow> (id U i)`A.
+    transport[id U i, A, B] p o[(id U i)`B] g ~[x: (id U i)`B. (id U i)`B] id (id U i)`B: U i"
+  proof
+    show "\<And>g. g : (id U i)`B \<rightarrow> (id U i)`A \<Longrightarrow>
+      Eq.transport (id U i) A B p o[(id U i)`B] g ~[x: (id U i)`B. (id U i)`B] id (id U i)`B: U i"
+    by fact
+  qed derive
+
+  fix g assume [intro]: "g: (id U i)`B \<rightarrow> (id U i)`A"
   have
     "g o[(id U i)`A] transport (id U i) A B p: (id U i)`A \<rightarrow> (id U i)`A"
       proof show "(id U i)`B: U i" by derive qed derive
-  moreover have
+  have
     "g o[(id U i)`A] transport (id U i) A B p ~[x: (id U i)`A. (id U i)`A] id (id U i)`A: U i"
       apply rule prefer 3 apply (fact, derive) done
   then show
     "g o[(id U i)`A] transport (id U i) A B p ~[x: (id U i)`A. (id U i)`A] id (id U i)`A: U i"
   by routine
-
-qed
+qed derive
 
 
 section \<open>Univalence\<close>
@@ -209,7 +214,7 @@ proof -
   moreover have [intro]:
     "(id U i)`A \<rightarrow> (id U i)`B \<equiv> A \<rightarrow> B" by derive
   ultimately show "transport (id U i) A B p: A \<rightarrow> B" by simp
-qed deriv
+qed derive
 
 (*
 section \<open>The univalence axiom\<close>
-- 
cgit v1.2.3