diff options
author | Josh Chen | 2021-06-24 22:40:05 +0100 |
---|---|---|
committer | Josh Chen | 2021-06-24 22:40:05 +0100 |
commit | f988d541364841cd208f4fd21ff8e5e2935fc7aa (patch) | |
tree | 8ccc4d4e4cdde7572453ac0e250a224fe8db3da1 /hott/Univalence.thy | |
parent | 0085798a86a35e2430a97289e894724f688db435 (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 '')
-rw-r--r-- | hott/Univalence.thy | 35 |
1 files changed, 35 insertions, 0 deletions
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 |