Mercurial > hg > Members > kono > Proof > category
annotate system-f.agda @ 787:ca5eba647990
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 18 Apr 2019 20:07:22 +0900 |
| parents | bded2347efa4 |
| children |
| rev | line source |
|---|---|
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
1 {-# OPTIONS --universe-polymorphism #-} |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
2 |
| 315 | 3 open import Level |
| 4 open import Relation.Binary.PropositionalEquality | |
| 5 | |
| 330 | 6 module system-f where |
| 315 | 7 |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
8 Bool : {l : Level} → Set l → Set l |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
9 Bool {l} = λ(X : Set l) → X → X → X |
| 315 | 10 |
| 336 | 11 T : {l : Level} (X : Set l) → Bool X |
| 12 T X = λ(x y : X) → x | |
| 315 | 13 |
| 336 | 14 F : {l : Level} (X : Set l) → Bool X |
| 783 | 15 |
| 16 | |
| 336 | 17 F X = λ(x y : X) → y |
| 315 | 18 |
| 336 | 19 D : {l : Level} → {U : Set l} → U → U → Bool U → U |
| 331 | 20 D u v t = t u v |
| 315 | 21 |
| 336 | 22 lemma04 : {l : Level} { U : Set l} {u v : U} → D {_} {U} u v (T U ) ≡ u |
| 315 | 23 lemma04 = refl |
| 24 | |
| 336 | 25 lemma05 : {l : Level} { U : Set l} {u v : U} → D {_} {U} u v (F U ) ≡ v |
| 315 | 26 lemma05 = refl |
| 27 | |
| 336 | 28 _×_ : {l : Level} → Set l → Set l → Set (suc l) |
| 29 _×_ {l} U V = {X : Set l} → (U → V → X) → X | |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
30 |
| 336 | 31 <_,_> : {l : Level} {U V : Set l} → U → V → (U × V) |
| 783 | 32 <_,_> {l} {U} {V} u v = λ x → x u v |
| 315 | 33 |
| 336 | 34 π1 : {l : Level} {U V : Set l} → (U × V) → U |
| 35 π1 {l} {U} {V} t = t {U} (λ(x : U) → λ(y : V) → x) | |
| 315 | 36 |
| 336 | 37 π2 : {l : Level} {U V : Set l} → (U × V) → V |
| 38 π2 {l} {U} {V} t = t {V} (λ(x : U) → λ(y : V) → y) | |
| 315 | 39 |
| 336 | 40 lemma06 : {l : Level} {U V : Set l } → {u : U } → {v : V} → π1 ( < u , v > ) ≡ u |
| 315 | 41 lemma06 = refl |
| 42 | |
| 336 | 43 lemma07 : {l : Level} {U V : Set l } → {u : U } → {v : V} → π2 ( < u , v > ) ≡ v |
| 315 | 44 lemma07 = refl |
| 45 | |
| 336 | 46 hoge : {l : Level} {U V : Set l} → U → V → (U × V) |
| 315 | 47 hoge u v = < u , v > |
| 48 | |
| 783 | 49 --lemma08 : {l : Level} {X U V : Set l } → {x : X } → {u : U } → (t : U × V) → < π1 t , π2 t > x ≡ t x |
| 50 --lemma08 t = refl | |
| 316 | 51 |
| 52 -- Emp definision is still wrong... | |
| 53 | |
| 349 | 54 --record Emp {l : Level } : Set (suc l) where |
| 55 -- field | |
| 56 -- ε : (U : Set l ) → U | |
| 57 -- e1 : {U V : Set l} → (u : U) → (ε (U → V) ) u ≡ ε V | |
| 58 -- | |
| 59 --open Emp | |
| 60 | |
| 61 --lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε t (U → V) ) u ≡ ε t V | |
| 62 --lemma103 u t = e1 t u | |
| 63 | |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
64 Emp : {l : Level } → Set (suc l) |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
65 Emp {l} = {X : Set l} → X |
| 348 | 66 |
| 783 | 67 ε : {l : Level} {U : Set l} → Emp {l} → U |
| 68 ε {l} {U} t = t {U} | |
| 316 | 69 |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
70 -- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t |
| 348 | 71 -- lemma103 u t = refl |
| 72 | |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
73 -- lemma09 : {l : Level} {U : Set l} → (t : Emp ) → ε {l} {U} (ε {_} {Emp} t) ≡ ε {_} {U} t |
| 322 | 74 -- lemma09 t = refl |
| 321 | 75 |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
76 -- lemma10 : {l : Level} {U V X : Set l} → (t : Emp ) → U × V |
|
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
77 -- lemma10 {l} {U} {V} t = ε {suc l} {U × V} t |
| 327 | 78 |
| 348 | 79 -- lemma100 : {l : Level} {U V X : Set l} → (t : Emp ) → Emp |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
80 -- lemma100 {l} {U} {V} t = ε {_} {U} t |
| 321 | 81 |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
82 -- lemma101 : {l : Level} {U V : Set l} → (t : Emp ) → π1 (ε {suc l} {U × V} t) ≡ ε {l} {U} t |
| 322 | 83 -- lemma101 t = refl |
| 319 | 84 |
|
350
c483374f542b
try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
349
diff
changeset
|
85 -- lemma102 : {l : Level} {U V : Set l} → (t : Emp ) → π2 (ε {_} {U × V} t) ≡ ε {_} {V} t |
| 322 | 86 -- lemma102 t = refl |
| 321 | 87 |
| 316 | 88 |
| 336 | 89 _+_ : {l : Level} → Set l → Set l → Set (suc l) |
| 90 _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X | |
| 316 | 91 |
| 336 | 92 ι1 : {l : Level } {U V : Set l} → U → U + V |
| 783 | 93 ι1 {l} {U} {V} u = λ x y → x u -- λ{X} → λ(x : U → X) → λ(y : V → X ) → x u |
| 316 | 94 |
| 336 | 95 ι2 : {l : Level } {U V : Set l} → V → U + V |
| 783 | 96 ι2 {l} {U} {V} v = λ x y → y v --λ{X} → λ(x : U → X) → λ(y : V → X ) → y v |
| 316 | 97 |
| 336 | 98 δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U |
| 99 δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y) | |
| 316 | 100 |
| 336 | 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 |
| 316 | 102 lemma11 u v r = refl |
| 103 | |
| 336 | 104 lemma12 : {l : Level} { U V R S : Set _ } → (u : R → U ) (v : S → U ) → (s : S) → δ {l} {U} {V} {R} {S} u v ( ι2 s ) ≡ v s |
| 316 | 105 lemma12 u v s = refl |
| 106 | |
| 107 | |
| 336 | 108 _××_ : {l : Level} → Set (suc l) → Set l → Set (suc l) |
| 109 _××_ {l} U V = {X : Set l} → (U → V → X) → X | |
| 322 | 110 |
| 336 | 111 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U ×× V) |
| 783 | 112 <<_,_>> {l} {U} {V} u v = λ x → x u v -- λ{X} → λ(x : U → V → X) → x u v |
| 316 | 113 |
| 114 | |
| 336 | 115 Int : {l : Level } ( X : Set l ) → Set l |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
116 Int X = X → ( X → X ) → X |
| 322 | 117 |
| 336 | 118 Zero : {l : Level } → { X : Set l } → Int X |
| 119 Zero {l} {X} = λ(x : X ) → λ(y : X → X ) → x | |
| 322 | 120 |
| 336 | 121 S : {l : Level } → { X : Set l } → Int X → Int X |
| 122 S {l} {X} t = λ(x : X) → λ(y : X → X ) → y ( t x y ) | |
| 322 | 123 |
| 336 | 124 n0 : {l : Level} {X : Set l} → Int X |
| 331 | 125 n0 = Zero |
| 326 | 126 |
| 336 | 127 n1 : {l : Level } → { X : Set l } → Int X |
| 128 n1 {_} {X} = λ(x : X ) → λ(y : X → X ) → y x | |
| 322 | 129 |
| 336 | 130 n2 : {l : Level } → { X : Set l } → Int X |
| 131 n2 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y x) | |
| 322 | 132 |
| 336 | 133 n3 : {l : Level } → { X : Set l } → Int X |
| 134 n3 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y (y x)) | |
| 323 | 135 |
| 336 | 136 n4 : {l : Level } → { X : Set l } → Int X |
| 137 n4 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y (y (y x))) | |
|
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
138 |
| 336 | 139 lemma13 : {l : Level } → { X : Set l } → S (S (Zero {_} {X})) ≡ n2 |
| 331 | 140 lemma13 = refl |
| 322 | 141 |
| 336 | 142 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
143 It u f t = t u f |
| 316 | 144 |
| 349 | 145 ItInt : {l : Level} {X : Set l} → Int X → (X → Int X ) → ( Int X → Int X ) → Int X → Int X |
| 146 ItInt {l} {X} u g f t = λ z s → t (u z s) ( λ (w : X) → (f (g w)) z s ) | |
| 323 | 147 |
| 783 | 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 | |
| 150 | |
| 345 | 151 R : {l : Level} { U X : Set l} → U → ( U → Int X → U ) → Int _ → U |
| 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 ) | |
| 336 | 153 |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
154 -- bad adder which modifies input type |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
155 add' : {l : Level} {X : Set l} → Int (Int X) → Int X → Int X |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
156 add' x y = It y S x |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
157 |
| 336 | 158 add : {l : Level} {X : Set l} → Int X → Int X → Int X |
| 344 | 159 add x y = λ z s → x (y z s) s |
| 336 | 160 |
| 345 | 161 add'' : {l : Level} {X : Set l} → Int X → Int X → Int X |
| 349 | 162 add'' x y = ItInt y (\w z s -> w )S x |
| 345 | 163 |
| 164 lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y ≡ add'' x y | |
| 165 lemma22 x y = refl | |
| 166 | |
| 783 | 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 | |
| 339 | 181 -- bad adder which modifies input type |
| 182 mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X | |
| 183 mul' {l} {X} x y = It Zero (add x) y | |
| 324 | 184 |
| 339 | 185 mul : {l : Level } {X : Set l} → Int X → Int X → Int X |
| 344 | 186 mul {l} {X} x y = λ z s → x z ( λ w → y w s ) |
| 187 | |
| 188 mul'' : {l : Level } {X : Set l} → Int X → Int X → Int X | |
| 349 | 189 mul'' {l} {X} x y = ItInt Zero (\w z s -> w) (add'' x) y |
|
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
190 |
| 336 | 191 fact : {l : Level} {X : Set l} → Int _ → Int X |
| 339 | 192 fact {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w)) n |
| 326 | 193 |
| 336 | 194 lemma13' : {l : Level} {X : Set l} → fact {l} {X} n4 ≡ mul n4 ( mul n2 n3) |
|
334
357d3114c9b5
add : Int X -> Int X -> Int X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
333
diff
changeset
|
195 lemma13' = refl |
| 324 | 196 |
| 345 | 197 -- lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → mul x y ≡ mul'' x y |
| 198 -- lemma23 x y = {!!} | |
| 199 | |
| 200 lemma24 : {l : Level } {X : Set l} → mul {l} {X} n4 n3 ≡ mul'' {l} {X} n3 n4 | |
| 201 lemma24 = refl | |
| 202 | |
| 344 | 203 |
| 336 | 204 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y ≡ mul y x |
| 783 | 205 -- lemma14 x y = {!!} -- It {!!} {!!} {!!} |
| 323 | 206 |
| 336 | 207 lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2 |
| 324 | 208 lemma15 x y = refl |
| 323 | 209 |
| 344 | 210 lemma15' : {l : Level} {X : Set l} (x y : Int X) → mul'' {l} {X} n2 n3 ≡ mul'' {l} {X} n3 n2 |
| 211 lemma15' x y = refl | |
| 212 | |
| 336 | 213 lemma16 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int X → U ) → R u v Zero ≡ u |
| 324 | 214 lemma16 u v = refl |
| 215 | |
| 336 | 216 -- lemma17 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int → U ) → (t : Int ) → R u v (S t) ≡ v ( R u v t ) t |
| 324 | 217 -- lemma17 u v t = refl |
| 218 | |
| 336 | 219 -- postulate lemma17 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int X → U ) → (t : Int X ) → R u v (S t) ≡ v ( R u v t ) t |
| 316 | 220 |
| 336 | 221 List : {l : Level} (U X : Set l) → Set l |
| 347 | 222 List {l} = λ( U X : Set l) → X → ( U → X → X ) → X |
| 323 | 223 |
| 336 | 224 Nil : {l : Level} {U : Set l} {X : Set l} → List U X |
| 225 Nil {l} {U} {X} = λ(x : X) → λ(y : U → X → X) → x | |
| 325 | 226 |
| 336 | 227 Cons : {l : Level} {U : Set l} {X : Set l} → U → List U X → List U X |
| 228 Cons {l} {U} {X} u t = λ(x : X) → λ(y : U → X → X) → y u (t x y ) | |
| 325 | 229 |
| 336 | 230 l0 : {l : Level} {X X' : Set l} → List (Int X) (X') |
| 325 | 231 l0 = Nil |
| 232 | |
| 336 | 233 l1 : {l : Level} {X X' : Set l} → List (Int X) (X') |
| 325 | 234 l1 = Cons n1 Nil |
| 235 | |
| 336 | 236 l2 : {l : Level} {X X' : Set l} → List (Int X) (X') |
| 325 | 237 l2 = Cons n2 l1 |
| 323 | 238 |
| 336 | 239 l3 : {l : Level} {X X' : Set l} → List (Int X) (X') |
| 330 | 240 l3 = Cons n3 l2 |
| 241 | |
| 347 | 242 -- λ x x₁ y → y x (y x (y x x₁)) |
| 243 l4 : {l : Level} {X X' : Set l} → Int X → List (Int X) (X') | |
| 244 l4 x = Cons x (Cons x (Cons x Nil)) | |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
245 |
| 349 | 246 ListIt : {l : Level} {U X : Set l} → X → ( U → X → X ) → List U X → X |
| 347 | 247 ListIt w f t = t w f |
| 248 | |
| 349 | 249 LListIt : {l : Level} {U X : Set l} → List U X → (X → List U X) → ( U → List U X → List U X ) → List U X → List U X |
| 250 LListIt {l} {U} {X} w g f t = λ x y → t (w x y) (λ (x' : U) (y' : X) → (f x' (g y')) x y ) | |
| 347 | 251 |
| 348 | 252 -- Cdr : {l : Level} {U : Set l} {X : Set l} → List U X → List U X |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
253 -- Cdr w = λ x → λ y → w x (λ x y → y) |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
254 |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
255 -- lemma181 :{l : Level} {U : Set l} {X : Set l} → Car Zero l2 ≡ n2 |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
256 -- lemma181 = refl |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
257 |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
258 -- lemma182 :{l : Level} {U : Set l} {X : Set l} → Cdr l2 ≡ l1 |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
259 -- lemma182 = refl |
| 323 | 260 |
| 348 | 261 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool X |
| 347 | 262 Nullp {_} {_} {X} list = ListIt (T X) (λ u w → (F X)) list |
| 263 | |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
264 -- bad append |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
265 Append' : {l : Level} {U X : Set l} → List U (List U X) → List U X → List U X |
| 347 | 266 Append' {_} {_} {X} x y = ListIt y Cons x |
| 325 | 267 |
| 336 | 268 Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X |
| 349 | 269 Append x y = λ n c → x (y n c) c |
| 325 | 270 |
| 347 | 271 Append'' : {l : Level} {U X : Set l} → List U X → List U X → List U X |
| 349 | 272 Append'' {_} {_} {X} x y = LListIt y (\e n c -> e) Cons x |
| 347 | 273 |
| 336 | 274 lemma18 :{l : Level} {U : Set l} {X : Set l} → Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) |
| 328 | 275 lemma18 = refl |
| 326 | 276 |
| 347 | 277 lemma18' :{l : Level} {U : Set l} {X : Set l} → Append'' {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) |
| 278 lemma18' = refl | |
| 279 | |
| 280 lemma18'' :{l : Level} {U : Set l} {X : Set l} → Append'' {_} {Int U} {X} ≡ Append | |
| 281 lemma18'' = refl | |
| 282 | |
| 336 | 283 Reverse : {l : Level} {U : Set l} {X : Set l} → List U (List U X) → List U X |
| 347 | 284 Reverse {l} {U} {X} x = ListIt Nil ( λ u w → Append w (Cons u Nil) ) x |
| 348 | 285 -- λ x → x (λ x₁ y → x₁) (λ u w s t → w (t u s) t) |
| 330 | 286 |
| 336 | 287 lemma19 :{l : Level} {U : Set l} {X : Set l} → Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil)) |
| 330 | 288 lemma19 = refl |
| 289 | |
| 347 | 290 Reverse' : {l : Level} {U : Set l} {X : Set l} → List U X → List U X |
| 349 | 291 Reverse' {l} {U} {X} x = LListIt Nil (\e n c -> e) ( λ u w → Append w (Cons u Nil) ) x |
| 348 | 292 -- λ x x₁ y → x x₁ (λ x' y' → y') |
| 347 | 293 |
| 348 | 294 -- lemma19' :{l : Level} {U : Set l} {X : Set l} → Reverse' {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil)) |
| 349 | 295 -- lemma19' = refl |
| 347 | 296 |
| 336 | 297 Tree : {l : Level} → Set l → Set l → Set l |
| 298 Tree {l} = λ( U X : Set l) → X → ( (U → X) → X ) → X | |
| 325 | 299 |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
300 NilTree : {l : Level} {U : Set l} {X : Set l} → Tree U X |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
301 NilTree {l} {U} {X} = λ(x : X) → λ(y : (U → X) → X) → x |
| 325 | 302 |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
303 Collect : {l : Level} {U : Set l} {X : Set l} → (U → Tree U X ) → Tree U X |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
304 Collect {l} {U} {X} f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y ) |
| 325 | 305 |
| 349 | 306 TreeIt : {l : Level} {U X X : Set l} → X → ( (U → X) → X ) → Tree U X → X |
| 331 | 307 TreeIt w h t = t w h |
|
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
308 |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
309 t0 : {l : Level} {X X' : Set l} → Tree (Bool X) X' |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
310 t0 {l} {X} {X'} = NilTree |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
311 |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
312 t1 : {l : Level} {X X' : Set l} → Tree (Bool X) X' |
|
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
313 t1 {l} {X} {X'} = NilTree -- Collect (λ b → D b NilTree (λ c → Collect NilTree NilTree )) |