--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/and.agda	Tue Mar 04 15:04:53 2014 +0900
@@ -0,0 +1,38 @@
+module and where
+
+postulate U : Set
+postulate V : Set
+postulate T : Set
+
+f : Set
+f = U -> V
+
+record _x_ (U V : Set) : Set where
+  field
+    pi1 : U
+    pi2 : V
+
+postulate <_,_> : U -> V -> (U x V)
+
+open _x_
+postulate u : U
+postulate v : V
+
+uv : U x V
+uv = < u , v >
+pair : Set
+pair = U x V 
+
+
+postulate t : T 
+
+x : T 
+x = t
+
+data _==_ {A : Set} : A -> A -> Set where 
+  refl : {x : A} -> x == x
+
+lemma02 : U
+lemma02 = pi1 (< u , v >)
+lemma01 : (pi1 ( < u , v > )) == u
+lemma01 = {!!}
\ No newline at end of file