From 7a5897039287ddc1d9a0efcb84a7732f2acdd8fd Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 1 Mar 2019 00:45:40 +0100 Subject: Working on univalence --- Univalence.thy | 161 ++++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 115 insertions(+), 46 deletions(-) diff --git a/Univalence.thy b/Univalence.thy index c6733c6..e073e50 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -1,72 +1,141 @@ -(* -Title: Univalence.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Univalence +Feb 2019 -Definitions of homotopy, equivalence and the univalence axiom. -*) +********) theory Univalence -imports HoTT_Methods Equality Prod Sum +imports HoTT_Methods Prod Sum Eq begin -section \Homotopy and equivalence\ - -definition homotopic :: "[t, tf, t, t] \ t" where "homotopic A B f g \ \x:A. (f`x) =[B x] (g`x)" +section \Homotopy\ -syntax "_homotopic" :: "[t, idt, t, t, t] \ t" ("(1_ ~[_:_. _]/ _)" [101, 0, 0, 0, 101] 100) -translations "f ~[x:A. B] g" \ "CONST homotopic A (\x. B) f g" +definition homotopic :: "[t, t \ t, t, t] \ t" ("(2homotopic[_, _] _ _)" [0, 0, 1000, 1000]) +where "homotopic[A, B] f g \ \x: A. f`x =[B x] g`x" declare homotopic_def [comp] -definition isequiv :: "[t, t, t] \ t" ("(3isequiv[_, _]/ _)") where - "isequiv[A, B] f \ (\g: B \ A. g \ f ~[x:A. A] id) \ (\g: B \ A. f \ g ~[x:B. B] id)" +syntax "_homotopic" :: "[t, idt, t, t, t] \ t" ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100) +translations "f ~[x: A. B] g" \ "(CONST homotopic) A (\x. B) f g" + +syntax "_homotopic'" :: "[t, t] \ t" ("(2_ ~ _)" [1000, 1000]) + +ML \val pretty_homotopic = Attrib.setup_config_bool @{binding "pretty_homotopic"} (K true)\ + +print_translation \ +let fun homotopic_tr' ctxt [A, B, f, g] = + if Config.get ctxt pretty_homotopic + then Syntax.const @{syntax_const "_homotopic'"} $ f $ g + else @{const homotopic} $ A $ B $ f $ g +in + [(@{const_syntax homotopic}, homotopic_tr')] +end +\ + +lemma homotopic_type: + assumes [intro]: "A: U i" "B: A \ U i" "f: \x: A. B x" "g: \x: A. B x" + shows "f ~[x: A. B x] g: U i" +by derive + +declare homotopic_type [intro] + +schematic_goal fun_eq_imp_homotopic: + assumes [intro]: + "A: U i" "B: A \ U i" + "f: \x: A. B x" "g: \x: A. B x" + "p: f =[\x: A. B x] g" + shows "?prf: f ~[x: A. B x] g" +proof (path_ind' f g p) + show "\f. f : \(x: A). B x \ \x: A. refl(f`x): f ~[x: A. B x] f" by derive +qed routine + +definition happly :: "[t, t \ t, t, t, t] \ t" ("(2happly[_, _] _ _ _)" [0, 0, 1000, 1000, 1000]) +where "happly[A, B] f g p \ indEq (\f g. & f ~[x: A. B x] g) (\f. \(x: A). refl(f`x)) f g p" + +corollary happly_type: + assumes [intro]: + "A: U i" "B: A \ U i" + "f: \x: A. B x" "g: \x: A. B x" + "p: f =[\x: A. B x] g" + shows "happly[A, B] f g p: f ~[x: A. B x] g" +unfolding happly_def by (derive lems: fun_eq_imp_homotopic) + + +section \Equivalence\ + +text \For now, we define equivalence in terms of bi-invertibility.\ + +definition biinv :: "[t, t, t] \ t" ("(2biinv[_, _]/ _)") +where "biinv[A, B] f \ + (\g: B \ A. g o[A] f ~[x:A. A] id A) \ (\g: B \ A. f o[B] g ~[x: B. B] id B)" text \ The meanings of the syntax defined above are: -\<^item> @{term "f ~[x:A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "\x:A. B x"}. -\<^item> @{term "isequiv[A, B] f"} expresses that the non-dependent function @{term f} of type @{term "A \ B"} is an equivalence. +\<^item> @{term "f ~[x: A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "\x:A. B x"}. +\<^item> @{term "biinv[A, B] f"} expresses that the function @{term f} of type @{term "A \ B"} is bi-invertible. \ -definition equivalence :: "[t, t] \ t" (infix "\" 100) - where "A \ B \ \f: A \ B. isequiv[A, B] f" +lemma biinv_type: + assumes [intro]: "A: U i" "B: U i" "f: A \ B" + shows "biinv[A, B] f: U i" +unfolding biinv_def by derive -lemma id_isequiv: - assumes "A: U i" "id: A \ A" - shows "<\x. refl x>, \x. refl x>>: isequiv[A, A] id" -unfolding isequiv_def proof (routine add: assms) - show "\g. g: A \ A \ id \ g ~[x:A. A] id: U i" by (derive lems: assms) - show "\x. refl x>: \g:A \ A. (g \ id) ~[x:A. A] id" by (derive lems: assms) - show "\x. refl x>: \g:A \ A. (id \ g) ~[x:A. A] id" by (derive lems: assms) -qed +declare biinv_type [intro] -lemma equivalence_symm: - assumes "A: U i" and "id: A \ A" - shows "\x. refl x>, \x. refl x>>>: A \ A" -unfolding equivalence_def proof - show "\f. f: A \ A \ isequiv[A, A] f: U i" by (derive lems: assms isequiv_def) - show "<\x. refl x>, \x. refl x>>: isequiv[A, A] id" using assms by (rule id_isequiv) -qed fact +schematic_goal id_is_biinv: + assumes [intro]: "A: U i" + shows "?prf: biinv[A, A] (id A)" +unfolding biinv_def proof (rule Sum_routine, compute) + show "x: A. refl x>: \(g: A \ A). (g o[A] id A) ~[x: A. A] (id A)" by derive + show "x: A. refl x>: \(g: A \ A). (id A o[A] g) ~[x: A. A] (id A)" by derive +qed routine +definition equivalence :: "[t, t] \ t" (infix "\" 100) +where "A \ B \ \f: A \ B. biinv[A, B] f" + +schematic_goal equivalence_symmetric: + assumes [intro]: "A: U i" + shows "?prf: A \ A" +unfolding equivalence_def proof (rule Sum_routine) + show "\f. f : A \ A \ biinv[A, A] f : U i" unfolding biinv_def by derive + show "id A: A \ A" by routine +qed (routine add: id_is_biinv) -section \idtoeqv\ -definition idtoeqv :: t where "idtoeqv \ \<^bold>\p. = (\_. <\x. refl x>, \x. refl x>>) p>" +section \Univalence\ -text \We prove that equal types are equivalent. The proof involves universe types.\ +(* +schematic_goal + assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B" + shows "?prf: biinv[A, B] (transport[id(U i), A, B] p)" +unfolding biinv_def +apply (rule Sum_routine) defer +apply (rule Sum_intro) + have + "transport[id(U i), A, B] p: (id (U i))`A \ (id (U i))`B" + by (derive lems: transport_type[where ?A="U i"] + moreover have + "(id (U i))`A \ (id (U i))`B \ A \ B" by deriv + ultimately have [intro]: + "transport[id(U i), A, B] p: A \ B" by simp + + show "\g: B \ A. (transport[id(U i), A, B] p o[B] g) ~[x: B. B] (id B) : U i" + by deriv + -theorem - assumes "A: U i" and "B: U i" - shows "idtoeqv: (A =[U i] B) \ A \ B" -unfolding idtoeqv_def equivalence_def proof (routine add: assms) +schematic_goal type_eq_imp_equiv: + assumes [intro]: "A: U i" "B: U i" + shows "?prf: (A =[U i] B) \ A \ B" +unfolding equivalence_def +apply (rule Prod_routine, rule Sum_routine) +prefer 2 show *: "\f. f: A \ B \ isequiv[A, B] f: U i" - unfolding isequiv_def by (derive lems: assms) + unfolding isequiv_def by (derive lems: assms show "\p. p: A =[U i] B \ transport p: A \ B" - by (derive lems: assms transport_type[where ?i="Suc i"]) - \ \Instantiate @{thm transport_type} with a suitable universe level here...\ + by (derive lems: assms transport_type[where ?i="Suc i"] \ \Instantiate @{thm transport_type} with a suitable universe level here...\ show "\p. p: A =[U i] B \ ind\<^sub>= (\_. <\x. refl x>, \x. refl x>>) p: isequiv[A, B] (transport p)" proof (elim Equal_elim) @@ -75,14 +144,14 @@ unfolding idtoeqv_def equivalence_def proof (routine add: assms) \ \...and also here.\ show "\A B p. \A: U i; B: U i; p: A =[U i] B\ \ isequiv[A, B] (transport p): U i" - unfolding isequiv_def by (derive lems: assms transport_type) + unfolding isequiv_def by (derive lems: assms transport_type qed fact+ -qed (derive lems: assms) +qed (derive lems: assms section \The univalence axiom\ axiomatization univalence :: "[t, t] \ t" where UA: "univalence A B: isequiv[A, B] idtoeqv" - +*) end -- cgit v1.2.3