Theories fully reorganized. Well-formedness rules removed. New methods etc.

1 files changed, 53 insertions, 141 deletions

diff --git a/Univalence.thy b/Univalence.thy
index 001ee33..3c9b520 100644
--- a/Univalence.thy
+++ b/Univalence.thy
@@ -1,176 +1,88 @@
-(*  Title:  HoTT/Univalence.thy
-    Author: Joshua Chen
+(*
+Title:  Univalence.thy
+Author: Joshua Chen
+Date:   2018
 
 Definitions of homotopy, equivalence and the univalence axiom.
 *)
 
 theory Univalence
-imports
-  HoTT_Methods
-  EqualProps
-  ProdProps
-  Sum
+imports HoTT_Methods EqualProps Prod Sum
 
 begin
 
 
 section \<open>Homotopy and equivalence\<close>
 
-axiomatization homotopic :: "[t, t] \<Rightarrow> t"  (infix "~" 100) where
-  homotopic_def: "\<lbrakk>
-    f: \<Prod>x:A. B x;
-    g: \<Prod>x:A. B x
-  \<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"
+definition homotopic :: "[t, tf, t, t] \<Rightarrow> t" where "homotopic A B f g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"
 
-axiomatization isequiv :: "t \<Rightarrow> t" where
-  isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)"
+syntax "_homotopic" :: "[t, idt, t, t, t] \<Rightarrow> t"  ("(1_ ~[_:_. _]/ _)" [101, 0, 0, 0, 101] 100)
+translations "f ~[x:A. B] g" \<rightleftharpoons> "CONST homotopic A (\<lambda>x. B) f g"
 
-definition equivalence :: "[t, t] \<Rightarrow> t"  (infix "\<simeq>" 100)
-  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f"
-
-
-text "The identity function is an equivalence:"
-
-lemma isequiv_id:
-  assumes "A: U i" and "id: A \<rightarrow> A"
-  shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id"
-proof (derive lems: assms isequiv_def homotopic_def)
-  fix g assume asm: "g: A \<rightarrow> A"
-  show "id \<circ> g: A \<rightarrow> A"
-    unfolding compose_def by (routine lems: asm assms)
-
-  show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i"
-    unfolding compose_def by (routine lems: asm assms)
-  next
-  
-  show "<\<^bold>\<lambda>x. x, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~ id"
-    unfolding compose_def by (derive lems: assms homotopic_def)
-
-  show "<\<^bold>\<lambda>x. x, lambda refl>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~ id"
-    unfolding compose_def by (derive lems: assms homotopic_def)
-qed (rule assms)
+declare homotopic_def [comp]
 
+definition isequiv :: "[t, t, t] \<Rightarrow> t"  ("(3isequiv[_, _]/ _)") where
+  "isequiv[A, B] f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~[x:A. A] id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~[x:B. B] id)"
 
-text "We use the following lemma in a few proofs:"
+text \<open>
+The meanings of the syntax defined above are:
+\<^item> @{term "f ~[x:A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "\<Prod>x:A. B x"}.
+\<^item> @{term "isequiv[A, B] f"} expresses that the non-dependent function @{term f} of type @{term "A \<rightarrow> B"} is an equivalence.
+\<close>
 
-lemma isequiv_type:
-  assumes "A: U i" and "B: U i" and "f: A \<rightarrow> B"
-  shows "isequiv f: U i"
-  by (derive lems: assms isequiv_def homotopic_def compose_def)
-
-
-text "The equivalence relation \<open>\<simeq>\<close> is symmetric:"
+definition equivalence :: "[t, t] \<Rightarrow> t"  (infix "\<simeq>" 100)
+  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv[A, B] f"
+
+lemma id_isequiv:
+  assumes "A: U i" "id: A \<rightarrow> A"
+  shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id"
+unfolding isequiv_def proof (routine add: assms)
+  show "\<And>g. g: A \<rightarrow> A \<Longrightarrow> id \<circ> g ~[x:A. A] id: U i" by (derive lems: assms)
+  show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~[x:A. A] id" by (derive lems: assms)
+  show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~[x:A. A] id" by (derive lems: assms)
+qed
 
-lemma equiv_sym:
+lemma equivalence_symm:
   assumes "A: U i" and "id: A \<rightarrow> A"
   shows "<id, <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>>: A \<simeq> A"
 unfolding equivalence_def proof
-  show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" using assms by (rule isequiv_id)
-  
-  fix f assume "f: A \<rightarrow> A"
-  with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type)
-qed (rule assms)
+  show "\<And>f. f: A \<rightarrow> A \<Longrightarrow> isequiv[A, A] f: U i" by (derive lems: assms isequiv_def)
+  show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id" using assms by (rule id_isequiv)
+qed fact
 
 
-section \<open>idtoeqv and the univalence axiom\<close>
+section \<open>idtoeqv\<close>
 
-definition idtoeqv :: t
-  where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"
+definition idtoeqv :: t where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"
 
-
-text "We prove that equal types are equivalent. The proof is long and uses universes."
+text \<open>We prove that equal types are equivalent. The proof involves universe types.\<close>
 
 theorem
   assumes "A: U i" and "B: U i"
   shows "idtoeqv: (A =[U i] B) \<rightarrow> A \<simeq> B"
-unfolding idtoeqv_def equivalence_def
-proof
-  fix p assume "p: A =[U i] B"
-  show "<transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>: \<Sum>f: A \<rightarrow> B. isequiv f"
-  proof
-    { fix f assume "f: A \<rightarrow> B"
-    with assms show "isequiv f: U i" by (rule isequiv_type)
-    }
-    
-    show "transport p: A \<rightarrow> B"
-    proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="Suc i"])
-      show "\<And>x. x: U i \<Longrightarrow> x: U (Suc i)" by cumulativity
-      show "U i: U (Suc i)" by hierarchy
-    qed fact+
+unfolding idtoeqv_def equivalence_def proof (routine add: assms)
+  show *: "\<And>f. f: A \<rightarrow> B \<Longrightarrow> isequiv[A, B] f: U i"
+  unfolding isequiv_def by (derive lems: assms)
+
+  show "\<And>p. p: A =[U i] B \<Longrightarrow> transport p: A \<rightarrow> B"
+  by (derive lems: assms transport_type[where ?i="Suc i"])
+  \<comment> \<open>Instantiate @{thm transport_type} with a suitable universe level here...\<close>
+
+  show "\<And>p. p: A =[U i] B \<Longrightarrow> ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv[A, B] (transport p)"
+  proof (elim Equal_elim)
+    show "\<And>T. T: U i \<Longrightarrow> <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[T, T] (transport (refl T))"
+    by (derive lems: transport_comp[where ?i="Suc i" and ?A="U i"] id_isequiv)
+    \<comment> \<open>...and also here.\<close>
     
-    show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)"
-    proof (rule Equal_elim[where ?C="\<lambda>_ _ p. isequiv (transport p)"])
-      fix A assume asm: "A: U i"
-      show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv (transport (refl A))"
-      proof (derive lems: isequiv_def)
-        show "transport (refl A): A \<rightarrow> A"
-          unfolding transport_def
-          by (compute lems: Equal_comp[where ?A="U i" and ?C="\<lambda>_ _ _. A \<rightarrow> A"]) (derive lems: asm)
-        
-        show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
-                (\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times>
-                (\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)"
-        proof (subst (1 2) transport_comp)
-          show "U i: U (Suc i)" by (rule U_hierarchy) rule
-          show "U i: U (Suc i)" by (rule U_hierarchy) rule
-          
-          show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
-                  (\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)"
-          proof
-            show "\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id: U i"
-            proof (derive lems: asm homotopic_def)
-              fix g assume asm': "g: A \<rightarrow> A"
-              show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
-              show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
-            qed (routine lems: asm)
-
-            show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. id \<circ> g ~ id"
-            proof
-              fix g assume asm': "g: A \<rightarrow> A"
-              show "id \<circ> g ~ id: U i"
-              proof (derive lems: homotopic_def)
-                show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
-                show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
-              qed (routine lems: asm)
-              next
-              show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
-              proof compute
-                show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
-              qed (rule asm)
-            qed (routine lems: asm)
-
-            show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. g \<circ> id ~ id"
-            proof
-              fix g assume asm': "g: A \<rightarrow> A"
-              show "g \<circ> id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def)
-              next
-              show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
-              proof compute
-                show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
-              qed (rule asm)
-            qed (routine lems: asm)
-          qed
-        qed fact+
-      qed
-      next
-      
-      fix A' B' p' assume asm:  "A': U i" "B': U i" "p': A' =[U i] B'"
-      show "isequiv (transport p'): U i"
-      proof (rule isequiv_type)
-        show "transport p': A' \<rightarrow> B'" by (derive lems: asm transport_def)
-      qed fact+
-    qed fact+
-  qed
-  next
-
-  show "A =[U i] B: U (Suc i)" proof (derive lems: assms, (rule U_hierarchy, rule lt_Suc)?)+
-qed
+    show "\<And>A B p. \<lbrakk>A: U i; B: U i; p: A =[U i] B\<rbrakk> \<Longrightarrow> isequiv[A, B] (transport p): U i"
+    unfolding isequiv_def by (derive lems: assms transport_type)
+  qed fact+
+qed (derive lems: assms)
 
 
-text "The univalence axiom."
+section \<open>The univalence axiom\<close>
 
-axiomatization univalence :: t where
-  UA: "univalence: isequiv idtoeqv"
+axiomatization univalence :: "[t, t] \<Rightarrow> t" where UA: "univalence A B: isequiv[A, B] idtoeqv"
 
 
 end