[Agda] projection?

[KINOSHITA Yoshiki]

For demonstration purpose, I tried to define a `projection' of
product types in general, in vain.  I would appreciate any
suggestion.

First I defined cross (there is a unicode character for cross, but
in order to send it via e-mail, I use >< for cross) as follows.
  record _><_ : (A B : Set) : Set where
    field
      pi1 : A
      pi2 : B
Then I wanted to define
  p1 : {A B : Set} -> A
with an obvious meaning.  But the record selector XXX.YYY is allowed
only for identifiers XXX; XXX may not be a general term.  So,
I cannot write something like (A >< B).pi1, which means the
following fails.
  p1 {A} {B} = (A >< B).pi1
I also tried
  pi {A} {B} = let C = A >< B in C.pi1
in vain, because C.pi1 cannot be used outside the let expression,
C being local.
So I got stucked.

Any nice idea?

Yoshiki.