Jacques Carette
Jacques Carette
My 2 cents: I think it would make most sense to use module names (likely behind an interface, so that library-relative module names could be used in the future) rather...
Wow, that's impressive. That does indeed seem like quite the slog.
`return` to `pure` makes perfect sense. Deduplification of definitions is often a good thing, so the other half of this seems like a good idea as well. But it could...
Almost. For access, it is. For creation, AFAIK, you still have to use the nested structure. Or, at least, that's what ctrl-R always gives me.
Thanks - hopefully I'll have time (and wifi) on the long train ride tomorrow to deal with this.
My long-term bias definitely is to structure things as per this suggestion, with `empty : F A` first, then combined with `__`. `Pointed` is a confusing thing. Pointed objects are...
Can you explain what order you have in mind that makes `ReflClosure` a special case of `_≤_`? Right now, I'm not seeing it. Maybe that propositional is always contained in...
This still seems different to me. With `ReflClosure`, you build up an explicit path that relates things, but that seems to rule out other kinds of evidence? Unless `_~_` does...
That's a really good idea. Count me in on those willing to do the admin work to get this done.
My personal view is that the paper should "thank" people with a very small number of contributions (and those who have been active on issues without necessarily doing PRs), but...