5 files changed, 60 insertions, 16 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 745bc67..8007b89 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -202,7 +202,7 @@ Lemma is_qinvI:
   unfolding is_qinv_def
   proof intro
     show "g: B \<rightarrow> A" by fact
-    show "g \<circ> f ~ id A \<and> f \<circ> g ~ id B" by (intro; fact)
+    show "g \<circ> f ~ id A \<times> f \<circ> g ~ id B" by (intro; fact)
   qed
 
 Lemma is_qinv_components [type]:
@@ -405,8 +405,9 @@ text \<open>
 \<close>
 
 Lemma (def) equiv_if_equal:
+  notes Ui_in_USi [form]
   assumes
-    "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+    "A: U i" "B: U i" "p: A = B"
   shows "<transp (id (U i)) p, ?isequiv>: A \<simeq> B"
   unfolding equivalence_def
   apply intro defer
@@ -415,13 +416,10 @@ Lemma (def) equiv_if_equal:
         apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
         using [[solve_side_conds=1]]
         apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
-        apply (rule transport, rule Ui_in_USi)
-        by (rule lift_universe_codomain, rule Ui_in_USi)
+        using Ui_in_USi by (rule transport, rule lift_universe_codomain)
       \<^enum> vars A
-        using [[solve_side_conds=1]]
         apply (comp transport_comp)
-          \<circ> by (rule Ui_in_USi)
-          \<circ> by compute (rule U_lift)
+          \<circ> by (rule U_lift)
           \<circ> by compute (rule id_is_biinv)
         done
       done
@@ -430,9 +428,16 @@ Lemma (def) equiv_if_equal:
       apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
       using [[solve_side_conds=1]]
       apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
-      apply (rule transport, rule Ui_in_USi)
-      by (rule lift_universe_codomain, rule Ui_in_USi)
+      using Ui_in_USi by (rule transport, rule lift_universe_codomain)
   done
 
+Definition idtoeqv: ":= MLTT.fst (A \<rightarrow> B) is_biinv (equiv_if_equal i A B p)"
+  where "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+  using equiv_if_equal unfolding equivalence_def
+  by typechk
+
+definition idtoeqv_i ("idtoeqv")
+  where [implicit]: "idtoeqv p \<equiv> Equivalence.idtoeqv {} {} {} p"
+
 
 end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 9ae0894..ce0e0ec 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -259,16 +259,16 @@ section \<open>Transport\<close>
 Lemma (def) transport:
   assumes
     "A: U i"
-    "\<And>x. x: A \<Longrightarrow> P x: U i"
     "x: A" "y: A"
     "p: x = y"
+    "\<And>x. x: A \<Longrightarrow> P x: U i"
   shows "P x \<rightarrow> P y"
   by (eq p) intro
 
 definition transport_i ("transp")
-  where [implicit]: "transp P p \<equiv> transport {} P {} {} p"
+  where [implicit]: "transp P p \<equiv> transport {} {} {} p P"
 
-translations "transp P p" \<leftharpoondown> "CONST transport A P x y p"
+translations "transp P p" \<leftharpoondown> "CONST transport A x y p P"
 
 Lemma transport_comp [comp]:
   assumes
diff --git a/hott/List_HoTT.thy b/hott/List_HoTT.thy
index d866f59..a48d2ab 100644
--- a/hott/List_HoTT.thy
+++ b/hott/List_HoTT.thy
@@ -10,8 +10,8 @@ section \<open>Length\<close>
 definition [implicit]: "len \<equiv> ListRec {} Nat 0 (fn _ _ rec. suc rec)"
 
 experiment begin
-  Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)
-  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+
+  Lemma "len [] \<equiv> ?n" by compute
+  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by compute
 end
 
 
diff --git a/hott/Propositions.thy b/hott/Propositions.thy
index 66e34d2..2c98a5a 100644
--- a/hott/Propositions.thy
+++ b/hott/Propositions.thy
@@ -5,8 +5,11 @@ imports
 
 begin
 
-definition isProp where "isProp A \<equiv> \<Prod>x y: A. x =\<^bsub>A\<^esub> y"
-definition isSet where "isSet A \<equiv> \<Prod>x y: A. \<Prod>p q: x =\<^bsub>A\<^esub> y. p =\<^bsub>x =\<^bsub>A\<^esub> y\<^esub> q"
+Definition isProp: ":= \<Prod>x y: A. x = y"
+  where "A: U i" by typechk
+
+Definition isSet: ":=\<Prod>x y: A. \<Prod>p q: x = y. p = q"
+  where "A: U i" by typechk
 
 Theorem isProp_Top: "isProp \<top>"
   unfolding isProp_def
@@ -16,4 +19,5 @@ Theorem isProp_Bot: "isProp \<bottom>"
   unfolding isProp_def
   by (intros, elim)
 
+
 end
diff --git a/hott/Univalence.thy b/hott/Univalence.thy
new file mode 100644
index 0000000..114577b
--- /dev/null
+++ b/hott/Univalence.thy
@@ -0,0 +1,35 @@
+theory Univalence
+imports Equivalence
+
+begin
+
+declare Ui_in_USi [form]
+
+Definition univalent_U: ":= \<Prod> A B: U i. \<Prod> p: A = B. is_biinv (idtoeqv p)"
+  by (typechk; rule U_lift)+
+
+axiomatization univalence where
+  univalence: "\<And>i. univalence i: univalent_U i"
+
+Lemma (def) idtoeqv_is_qinv:
+  assumes "A: U i" "B: U i" "p: A = B"
+  shows "is_qinv (idtoeqv p)"
+  by (rule is_qinv_if_is_biinv) (rule univalence[unfolded univalent_U_def])
+
+Definition ua: ":= fst (idtoeqv_is_qinv i A B p)"
+  where "A: U i" "B: U i" "p: A = B"
+  by typechk
+
+definition ua_i ("ua")
+  where [implicit]: "ua p \<equiv> Univalence.ua {} {} {} p"
+
+Definition ua_idtoeqv [folded ua_def]: ":= fst (snd (idtoeqv_is_qinv i A B p))"
+  where "A: U i" "B: U i" "p: A = B"
+  by typechk
+
+Definition idtoeqv_ua [folded ua_def]: ":= snd (snd (idtoeqv_is_qinv i A B p))"
+  where "A: U i" "B: U i" "p: A = B"
+  by typechk
+
+
+end