diff options
Diffstat (limited to '')
| -rw-r--r-- | hott/Equivalence.thy | 23 | ||||
| -rw-r--r-- | hott/Identity.thy | 6 | ||||
| -rw-r--r-- | hott/List_HoTT.thy | 4 | ||||
| -rw-r--r-- | hott/Propositions.thy | 8 | ||||
| -rw-r--r-- | hott/Univalence.thy | 35 |
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 |