From dcf87145a1059659099bbecde55973de0d36d43f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 03:04:37 +0200
Subject: Theories fully reorganized. Well-formedness rules removed. New
 methods etc.

---
 Equal.thy        |  10 +-
 EqualProps.thy   | 398 ++++++++++++-------------------------------------------
 HoTT_Base.thy    |   4 +-
 HoTT_Methods.thy |  18 +--
 Prod.thy         |   5 +-
 Univalence.thy   | 194 ++++++++-------------------
 6 files changed, 158 insertions(+), 471 deletions(-)

diff --git a/Equal.thy b/Equal.thy
index f9bc223..7a31e37 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -7,7 +7,7 @@ Equality type
 *)
 
 theory Equal
-imports HoTT_Base HoTT_Methods
+imports HoTT_Base
 
 begin
 
@@ -36,13 +36,13 @@ axiomatization where
     p: x =\<^sub>A y;
     x: A;
     y: A;
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
 
   Equal_comp: "\<lbrakk>
     a: A;
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
 lemmas Equal_comp [comp]
diff --git a/EqualProps.thy b/EqualProps.thy
index 19c788c..abb2623 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -1,361 +1,137 @@
-(*  Title:  HoTT/EqualProps.thy
-    Author: Josh Chen
+(*
+Title:  EqualProps.thy
+Author: Joshua Chen
+Date:   2018
 
 Properties of equality
 *)
 
 theory EqualProps
-  imports
-    HoTT_Methods
-    Equal
-    Prod
+imports HoTT_Methods Equal Prod
+
 begin
 
 
-section \<open>Symmetry / Path inverse\<close>
-
-definition inv :: "t \<Rightarrow> t"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p"
-
-text "
-  In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use.
-  The proof is finished with a standard application of the relevant type rules.
-"
-
-lemma inv_type:
-  assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
-unfolding inv_def
-by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms)
-  \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close>
-
-text "
-  The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules.
-  (If viewing this inside Isabelle, place the cursor after the \<open>proof\<close> statement and observe the second subgoal.)
-"
-
-lemma inv_comp:
-  assumes "A : U i " and "a : A" shows "(refl a)\<inverse> \<equiv> refl a"
-unfolding inv_def
-proof compute
-  show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
-qed (routine lems: assms)
-
-
-section \<open>Transitivity / Path composition\<close>
-
-text "
-  Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>.
-"
-
-definition rpathcomp :: t where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
-
-text "
-  More complicated proofs---the nested path inductions require more explicit step-by-step rule applications:
-"
-
-lemma rpathcomp_type:
-  assumes "A: U i"
-  shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-unfolding rpathcomp_def
-proof
-  fix x assume 1: "x: A"
-  show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-  proof
-    fix y assume 2: "y: A"
-    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-    proof
-      fix p assume 3: "p: x =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=x and ?y=y])
-        show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z"
-            show "ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm)
-          qed (routine lems: assms)
-        qed (rule assms)
-      qed (routine lems: assms 1 2 3)
-    qed (routine lems: assms 1 2)
-  qed (rule assms)
-qed fact
-
-corollary
-  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
-  shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z"
-  by (routine lems: assms rpathcomp_type)
-
-text "
-  The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule.
-"
-
-lemma rpathcomp_comp:
-  assumes "A: U i" and "a: A"
-  shows "rpathcomp`a`a`(refl a)`a`(refl a) \<equiv> refl a"
-unfolding rpathcomp_def
-proof compute
-  fix x assume 1: "x: A"
-  show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-  proof
-    fix y assume 2: "y: A"
-    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-    proof
-      fix p assume 3: "p: x =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=x and ?y=y])
-        show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            fix u z assume asm: "u: A" "z: A"
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm)
-          qed (routine lems: assms)
-        qed (rule assms)
-      qed (routine lems: assms 1 2 3)
-    qed (routine lems: assms 1 2)
-  qed (rule assms)
-
-  next show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \<equiv> refl a"
-  proof compute
-    fix y assume 1: "y: A"
-    show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)"
-    proof
-      fix p assume 2: "p: a =\<^sub>A y"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=a and ?y=y])
-        fix u assume 3: "u: A"
-        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          fix z assume 4: "z: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4)
-          qed (routine lems: assms 3 4)
-        qed fact
-      qed (routine lems: assms 1 2)
-    qed (routine lems: assms 1)
-    
-    next show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \<equiv> refl a"
-    proof compute
-      fix p assume 1: "p: a =\<^sub>A a"
-      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A z \<rightarrow> a =\<^sub>A z"
-      proof (rule Equal_elim[where ?x=a and ?y=a])
-        fix u assume 2: "u: A"
-        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          fix z assume 3: "z: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3)
-          qed (routine lems: assms 2 3)
-        qed fact
-      qed (routine lems: assms 1)
-      
-      next show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \<equiv> refl a"
-      proof compute
-        fix u assume 1: "u: A"
-        show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-        proof
-          fix z assume 2: "z: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
-          proof
-            show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2)
-          qed (routine lems: assms 1 2)
-        qed fact
-        
-        next show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`(refl a) \<equiv> refl a"
-        proof compute
-          fix a assume 1: "a: A"
-          show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
-          proof
-            show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a"
-            by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1)
-          qed (routine lems: assms 1)
-          
-          next show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`(refl a) \<equiv> refl a"
-          proof compute
-            show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a"
-            by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms)
-            show "ind\<^sub>= refl (refl a) \<equiv> refl a"
-            proof compute
-              show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" ..
-            qed (routine lems: assms)
-          qed (routine lems: assms)
-        qed fact
-      qed (routine lems: assms)
-    qed (routine lems: assms)
-  qed fact
-qed fact
-
-
-text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead."
-
-axiomatization pathcomp :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 120) where
-  pathcomp_def: "\<lbrakk>
-    A: U i;
-    x: A; y: A; z: A;
-    p: x =\<^sub>A y; q: y =\<^sub>A z
-  \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q"
+section \<open>Symmetry of equality/Path inverse\<close>
 
+definition inv :: "t \<Rightarrow> t"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl x) p"
 
-lemma pathcomp_type:
-  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
-  shows "p \<bullet> q: x =\<^sub>A z"
+lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =\<^sub>A y\<rbrakk> \<Longrightarrow> p\<inverse>: y =\<^sub>A x"
+unfolding inv_def by (elim Equal_elim) routine
 
-proof (subst pathcomp_def)
-  show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
-qed (routine lems: assms rpathcomp_type)
+lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (refl a)\<inverse> \<equiv> refl a"
+unfolding inv_def by compute routine
 
 
-lemma pathcomp_comp:
-  assumes "A : U i" and "a : A" shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
-by (subst pathcomp_def) (routine lems: assms rpathcomp_comp)
+section \<open>Transitivity of equality/Path composition\<close>
 
+text \<open>
+Composition function, of type @{term "x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"} polymorphic over @{term A}, @{term x}, @{term y}, and @{term z}.
+\<close>
 
-lemmas inv_type [intro]
-lemmas pathcomp_type [intro]
+definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
 
-lemmas inv_comp [comp]
-lemmas pathcomp_comp [comp]
+syntax "_pathcomp" :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 120)
+translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
 
+lemma pathcomp_type:
+  assumes "A: U i" and "x: A" "y: A" "z: A"
+  shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"
+unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms)
 
-section \<open>Weak higher groupoid structure of types\<close>
+corollary pathcomp_trans:
+  assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  shows "p \<bullet> q: x =\<^sub>A z"
+by (routine add: assms pathcomp_type)
 
-schematic_goal whg1a:
+lemma pathcomp_comp:
+  assumes "A: U i" and "a: A"
+  shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
+unfolding pathcomp_def proof compute
+  show "(ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) (refl a))`(refl a) \<equiv> refl a"
+  proof compute
+    show "\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q): a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
+    by (routine add: assms)
+
+    show "(\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q))`(refl a) \<equiv> refl a"
+    proof compute
+      show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>x. refl x) q: a =\<^sub>A a" by (routine add: assms)
+    qed (derive lems: assms)
+  qed (routine add: assms)
+
+  show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) p: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
+  by (routine add: assms)
+qed (routine add: assms)
+
+
+section \<open>Higher groupoid structure of types\<close>
+
+schematic_goal pathcomp_right_id:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows "?a: p =[x =\<^sub>A y] (p \<bullet> (refl(y)))"
-proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))"
-  by compute (routine lems: assms)
-qed (routine lems: assms)
+  shows "?a: p \<bullet> (refl y) =[x =\<^sub>A y] p"
+proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])  \<comment> \<open>@{method elim} does not seem to work with schematic goals.\<close>
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms pathcomp_comp)
+qed (routine add: assms pathcomp_type)
 
-schematic_goal whg1b:
+schematic_goal pathcomp_left_id:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows "?a: p =[x =\<^sub>A y] (refl(x) \<bullet> p)"
+  shows "?a: (refl x) \<bullet> p =[x =\<^sub>A y] p"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))"
-  by compute (routine lems: assms)
-qed (routine lems: assms)
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms pathcomp_comp)
+qed (routine add: assms pathcomp_type)
 
-schematic_goal whg2a:
+schematic_goal pathcomp_left_inv:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): ((refl(x))\<inverse> \<bullet> refl(x)) =[x =\<^sub>A x] refl(x)"
-  by (compute | routine lems: assms)+
-qed (routine lems: assms)+
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse> \<bullet> (refl x) =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms inv_comp pathcomp_comp)
+qed (routine add: assms inv_type pathcomp_type)
 
-schematic_goal whg2b:
+schematic_goal pathcomp_right_inv:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x) \<bullet> (refl(x))\<inverse>) =[x =\<^sub>A x] refl(x)"
-  by (compute | routine lems: assms)+
-qed (routine lems: assms)+
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x)\<inverse> =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms inv_comp pathcomp_comp)
+qed (routine add: assms inv_type pathcomp_type)
 
-schematic_goal whg3:
+schematic_goal inv_involutive:
   assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x))\<inverse>\<inverse> =[x =\<^sub>A x] refl(x)"
-  by (compute | routine lems: assms)+
-qed (routine lems: assms)
-
-
-lemma assumes "A: U(i)" shows "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x"
-by (rule Prod_atomize[where ?A=A and ?B="\<lambda>x. x =\<^sub>A x"]) (routine lems: assms)
-
+  show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse>\<inverse> =[x =\<^sub>A x] (refl x)"
+  by (derive lems: assms inv_comp)
+qed (routine add: assms inv_type)
 
-schematic_goal
+schematic_goal pathcomp_assoc:
   assumes
-    "A: U(i)" and
-    "x: A" "y: A" "z: A" "w: A" and
+    "A: U(i)"
+    "x: A" "y: A" "z: A" "w: A"
     "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
   shows
     "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r"
 proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p])
-  fix y assume "y: A"
-  show "refl(q \<bullet> r): refl(y) \<bullet> (q \<bullet> r) =[y =\<^sub>A w] (refl(y) \<bullet> q) \<bullet> r"
-  proof (compute lems: whg1b)
-  
-
-section \<open>Higher groupoid structure of types\<close>
-
-lemma
-  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> (refl y)" and
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \<bullet> p"
-
-proof -
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> (refl y)"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] (refl x) \<bullet> p"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-qed
-
-
-lemma
-  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" and
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)"
-
-proof -
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)"
-  by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
-qed
-
-
-lemma
-  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
-  shows "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
-by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)
-
-text "Next we construct a proof term of associativity of path composition."
-
-schematic_goal
-  assumes
-    "A: U i"
-    "x: A" "y: A" "z: A" "w: A"
-    "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
-  shows
-    "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A z] (p \<bullet> q) \<bullet> r"
-
-apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y])
-apply (rule assms)+
-\<comment> \<open>Continue by substituting \<open>refl x \<bullet> q = q\<close> etc.\<close>
-sorry
+  fix x assume "x: A"
+  show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r"
+  \<comment> \<open>This requires substitution of *propositional* equality. \<close>
+  sorry
+  oops
 
 
 section \<open>Transport\<close>
 
-definition transport :: "t \<Rightarrow> t" where
-  "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p"
+definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>_. (\<^bold>\<lambda>x. x)) p"
 
-text "Note that \<open>transport\<close> is a polymorphic function in our formulation."
+text \<open>Note that @{term transport} is a polymorphic function in our formulation.\<close>
 
-lemma transport_type:
-  assumes
-    "A: U i" "P: A \<longrightarrow> U i"
-    "x: A" "y: A"
-    "p: x =\<^sub>A y"
-  shows "transport p: P x \<rightarrow> P y"
-unfolding transport_def
-by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms)
-
-lemma transport_comp:
-  assumes "A: U i" and "x: A"
-  shows "transport (refl x) \<equiv> id"
-unfolding transport_def by (derive lems: assms)
+lemma transport_type: "\<lbrakk>p: x =\<^sub>A y; x: A; y: A; A: U i; P: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> transport p: P x \<rightarrow> P y"
+unfolding transport_def by (elim Equal_elim) routine
+
+lemma transport_comp: "\<lbrakk>A: U i; x: A\<rbrakk> \<Longrightarrow> transport (refl x) \<equiv> id"
+unfolding transport_def by derive
 
 
 end
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 17e3142..7453883 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -7,9 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty
 *)
 
 theory HoTT_Base
-imports
-  Pure
-  "HOL-Eisbach.Eisbach"
+imports Pure "HOL-Eisbach.Eisbach"
 
 begin
 
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 411176e..8929f69 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -3,14 +3,11 @@ Title:  HoTT_Methods.thy
 Author: Joshua Chen
 Date:   2018
 
-Method setup for the HoTT logic. Relies heavily on Eisbach.
+Method setup for the HoTT logic.
 *)
 
 theory HoTT_Methods
-imports
-  "HOL-Eisbach.Eisbach"
-  "HOL-Eisbach.Eisbach_Tools"
-  HoTT_Base
+imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 
 begin
 
@@ -43,16 +40,19 @@ Premises of the rule(s) applied are added as new subgoals.
 
 section \<open>Derivation search\<close>
 
-text \<open>Combine @{method routine} and @{method compute} to search for derivations of judgments.\<close>
+text \<open>
+Combine @{method routine} and @{method compute} to search for derivations of judgments.
+Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}.
+\<close>
 
-method derive uses lems = (routine add: lems | compute comp: lems)+
+method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+
 
 
 section \<open>Induction\<close>
 
 text \<open>
-  Placeholder section for the automation of induction, i.e. using the elimination rules.
-  At the moment one must directly apply them with \<open>rule X_elim\<close>.
+Placeholder section for the automation of induction, i.e. using the elimination rules.
+At the moment one must directly apply them with \<open>rule X_elim\<close>.
 \<close>
 
 
diff --git a/Prod.thy b/Prod.thy
index db18454..4aa7119 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -17,7 +17,7 @@ section \<open>Basic definitions\<close>
 axiomatization
   Prod   :: "[t, tf] \<Rightarrow> t" and
   lambda :: "(t \<Rightarrow> t) \<Rightarrow> t"  (binder "\<^bold>\<lambda>" 30) and
-  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`/_)" [60, 61] 60)  \<comment> \<open>Application binds tighter than abstraction.\<close>
+  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`/_)" [105, 106] 105)  \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
   "_prod" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Prod>_:_./ _)" 30)
@@ -43,7 +43,7 @@ axiomatization where
 
   Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and
 
-  Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and
+  Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and
 
   Prod_uniq: "f: \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. f`x \<equiv> f" and
 
@@ -68,6 +68,7 @@ lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 section \<open>Additional definitions\<close>
 
 definition compose :: "[t, t] \<Rightarrow> t"  (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)"
+
 syntax "_compose" :: "[t, t] \<Rightarrow> t"  (infixr "\<circ>" 110)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
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
-- 
cgit v1.2.3