<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>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.</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div>- darryl<br></div> <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1"> <b><span style="font-weight:bold;">From:</span></b> Serge D. Mechveliani <mechvel@botik.ru><br> <b><span style="font-weight: bold;">To:</span></b> agda@lists.chalmers.se <br> <b><span style="font-weight: bold;">Sent:</span></b> Saturday, February 9, 2013
12:31 PM<br> <b><span style="font-weight: bold;">Subject:</span></b> [Agda] preserving predicate<br> </font> </div> <br>
People,<br>does there exist a library item which is close to <br><br> Closed_2 : \forall {l} {A : Set l} (A -> Bool) -> Op_2 A -> Set _<br> Closed_2 p _*_ = p x -> p y -> p (x * y)<br>?<br><br>(for example, this expresses that a subset in A is closed by _*_).<br><br>Thanks,<br><br>------<br>Sergei<br> <br><br><br><br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br> </div> </div> </div></body></html>