[Agda] preserving predicate

Darryl McAdams psygnisfive at yahoo.com
Sat Feb 9 20:44:35 CET 2013

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
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 _*_).



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

More information about the Agda mailing list