|
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
|
|
|
27 Bool = {X : Set l} -> X -> X -> X
|
|
|
28
|
|
|
29 T : Bool
|
|
|
30 T = \{X : Set l} -> \(x y : X) -> x
|
|
|
31
|
|
|
32 F : Bool
|
|
|
33 F = \{X : Set l} -> \(x y : X) -> y
|
|
|
34
|
|
|
35 D : {U : Set l} -> U -> U -> Bool -> U
|
|
|
36 D {U} u v t = t {U} u v
|
|
|
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
|
|
|
44 _×_ : Set l -> Set l -> Set (suc l)
|
|
|
45 U × V = {X : Set l} -> (U -> V -> X) -> X
|
|
|
46
|
|
|
47 <_,_> : {U V : Set l} -> U -> V -> (U × V)
|
|
|
48 <_,_> {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
|
|
|
49
|
|
|
50 π1 : {U V : Set l} -> (U × V) -> U
|
|
|
51 π1 {U} {V} t = t {U} (\(x : U) -> \(y : V) -> x)
|
|
|
52
|
|
|
53 π2 : {U V : Set l} -> (U × V) -> V
|
|
|
54 π2 {U} {V} t = t {V} (\(x : U) -> \(y : V) -> y)
|
|
|
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
|
|
|
70 Emp = \{X : Set l } -> X
|
|
|
71
|
|
|
72 ε : {X : Set l } -> ( Set l -> X ) -> Emp {X}
|
|
|
73 ε {U} t = t U
|
|
|
74
|
|
|
75 --lemma09 : {U : Set l} -> {t : U } -> ε {U} (ε {Emp} t) ≡ ε {U} t
|
|
|
76 --lemma09 = ?
|
|
|
77
|
|
|
78 --lemma10 : {U V : Set l} -> (t : U × V ) -> π1 ( ε { U × V } t ) ≡ ε {U} t
|
|
|
79 --lemma10 = ?
|
|
|
80
|
|
|
81 _+_ : Set l -> Set l -> Set (suc l)
|
|
|
82 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
|
|
|
83
|
|
|
84 ι1 : {U V : Set l} -> U -> U + V
|
|
|
85 ι1 {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
|
|
|
86
|
|
|
87 ι2 : {U V : Set l} -> V -> U + V
|
|
|
88 ι2 {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
|
|
|
89
|
|
|
90 -- δ's aguments should aware x as raw symbol
|
|
|
91
|
|
|
92 δ : { U V R S : Set l } -> U -> U -> ( R + S ) -> U
|
|
|
93 δ {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u ) ( \(y : S) -> v )
|
|
|
94
|
|
|
95 lemma11 : { U V R S : Set l } -> (u v : U ) -> (r : R) -> δ {U} {V} {R} {S} u v ( ι1 r ) ≡ u
|
|
|
96 lemma11 u v r = refl
|
|
|
97
|
|
|
98 lemma12 : { U V R S : Set l } -> (u v : U ) -> (s : S) -> δ {U} {V} {R} {S} u v ( ι2 s ) ≡ v
|
|
|
99 lemma12 u v s = refl
|
|
|
100
|
|
|
101
|
|
|
102
|
|
|
103
|
|
|
104
|
|
|
105
|
|
|
106
|
|
|
107
|
|
|
108
|
|
|
109
|
|
|
110
|
|
|
111
|
|
|
112
|
