--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/systemF.agda	Thu Mar 20 14:49:33 2014 +0900
@@ -0,0 +1,43 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+module systemF {l : Level}  where
+
+-- Bool
+
+Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
+
+T : Bool
+T = \{X : Set} -> \(x : X) -> \y -> x
+
+F : Bool
+F = \{X : Set} -> \x -> \(y : X) -> y
+
+D : {X : Set} -> (U V : X) -> Bool -> X
+D {X} u v bool = bool {X} u v
+
+lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u
+lemma-bool-t = refl
+
+lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
+lemma-bool-f = refl
+
+-- Product
+
+_×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
+_×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
+
+<_,_> : {l : Level} -> {U V : Set l} -> U -> V -> (U × V)
+<_,_> {l} {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
+
+lemma-product-pi1 : {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
+lemma-product-pi1 = refl
+
+lemma-product-pi2 : {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
+lemma-product-pi2 = refl
\ No newline at end of file