Mercurial > hg > Members > kono > Proof > category

comparison system-f.agda @ 783:bded2347efa4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCC by equation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Apr 2019 12:03:45 +0900
parents 6b4bd02efd80
children
comparison
equal deleted inserted replaced
782:db59b8f954aa 783:bded2347efa4
10 10
11 T : {l : Level} (X : Set l) → Bool X 11 T : {l : Level} (X : Set l) → Bool X
12 T X = λ(x y : X) → x 12 T X = λ(x y : X) → x
13 13
14 F : {l : Level} (X : Set l) → Bool X 14 F : {l : Level} (X : Set l) → Bool X
15
16
15 F X = λ(x y : X) → y 17 F X = λ(x y : X) → y
16 18
17 D : {l : Level} → {U : Set l} → U → U → Bool U → U 19 D : {l : Level} → {U : Set l} → U → U → Bool U → U
18 D u v t = t u v 20 D u v t = t u v
19 21
25 27
26 _×_ : {l : Level} → Set l → Set l → Set (suc l) 28 _×_ : {l : Level} → Set l → Set l → Set (suc l)
27 _×_ {l} U V = {X : Set l} → (U → V → X) → X 29 _×_ {l} U V = {X : Set l} → (U → V → X) → X
28 30
29 <_,_> : {l : Level} {U V : Set l} → U → V → (U × V) 31 <_,_> : {l : Level} {U V : Set l} → U → V → (U × V)
30 <_,_> {l} {U} {V} u v = λ X → λ(x : U → V → X) → x u v 32 <_,_> {l} {U} {V} u v = λ x → x u v
31 33
32 π1 : {l : Level} {U V : Set l} → (U × V) → U 34 π1 : {l : Level} {U V : Set l} → (U × V) → U
33 π1 {l} {U} {V} t = t {U} (λ(x : U) → λ(y : V) → x) 35 π1 {l} {U} {V} t = t {U} (λ(x : U) → λ(y : V) → x)
34 36
35 π2 : {l : Level} {U V : Set l} → (U × V) → V 37 π2 : {l : Level} {U V : Set l} → (U × V) → V
42 lemma07 = refl 44 lemma07 = refl
43 45
44 hoge : {l : Level} {U V : Set l} → U → V → (U × V) 46 hoge : {l : Level} {U V : Set l} → U → V → (U × V)
45 hoge u v = < u , v > 47 hoge u v = < u , v >
46 48
47 -- lemma08 : {l : Level} {U V : Set l } → {u : U } → (t : U × V) → < π1 t , π2 t > ≡ t 49 --lemma08 : {l : Level} {X U V : Set l } → {x : X } → {u : U } → (t : U × V) → < π1 t , π2 t > x ≡ t x
48 -- lemma08 t = refl 50 --lemma08 t = refl
49 51
50 -- Emp definision is still wrong... 52 -- Emp definision is still wrong...
51 53
52 --record Emp {l : Level } : Set (suc l) where 54 --record Emp {l : Level } : Set (suc l) where
53 -- field 55 -- field
60 --lemma103 u t = e1 t u 62 --lemma103 u t = e1 t u
61 63
62 Emp : {l : Level } → Set (suc l) 64 Emp : {l : Level } → Set (suc l)
63 Emp {l} = {X : Set l} → X 65 Emp {l} = {X : Set l} → X
64 66
65 -- ε : {l : Level} {U : Set l} → Emp {l} → U 67 ε : {l : Level} {U : Set l} → Emp {l} → U
66 -- ε {l} {U} t = t U 68 ε {l} {U} t = t {U}
67 69
68 -- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t 70 -- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t
69 -- lemma103 u t = refl 71 -- lemma103 u t = refl
70 72
71 -- lemma09 : {l : Level} {U : Set l} → (t : Emp ) → ε {l} {U} (ε {_} {Emp} t) ≡ ε {_} {U} t 73 -- lemma09 : {l : Level} {U : Set l} → (t : Emp ) → ε {l} {U} (ε {_} {Emp} t) ≡ ε {_} {U} t
86 88
87 _+_ : {l : Level} → Set l → Set l → Set (suc l) 89 _+_ : {l : Level} → Set l → Set l → Set (suc l)
88 _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X 90 _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X
89 91
90 ι1 : {l : Level } {U V : Set l} → U → U + V 92 ι1 : {l : Level } {U V : Set l} → U → U + V
91 ι1 {l} {U} {V} u = λ{X} → λ(x : U → X) → λ(y : V → X ) → x u 93 ι1 {l} {U} {V} u = λ x y → x u -- λ{X} → λ(x : U → X) → λ(y : V → X ) → x u
92 94
93 ι2 : {l : Level } {U V : Set l} → V → U + V 95 ι2 : {l : Level } {U V : Set l} → V → U + V
94 ι2 {l} {U} {V} v = λ{X} → λ(x : U → X) → λ(y : V → X ) → y v 96 ι2 {l} {U} {V} v = λ x y → y v --λ{X} → λ(x : U → X) → λ(y : V → X ) → y v
95 97
96 δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U 98 δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U
97 δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y) 99 δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y)
98 100
99 lemma11 : {l : Level} { U V R S : Set _ } → (u : R → U ) (v : S → U ) → (r : R) → δ {l} {U} {V} {R} {S} u v ( ι1 r ) ≡ u r 101 lemma11 : {l : Level} { U V R S : Set _ } → (u : R → U ) (v : S → U ) → (r : R) → δ {l} {U} {V} {R} {S} u v ( ι1 r ) ≡ u r
105 107
106 _××_ : {l : Level} → Set (suc l) → Set l → Set (suc l) 108 _××_ : {l : Level} → Set (suc l) → Set l → Set (suc l)
107 _××_ {l} U V = {X : Set l} → (U → V → X) → X 109 _××_ {l} U V = {X : Set l} → (U → V → X) → X
108 110
109 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U ×× V) 111 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U ×× V)
110 <<_,_>> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v 112 <<_,_>> {l} {U} {V} u v = λ x → x u v -- λ{X} → λ(x : U → V → X) → x u v
111 113
112 114
113 Int : {l : Level } ( X : Set l ) → Set l 115 Int : {l : Level } ( X : Set l ) → Set l
114 Int X = X → ( X → X ) → X 116 Int X = X → ( X → X ) → X
115 117
140 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U 142 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U
141 It u f t = t u f 143 It u f t = t u f
142 144
143 ItInt : {l : Level} {X : Set l} → Int X → (X → Int X ) → ( Int X → Int X ) → Int X → Int X 145 ItInt : {l : Level} {X : Set l} → Int X → (X → Int X ) → ( Int X → Int X ) → Int X → Int X
144 ItInt {l} {X} u g f t = λ z s → t (u z s) ( λ (w : X) → (f (g w)) z s ) 146 ItInt {l} {X} u g f t = λ z s → t (u z s) ( λ (w : X) → (f (g w)) z s )
147
148 copy_int : {l l' : Level } { X X' : Set l } → Int (X → (X → X) → X) → Int X
149 copy_int {_} {_} {X} {X'} x = It Zero S x
145 150
146 R : {l : Level} { U X : Set l} → U → ( U → Int X → U ) → Int _ → U 151 R : {l : Level} { U X : Set l} → U → ( U → Int X → U ) → Int _ → U
147 R {l} {U} {X} u v t = π1 ( It {suc l} {U × Int X} (< u , Zero >) (λ (x : U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) 152 R {l} {U} {X} u v t = π1 ( It {suc l} {U × Int X} (< u , Zero >) (λ (x : U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t )
148 153
149 -- bad adder which modifies input type 154 -- bad adder which modifies input type
157 add'' x y = ItInt y (\w z s -> w )S x 162 add'' x y = ItInt y (\w z s -> w )S x
158 163
159 lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y ≡ add'' x y 164 lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y ≡ add'' x y
160 lemma22 x y = refl 165 lemma22 x y = refl
161 166
167 lemma21 : {l : Level} {X : Set l} ( x y : Int X ) → add x Zero ≡ x
168 lemma21 x y = refl
169
170 postulate extensionality : {l : Level } → Relation.Binary.PropositionalEquality.Extensionality l l
171
172 --lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x (S y) ≡ S ( add x y )
173 --lemma23 x y = extensionality ( λ z → {!!} )
174 -- where
175 -- lemma24 : {!!}
176 -- lemma24 = {!!}
177
178 -- lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x y ≡ add y x
179 -- lemma23 x y = {!!}
180
162 -- bad adder which modifies input type 181 -- bad adder which modifies input type
163 mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X 182 mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
164 mul' {l} {X} x y = It Zero (add x) y 183 mul' {l} {X} x y = It Zero (add x) y
165 184
166 mul : {l : Level } {X : Set l} → Int X → Int X → Int X 185 mul : {l : Level } {X : Set l} → Int X → Int X → Int X
181 lemma24 : {l : Level } {X : Set l} → mul {l} {X} n4 n3 ≡ mul'' {l} {X} n3 n4 200 lemma24 : {l : Level } {X : Set l} → mul {l} {X} n4 n3 ≡ mul'' {l} {X} n3 n4
182 lemma24 = refl 201 lemma24 = refl
183 202
184 203
185 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y ≡ mul y x 204 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y ≡ mul y x
186 -- lemma14 x y = It {!!} {!!} {!!} 205 -- lemma14 x y = {!!} -- It {!!} {!!} {!!}
187 206
188 lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2 207 lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2
189 lemma15 x y = refl 208 lemma15 x y = refl
190 209
191 lemma15' : {l : Level} {X : Set l} (x y : Int X) → mul'' {l} {X} n2 n3 ≡ mul'' {l} {X} n3 n2 210 lemma15' : {l : Level} {X : Set l} (x y : Int X) → mul'' {l} {X} n2 n3 ≡ mul'' {l} {X} n3 n2