Mike Shulman
Mike Shulman
> as many copies of True as inhabited h-prop_n types In all the models I'm familiar with, this many copies would have too high a cardinality to fit in HProp₀....
I mean outside the type theory, in the set theory where we consider models. I'm not hugely familiar with System-F-style models, so it's possible you could play some game there....
I would be interested in seeing the details of a system-F-type model of this rule, though. Can you really cook things up so that `{x:A & a=x}`, for instance, always...
I'm fine with ScopeData. Thanks!
The comment in January suggested you would be open to a change like this. If that's right, do you have a guess about when it might happen? As in, "next...
I'm sorry to hear you're dealing with personal issues; I hope everything works out okay. Thanks for the update; I'll wait for the summer then.
I think I don't completely understand what the name-modifying effects are for. It looks to me like they are basically a way for the programmer to tell yuujinchou what to...
Ok, so these effects are basically a Reader to avoid passing arguments around between functions. I don't think that should cause any problems with what I have in mind, if...
Thinking about this some more, and looking at the code again, I have an even simpler suggestion. What `Scope` does with a pair of namespaces is not complicated and I...
I'll be sure to let you know when I write it!