diff options
| -rw-r--r-- | Prod.thy | 2 | ||||
| -rw-r--r-- | Univalence.thy | 101 |
2 files changed, 81 insertions, 22 deletions
@@ -24,8 +24,8 @@ syntax "_lam" :: "[idt, t, t] \<Rightarrow> t" ("(2\<lambda>'(_: _')./ _)" 30) "_lam'" :: "[idt, t, t] \<Rightarrow> t" ("(2\<lambda>_: _./ _)" 30) translations - "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" "\<Prod>x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" + "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" "\<lambda>(x: A). b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)" "\<lambda>x: A. b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)" diff --git a/Univalence.thy b/Univalence.thy index e073e50..04e1d67 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -20,6 +20,7 @@ declare homotopic_def [comp] syntax "_homotopic" :: "[t, idt, t, t, t] \<Rightarrow> t" ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100) translations "f ~[x: A. B] g" \<rightleftharpoons> "(CONST homotopic) A (\<lambda>x. B) f g" +(* syntax "_homotopic'" :: "[t, t] \<Rightarrow> t" ("(2_ ~ _)" [1000, 1000]) ML \<open>val pretty_homotopic = Attrib.setup_config_bool @{binding "pretty_homotopic"} (K true)\<close> @@ -33,6 +34,7 @@ in [(@{const_syntax homotopic}, homotopic_tr')] end \<close> +*) lemma homotopic_type: assumes [intro]: "A: U i" "B: A \<leadsto> U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" @@ -43,26 +45,59 @@ declare homotopic_type [intro] schematic_goal fun_eq_imp_homotopic: assumes [intro]: - "A: U i" "B: A \<leadsto> U i" - "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" "p: f =[\<Prod>x: A. B x] g" + "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" + "A: U i" "B: A \<leadsto> U i" shows "?prf: f ~[x: A. B x] g" proof (path_ind' f g p) show "\<And>f. f : \<Prod>(x: A). B x \<Longrightarrow> \<lambda>x: A. refl(f`x): f ~[x: A. B x] f" by derive qed routine -definition happly :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" ("(2happly[_, _] _ _ _)" [0, 0, 1000, 1000, 1000]) -where "happly[A, B] f g p \<equiv> indEq (\<lambda>f g. & f ~[x: A. B x] g) (\<lambda>f. \<lambda>(x: A). refl(f`x)) f g p" +definition happly :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" +where "happly A B f g p \<equiv> indEq (\<lambda>f g. & f ~[x: A. B x] g) (\<lambda>f. \<lambda>(x: A). refl(f`x)) f g p" + +syntax "_happly" :: "[idt, t, t, t, t, t] \<Rightarrow> t" + ("(2happly[_: _. _] _ _ _)" [0, 0, 0, 1000, 1000, 1000]) +translations "happly[x: A. B] f g p" \<rightleftharpoons> "(CONST happly) A (\<lambda>x. B) f g p" corollary happly_type: assumes [intro]: - "A: U i" "B: A \<leadsto> U i" - "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" "p: f =[\<Prod>x: A. B x] g" - shows "happly[A, B] f g p: f ~[x: A. B x] g" + "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" + "A: U i" "B: A \<leadsto> U i" + shows "happly[x: A. B x] f g p: f ~[x: A. B x] g" unfolding happly_def by (derive lems: fun_eq_imp_homotopic) +section \<open>Transport and homotopy\<close> + +schematic_goal transport_invl_hom: + assumes [intro]: + "A: U i" "P: A \<rightarrow> U j" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: + (transport[P, y, x] (inv[A, x, y] p)) o[P`x] (transport[P, x, y] p) ~[w: P`x. P`x] id(P`x)" +proof (rule happly_type[OF transport_invl]) + show "(transport[P, y, x] (inv[A, x, y] p)) o[P`x] (transport[P, x, y] p): P`x \<rightarrow> P`x" + proof show "P`y: U j" by routine qed routine +qed routine + +schematic_goal transport_invr_hom: + assumes [intro]: + "A: U i" "P: A \<rightarrow> U j" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: + (transport[P, x, y] p) o[P`y] (transport[P, y, x] (inv[A, x, y] p)) ~[w: P`y. P`y] id(P`y)" +proof (rule happly_type[OF transport_invr]) + show "(transport[P, x, y] p) o[P`y] (transport[P, y, x] (inv[A, x, y] p)): P`y \<rightarrow> P`y" + proof show "P`x: U j" by routine qed routine +qed routine + +declare + transport_invl_hom [intro] + transport_invr_hom [intro] + + section \<open>Equivalence\<close> text \<open>For now, we define equivalence in terms of bi-invertibility.\<close> @@ -106,23 +141,47 @@ qed (routine add: id_is_biinv) section \<open>Univalence\<close> -(* +declare[[goals_limit=100, pretty_transport=true]] + +lemma lem: "\<And>A. A: U i \<Longrightarrow> (id (U i))`A \<equiv> A" by derive + 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)" +apply (path_ind' A B p) +apply (unfold biinv_def) + show "?a : biinv[A, B] (transport[id(U i), A, B] p)" + +oops + +schematic_goal + assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B" + shows "?prf: biinv[id(U i)`A, id(U i)`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 \<rightarrow> (id (U i))`B" - by (derive lems: transport_type[where ?A="U i"] - moreover have - "(id (U i))`A \<rightarrow> (id (U i))`B \<equiv> A \<rightarrow> B" by deriv - ultimately have [intro]: - "transport[id(U i), A, B] p: A \<rightarrow> B" by simp - - show "\<Sum>g: B \<rightarrow> A. (transport[id(U i), A, B] p o[B] g) ~[x: B. B] (id B) : U i" - by deriv +apply (rule Sum_routine) +prefer 2 apply (rule Sum_routine) +prefer 3 apply (rule transport_invl_hom) +prefer 9 apply (rule Sum_routine) +prefer 3 apply (rule transport_invr_hom) +proof - + show "U i: U (Suc i)" by hierarchy + show "U i: U (Suc i)" by hierarchy + show "\<And>g. g : id (U i)`B \<rightarrow> id (U i)`A \<Longrightarrow> (transport[id(U i), A, B] p) o[id (U i)`B] g ~[x: id (U i)`B. id (U i)`B] id (id (U i)`B) : U i" + proof + show "id (U i)`B : U i" by derive + show "id (U i)`B : U i" by derive + show "id (id (U i)`B) : id (U i)`B \<rightarrow> id (U i)`B" by derive + show + "\<And>g. g : id (U i)`B \<rightarrow> id (U i)`A \<Longrightarrow> + (transport[id(U i), A, B] p) o[id (U i)`B] g: id (U i)`B \<rightarrow> id (U i)`B" + apply rule + prefer 4 apply assumption + proof - + show "id (U i)`B : U i" by derive + show "id (U i)`A : U i" by derive + show "id (U i)`B : U i" by derive + +oops schematic_goal type_eq_imp_equiv: @@ -148,7 +207,7 @@ prefer 2 qed fact+ qed (derive lems: assms - +(* section \<open>The univalence axiom\<close> axiomatization univalence :: "[t, t] \<Rightarrow> t" where UA: "univalence A B: isequiv[A, B] idtoeqv" |