[Agda] projection?

[Tatsuya Abe]

Sorry.  I have sent the following message from my non-member address.
I send it again.

Tatsuya Abe <abet at media.kyoto-u.ac.jp> wrote:
>Although I may miss the point, does _><_.pi1 satisfy your purpose?
>
>e.g.,
>
>tmp : Nat >< Bool
>tmp = record { pi1 = zero;  pi2 = true }
>
>_><_.pi1 tmp
>
>
>KINOSHITA Yoshiki <yoshiki at m.aist.go.jp> wrote:
>>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.
>>_______________________________________________
>>Agda mailing list
>>Agda at lists.chalmers.se
>>https://lists.chalmers.se/mailman/listinfo/agda