|
315
|
1 open import Level
|
|
|
2 open import Relation.Binary.PropositionalEquality
|
|
|
3
|
|
|
4 module system-f {l : Level} where
|
|
|
5
|
|
|
6 postulate A : Set
|
|
|
7 postulate B : Set
|
|
|
8
|
|
|
9 data _∨_ (A B : Set) : Set where
|
|
|
10 or1 : A -> A ∨ B
|
|
|
11 or2 : B -> A ∨ B
|
|
|
12
|
|
|
13 lemma01 : A -> A ∨ B
|
|
|
14 lemma01 a = or1 a
|
|
|
15
|
|
|
16 lemma02 : B -> A ∨ B
|
|
|
17 lemma02 b = or2 b
|
|
|
18
|
|
|
19 lemma03 : {C : Set} -> (A ∨ B) -> (A -> C) -> (B -> C) -> C
|
|
|
20 lemma03 (or1 a) ac bc = ac a
|
|
|
21 lemma03 (or2 b) ac bc = bc b
|
|
|
22
|
|
|
23 postulate U : Set l
|
|
|
24 postulate V : Set l
|
|
|
25
|
|
|
26
|
|
325
|
27 Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
|
|
315
|
28
|
|
325
|
29 T : {l : Level} -> Bool
|
|
|
30 T {l} = \{X : Set l} -> \(x y : X) -> x
|
|
315
|
31
|
|
325
|
32 F : {l : Level} -> Bool
|
|
|
33 F {l} = \{X : Set l} -> \(x y : X) -> y
|
|
315
|
34
|
|
325
|
35 D : {l : Level} -> {U : Set l} -> U -> U -> Bool -> U
|
|
|
36 D {l} {U} u v t = t {U} u v
|
|
315
|
37
|
|
|
38 lemma04 : {u v : U} -> D u v T ≡ u
|
|
|
39 lemma04 = refl
|
|
|
40
|
|
|
41 lemma05 : {u v : U} -> D u v F ≡ v
|
|
|
42 lemma05 = refl
|
|
|
43
|
|
321
|
44 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
|
|
|
45 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
|
|
315
|
46
|
|
321
|
47 <_,_> : {l : Level} {U V : Set l} -> U -> V -> (U × V)
|
|
|
48 <_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
|
|
315
|
49
|
|
321
|
50 π1 : {l : Level} {U V : Set l} -> (U × V) -> U
|
|
|
51 π1 {l} {U} {V} t = t {U} (\(x : U) -> \(y : V) -> x)
|
|
315
|
52
|
|
321
|
53 π2 : {l : Level} {U V : Set l} -> (U × V) -> V
|
|
|
54 π2 {l} {U} {V} t = t {V} (\(x : U) -> \(y : V) -> y)
|
|
315
|
55
|
|
|
56 lemma06 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡ u
|
|
|
57 lemma06 = refl
|
|
|
58
|
|
|
59 lemma07 : {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡ v
|
|
|
60 lemma07 = refl
|
|
|
61
|
|
|
62 hoge : {U V : Set l} -> U -> V -> (U × V)
|
|
|
63 hoge u v = < u , v >
|
|
|
64
|
|
|
65 -- lemma08 : (t : U × V) -> < π1 t , π2 t > ≡ t
|
|
|
66 -- lemma08 t = {!!}
|
|
316
|
67
|
|
|
68 -- Emp definision is still wrong...
|
|
|
69
|
|
327
|
70 Emp : {l : Level} {X : Set l} -> Set l
|
|
|
71 Emp {l} = \{X : Set l} -> X
|
|
316
|
72
|
|
327
|
73 -- ε : {l : Level} (U : Set l) {l' : Level} {U' : Set l'} -> Emp -> Emp
|
|
|
74 -- ε {l} U t = t
|
|
316
|
75
|
|
327
|
76 -- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} -> (t : Emp {l} {U} ) -> ε U (ε Emp t) ≡ ε U t
|
|
322
|
77 -- lemma09 t = refl
|
|
321
|
78
|
|
327
|
79 -- lemma10 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> U × V
|
|
|
80 -- lemma10 {l} {U} {V} t = ε (U × V) t
|
|
316
|
81
|
|
327
|
82 -- lemma10' : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> Emp
|
|
|
83 -- lemma10' {l} {U} {V} {X} t = ε (U × V) t
|
|
|
84
|
|
|
85 -- lemma100 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U}) -> Emp
|
|
322
|
86 -- lemma100 {l} {U} {V} t = ε U t
|
|
321
|
87
|
|
327
|
88 -- lemma101 : {l k : Level} {U V : Set l} -> (t : Emp {_} {U × V}) -> π1 (ε (U × V) t) ≡ ε U t
|
|
322
|
89 -- lemma101 t = refl
|
|
319
|
90
|
|
327
|
91 -- lemma102 : {l k : Level} {U V : Set l} -> (t : Emp {_} {U × V}) -> π2 (ε (U × V) t) ≡ ε V t
|
|
322
|
92 -- lemma102 t = refl
|
|
321
|
93
|
|
327
|
94 -- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t
|
|
322
|
95 -- lemma103 u t = refl
|
|
316
|
96
|
|
|
97 _+_ : Set l -> Set l -> Set (suc l)
|
|
|
98 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
|
|
|
99
|
|
|
100 ι1 : {U V : Set l} -> U -> U + V
|
|
|
101 ι1 {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
|
|
|
102
|
|
|
103 ι2 : {U V : Set l} -> V -> U + V
|
|
|
104 ι2 {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
|
|
|
105
|
|
317
|
106 δ : { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
|
|
|
107 δ {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)
|
|
316
|
108
|
|
317
|
109 lemma11 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ {U} {V} {R} {S} u v ( ι1 r ) ≡ u r
|
|
316
|
110 lemma11 u v r = refl
|
|
|
111
|
|
317
|
112 lemma12 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ {U} {V} {R} {S} u v ( ι2 s ) ≡ v s
|
|
316
|
113 lemma12 u v s = refl
|
|
|
114
|
|
|
115
|
|
322
|
116 _××_ : {l : Level} -> Set (suc l) -> Set l -> Set (suc l)
|
|
|
117 _××_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
|
|
|
118
|
|
|
119 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} -> U -> V -> (U ×× V)
|
|
|
120 <<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
|
|
316
|
121
|
|
|
122
|
|
322
|
123 Int = \{l : Level } -> \{ X : Set l } -> X -> ( X -> X ) -> X
|
|
|
124
|
|
|
125 Zero : {l : Level } -> { X : Set l } -> Int
|
|
|
126 Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x
|
|
|
127
|
|
|
128 S : {l : Level } -> { X : Set l } -> Int -> Int
|
|
|
129 S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )
|
|
|
130
|
|
326
|
131 n0 : {l : Level} {X : Set l} -> Int {l} {X}
|
|
|
132 n0 = Zero
|
|
|
133
|
|
322
|
134 n1 : {l : Level } -> { X : Set l } -> Int {l} {X}
|
|
|
135 n1 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y x
|
|
|
136
|
|
|
137 n2 : {l : Level } -> { X : Set l } -> Int {l} {X}
|
|
|
138 n2 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)
|
|
|
139
|
|
323
|
140 n3 : {l : Level } -> { X : Set l } -> Int {l} {X}
|
|
|
141 n3 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))
|
|
|
142
|
|
322
|
143 lemma13 : {l : Level } -> { X : Set l } -> S ( S ( Zero {l} {X}) ) ≡ n2
|
|
|
144 lemma13 {l} {X} = refl
|
|
|
145
|
|
|
146 It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int -> U
|
|
|
147 It {l} {U} u f t = t u f
|
|
316
|
148
|
|
|
149
|
|
323
|
150 R : {l : Level} { U X : Set l} -> U -> ( U -> Int {l} {X} -> U ) -> Int -> U
|
|
|
151 R {l} {U} u v t = π1 ( It {suc l} {U × Int} (< u , Zero >) (λ (x : U × Int) → < v (π1 x) (π2 x) , S (π2 x) > ) t )
|
|
|
152
|
|
|
153 sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int
|
|
326
|
154 sum x y = It y ( λ z -> S z ) x
|
|
|
155
|
|
|
156 mul : {l : Level } {X : Set l} -> Int {l} {_} -> Int -> Int {l} {X}
|
|
|
157 mul x y = It Zero ( λ (z : Int) -> sum y z ) x
|
|
324
|
158
|
|
326
|
159 copyInt : {l : Level } {X : Set l} -> Int {l} {_} -> Int {l} {X}
|
|
|
160 copyInt x = It Zero ( λ (z : Int) -> S z ) x
|
|
324
|
161
|
|
326
|
162 -- fact : {l : Level} {X X' : Set l} -> Int -> Int {l} {_}
|
|
|
163 -- fact {l} {X} {X'} n = R (S Zero) (λ ( z w : Int) -> mul {l} {_} z (S w) ) n
|
|
|
164
|
|
|
165 -- lemma13' : fact n3 ≡ mul n1 ( mul n2 n3)
|
|
|
166 -- lemma13' = refl
|
|
324
|
167
|
|
|
168 -- lemma14 : (x y : Int) -> mul x y ≡ mul y x
|
|
326
|
169 -- lemma14 x y = It {!!} {!!} {!!}
|
|
323
|
170
|
|
326
|
171 lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2
|
|
324
|
172 lemma15 x y = refl
|
|
323
|
173
|
|
324
|
174 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int {l} {X} -> U ) -> R u v Zero ≡ u
|
|
|
175 lemma16 u v = refl
|
|
|
176
|
|
|
177 -- 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
|
|
|
178 -- lemma17 u v t = refl
|
|
|
179
|
|
|
180 -- postulate 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
|
|
316
|
181
|
|
|
182
|
|
325
|
183 List = \{l : Level} -> \{ U X : Set l} -> X -> ( U -> X -> X ) -> X
|
|
323
|
184
|
|
325
|
185 Nil : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {X}
|
|
|
186 Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x
|
|
|
187
|
|
|
188 Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List {l} {U} {X} -> List {l} {U} {X}
|
|
|
189 Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y )
|
|
|
190
|
|
|
191 l0 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X}
|
|
|
192 l0 = Nil
|
|
|
193
|
|
|
194 l1 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X}
|
|
|
195 l1 = Cons n1 Nil
|
|
|
196
|
|
|
197 l2 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X}
|
|
|
198 l2 = Cons n2 l1
|
|
323
|
199
|
|
325
|
200 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W
|
|
|
201 ListIt {l} {U} {W} {X} w f t = t w f
|
|
323
|
202
|
|
325
|
203 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {l}} -> Bool
|
|
|
204 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool} {X} T (\u w -> F) list
|
|
|
205
|
|
326
|
206 Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_}
|
|
325
|
207 Append {l} {U} {X} x y = ListIt {l} {U} {_} {X} y (\u w -> Cons u w) x
|
|
|
208
|
|
326
|
209 -- lemma18 : Append l1 l2 ≡ Cons n1 ( Cons n2 Nil )
|
|
|
210 -- lemma18 = refl
|
|
|
211
|
|
325
|
212 Tree = \{l : Level} -> \{ U X : Set l} -> X -> ( (U -> X) -> X ) -> X
|
|
|
213
|
|
|
214 NilTree : {l : Level} {U : Set l} {X : Set l} -> Tree {l} {U} {X}
|
|
|
215 NilTree {l} {U} {X} = \(x : X) -> \(y : (U -> X) -> X) -> x
|
|
|
216
|
|
|
217 Collect : {l : Level} {U : Set l} {X : Set l} -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree {l} {U} {X}
|
|
|
218 Collect {l} {U} {X} f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y )
|
|
|
219
|
|
|
220 TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree {l} {U} {W} -> W
|
|
|
221 TreeIt {l} {U} {W} {X} w h t = t w h
|
