<div dir="ltr"><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">Glen,</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333"><br></div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">It is kind of funny to me, and yet should not surprise me, that an</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">individual was motivated to write a theorem prover in R. OTOH,</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">every attempt I have ever made to get Agda to work for me has</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">required sandboxing my Haskell environments and switching to</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">an emacs editor, so hey. Still, the project strikes me as being one</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">of bull headedness, a just-to-see-if-one-can kind of thing.</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333"><br></div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">Do you think they will go so far as to implement general dependent</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">typing? Last night at some point, I was thinking about the problem of</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">implementing flexible contravariant functors in a computing language.</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">This often appears to a stumbling block when I set out to define <i>for all</i></div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">and <i>there exists</i> from a substitution functor, a la Topos theory.</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">Any thoughts are welcome.</div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333"><br></div><div class="gmail_default" style="font-family:garamond,serif;font-size:small;color:#333333">Jon</div></div>