[Agda] preserving predicate

[Darryl McAdams]

I don't know if there's a built in, but this looks like it could be part of some form of generalization of an eliminator, for application non-initial algebras.

- darryl


________________________________
 From: Serge D. Mechveliani <mechvel at botik.ru>
To: agda at lists.chalmers.se 
Sent: Saturday, February 9, 2013 12:31 PM
Subject: [Agda] preserving predicate
 
People,
does there exist a library item which is close to 

  Closed_2 : \forall {l} {A : Set l} (A -> Bool) -> Op_2 A -> Set _
  Closed_2 p _*_ =  p x -> p y -> p (x * y)
?

(for example, this expresses that a subset in A is closed by _*_).

Thanks,

------
Sergei
  



_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130209/94a19ff9/attachment.html