aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2021-06-24 22:40:05 +0100
committerJosh Chen2021-06-24 22:40:05 +0100
commitf988d541364841cd208f4fd21ff8e5e2935fc7aa (patch)
tree8ccc4d4e4cdde7572453ac0e250a224fe8db3da1 /hott
parent0085798a86a35e2430a97289e894724f688db435 (diff)
Bad practice huge commit:
1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
Diffstat (limited to 'hott')
-rw-r--r--hott/Equivalence.thy23
-rw-r--r--hott/Identity.thy6
-rw-r--r--hott/List_HoTT.thy4
-rw-r--r--hott/Propositions.thy8
-rw-r--r--hott/Univalence.thy35
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