diff options
author | Josh Chen | 2019-03-06 11:42:19 +0100 |
---|---|---|
committer | Josh Chen | 2019-03-06 11:42:19 +0100 |
commit | 8f7164976d08446e77a0e1eceaaa01f0ed363e5b (patch) | |
tree | 6cbf9e5963e0273e75b12436cf5b3adc2c30b05c /Univalence.thy | |
parent | fa4c19c5ddce4d1f2d5ad58170e89cb74cb7f7e1 (diff) |
Make functions object-level
Diffstat (limited to '')
-rw-r--r-- | Univalence.thy | 36 |
1 files changed, 15 insertions, 21 deletions
diff --git a/Univalence.thy b/Univalence.thy index 30110f1..322dbbd 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -117,22 +117,16 @@ schematic_goal transport_invl_hom: "P: A \<leadsto> U j" "A: U i" "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 + (transport[A, P, y, x]`(inv[A, x, y]`p)) o[P x] (transport[A, P, x, y]`p) ~[w: P x. P x] id P x" +by (rule happly_type[OF transport_invl], derive) schematic_goal transport_invr_hom: assumes [intro]: - "P: A \<leadsto> U j" "A: U i" - "x: A" "y: A" "p: x =[A] y" + "A: U i" "P: A \<leadsto> U j" + "y: A" "x: 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 + (transport[A, P, x, y]`p) o[P y] (transport[A, P, y, x]`(inv[A, x, y]`p)) ~[w: P y. P y] id P y" +by (rule happly_type[OF transport_invr], derive) declare transport_invl_hom [intro] @@ -145,7 +139,7 @@ It is used in the derivation of @{text idtoeqv} in the next section. schematic_goal transport_biinv: assumes [intro]: "p: A =[U i] B" "A: U i" "B: U i" - shows "?prf: biinv[A, B] (transport[Id, A, B] p)" + shows "?prf: biinv[A, B] (transport[U i, Id, A, B]`p)" unfolding biinv_def apply (rule Sum_routine) prefer 2 @@ -173,25 +167,25 @@ done *) definition idtoeqv :: "[ord, t, t] \<Rightarrow> t" ("(2idtoeqv[_, _, _])") where " idtoeqv[i, A, B] \<equiv> - \<lambda>(p: A =[U i] B). - < transport (Id) A B p, < - < transport[Id, B, A] (inv[U i, A, B] p), + \<lambda>p: A =[U i] B. + < transport[U i, Id, A, B]`p, < + < transport[U i, Id, B, A]`(inv[U i, A, B]`p), happly[x: A. A] - ((transport[Id, B, A] (inv[U i, A, B] p)) o[A] transport[Id, A, B] p) + ((transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p) (id A) (indEq (\<lambda>A B p. - (transport[Id, B, A] (inv[U i, A, B] p)) o[A] transport[Id, A, B] p + (transport[U i, Id, B, A]`(inv[U i, A, B]`p)) o[A] transport[U i, Id, A, B]`p =[A \<rightarrow> A] id A) (\<lambda>x. refl (id x)) A B p) >, - < transport (Id) B A (inv[U i, A, B] p), + < transport[U i, Id, B, A]`(inv[U i, A, B]`p), happly[x: B. B] - ((transport[Id, A, B] p) o[B] (transport[Id, B, A] (inv[U i, A, B] p))) + ((transport[U i, Id, A, B]`p) o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p))) (id B) (indEq (\<lambda>A B p. - transport[Id, A, B] p o[B] (transport[Id, B, A] (inv[U i, A, B] p)) + transport[U i, Id, A, B]`p o[B] (transport[U i, Id, B, A]`(inv[U i, A, B]`p)) =[B \<rightarrow> B] id B) (\<lambda>x. refl (id x)) A B p) > |