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