Benedikt Ahrens

On 31/05/18 15:54, Daniel R. Grayson wrote: > A comment from Thorsten Altenkirch: > > In Moerdijk and Gambino’s “Wellfounded trees in categories” it is shown > that very topos...

On 01/20/2017 03:07 PM, Daniel R. Grayson wrote: > Benedikt, I guess you didn't literally mean "loop", but rather, "take > a long time". The honest answer is that I...

On 01/20/2017 04:11 PM, Daniel R. Grayson wrote: > It might be illuminating to run Coq in the debugger and see what it's > doing. Well, we know that it...

On 01/20/2017 04:37 PM, Daniel R. Grayson wrote: > Yes, but why does it examine it first, before doing what it would have done if the proof > hadn't been...

On 01/20/2017 04:43 PM, Daniel R. Grayson wrote: > I've assigned myself to this issue, so I can be reminded to look into > that in the debugger. That's great,...

Let's discuss scientific evidence instead of religious principles: Here is where Qed'ing has helped in the past: - The inductive sets Anders and I have programmed do compute as well...

Re "Having a Qed that can be “opened up” *but not closed up again” does not sound very useful." Closing up a term `t` can make that another term that...

On 02/18/2017 03:16 PM, Daniel R. Grayson wrote: > See the comment at https://github.com/UniMath/UniMath/pull/567#discussion_r101888918 > > Rename induction principles such as UU_rect to UU_rec, after #567 gets merged. > >...

I agree, but I do not want to spend time on this right now.

@DanGrayson : could you take a look at this?