diff options
author | Josh Chen | 2018-06-07 19:35:32 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-07 19:35:32 +0200 |
commit | fc19fe90e7cb13acc03deaf061b2b6cf3df2d165 (patch) | |
tree | ff229e0d5b5ddf784a549d38582d49dbcca51a29 /HoTT_Theorems.thy | |
parent | d09095bec2c136f600edd0039a1cc1eae441d823 (diff) |
Nondependent function arrow should bind tighter than the Pi former, but looser than equality.
Diffstat (limited to 'HoTT_Theorems.thy')
-rw-r--r-- | HoTT_Theorems.thy | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 52e1b32..5578bf8 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -57,11 +57,11 @@ proposition wellformed_currying: "B: A \<rightarrow> U" and "\<And>x::Term. C(x): B(x) \<rightarrow> U" shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U" -proof (rule Prod_formation) +proof fix x::Term assume *: "x : A" show "\<Prod>y:B(x). C x y : U" - proof (rule Prod_formation) + proof show "B(x) : U" using * by (rule assms) qed (rule assms) qed (rule assms) @@ -78,15 +78,15 @@ proposition triply_curried: "\<And>x y::Term. y : B(x) \<Longrightarrow> C(x)(y) : U" and "\<And>x y z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U" -proof (rule Prod_formation) +proof fix x::Term assume 1: "x : A" show "\<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U" - proof (rule Prod_formation) + proof show "B(x) : U" using 1 by (rule assms) fix y::Term assume 2: "y : B(x)" show "\<Prod>z:C(x)(y). D(x)(y)(z) : U" - proof (rule Prod_formation) + proof show "C x y : U" using 2 by (rule assms) show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms) qed |