diff options
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 |