--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/system-f.agda	Sat Mar 15 10:15:54 2014 +0900
@@ -0,0 +1,66 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+module system-f {l : Level} where
+
+postulate A : Set
+postulate B : Set
+
+data _∨_  (A B : Set) : Set where
+  or1 : A -> A ∨ B
+  or2 : B -> A ∨ B
+
+lemma01 : A -> A ∨ B
+lemma01 a = or1 a
+
+lemma02 : B -> A ∨ B
+lemma02 b = or2 b
+
+lemma03 : {C : Set} -> (A ∨ B) -> (A -> C) -> (B -> C) -> C
+lemma03 (or1 a) ac bc = ac a
+lemma03 (or2 b) ac bc = bc b
+
+postulate U : Set l
+postulate V : Set l
+
+
+Bool = {X : Set l} -> X -> X -> X
+
+T : Bool
+T = \{X : Set l} -> \(x y : X) -> x
+
+F : Bool
+F = \{X : Set l} -> \(x y : X) -> y
+
+D : {U : Set l} -> U -> U -> Bool -> U
+D {U} u v t = t {U} u v
+
+lemma04 : {u v : U} -> D u v T ≡  u
+lemma04 = refl
+
+lemma05 : {u v : U} -> D u v F ≡  v
+lemma05 = refl
+
+_×_ : Set l -> Set l ->  Set (suc l)
+U × V =  {X : Set l} -> (U -> V -> X)  -> X 
+
+<_,_> : {U V : Set l} -> U -> V -> (U ×  V) 
+<_,_> {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
+
+π1 : {U V : Set l} -> (U ×  V) -> U
+π1 {U} {V}  t = t {U} (\(x : U) -> \(y : V) -> x)
+
+π2 : {U V : Set l} -> (U ×  V) -> V
+π2 {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)
+
+lemma06 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
+lemma06 = refl
+
+lemma07 : {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡  v
+lemma07 = refl
+
+hoge : {U V : Set l} -> U -> V  -> (U ×  V)
+hoge u v = < u , v >
+
+-- lemma08 :  (t : U ×  V)  -> < π1 t  , π2 t > ≡ t
+-- lemma08 t = {!!}