diff options
| -rw-r--r-- | Eq.thy | 100 |
1 files changed, 1 insertions, 99 deletions
@@ -7,7 +7,7 @@ Intensional equality, path induction, and proofs of various results. ********) theory Eq -imports Prod HoTT_Methods +imports HoTT_Methods Prod begin @@ -243,10 +243,6 @@ proof - by derive qed routine -(* Todo, if possible: - Implement a custom version of schematic_goal/theorem that exports the derived proof term. -*) - section \<open>Functoriality of functions on types under equality\<close> @@ -376,98 +372,4 @@ proof (path_ind' x y p) qed -section \<open>Transport\<close> - -schematic_goal transport: - assumes [intro]: - "P: A \<rightarrow> U j" "A: U i" - "x: A" "y: A" "p: x =[A] y" - shows "?prf: P`x \<rightarrow> P`y" -proof (path_ind' x y p) - show "\<And>x. x: A \<Longrightarrow> id P`x: P`x \<rightarrow> P`x" by derive -qed routine - -definition transport :: "[t, t, t, t] \<Rightarrow> t" ("(2transport[_, _, _] _)" [0, 0, 0, 1000]) -where "transport[P, x, y] p \<equiv> indEq (\<lambda>a b. & (P`a \<rightarrow> P`b)) (\<lambda>x. id P`x) x y p" - -syntax "_transport'" :: "[t, t] \<Rightarrow> t" ("(2_*)" [1000]) - -ML \<open>val pretty_transport = Attrib.setup_config_bool @{binding "pretty_transport"} (K true)\<close> - -print_translation \<open> -let fun transport_tr' ctxt [P, x, y, p] = - if Config.get ctxt pretty_transport - then Syntax.const @{syntax_const "_transport'"} $ p - else @{const transport} $ P $ x $ y $ p -in - [(@{const_syntax transport}, transport_tr')] -end -\<close> - -corollary transport_type: - assumes "P: A \<rightarrow> U j" "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "transport[P, x, y] p: P`x \<rightarrow> P`y" -unfolding transport_def using assms by (rule transport) - -lemma transport_comp: - assumes [intro]: "A: U i" "P: A \<rightarrow> U j" "a: A" - shows "transport P a a (refl a) \<equiv> id P`a" -unfolding transport_def by derive - -declare - transport_type [intro] - transport_comp [comp] - -schematic_goal transport_invl: - 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) =[P`x \<rightarrow> P`x] id P`x" -proof (path_ind' x y p) - fix x assume [intro]: "x: A" - show - "refl (id P`x) : - transport[P, x, x] (inv[A, x, x] (refl x)) o[P`x] (transport[P, x, x] (refl x)) =[P`x \<rightarrow> P`x] - id P`x" - by derive - - fix y p assume [intro]: "y: A" "p: x =[A] y" - have [intro]: - "transport[P, y, x] (inv[A, x, y] p) o[P`x] transport[P, x, y] p : P`x \<rightarrow> P`x" - proof show "transport[P, x, y] p: P`x \<rightarrow> P`y" by routine qed routine - - show - "transport[P, y, x] (inv[A, x, y] p) o[P`x] transport[P, x, y] p =[P`x \<rightarrow> P`x] id P`x: U j" - by derive -qed - -schematic_goal transport_invr: - 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)) =[P`y \<rightarrow> P`y] id P`y" -proof (path_ind' x y p) - fix x assume [intro]: "x: A" - show - "refl (id P`x) : - (transport[P, x, x] (refl x)) o[P`x] transport[P, x, x] (inv[A, x, x] (refl x)) =[P`x \<rightarrow> P`x] - id P`x" - by derive - - fix y p assume [intro]: "y: A" "p: x =[A] y" - have [intro]: - "transport[P, x, y] p o[P`y] transport[P, y, x] (inv[A, x, y] p): P`y \<rightarrow> P`y" - proof show "transport[P, x, y] p: P`x \<rightarrow> P`y" by routine qed routine - - show - "transport[P, x, y] p o[P`y] transport[P, y, x] (inv[A, x, y] p) =[P`y \<rightarrow> P`y] id P`y: U j" - by derive -qed - -declare - transport_invl [intro] - transport_invr [intro] - end |