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 = {!!}