[Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Cody Roux]

Nice summary!


On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
> Agda enforces termination via a termination checker which is more 
> flexible but I think less principled than Coq's approach. 
     That's a bit scary given that there was an inconsistency found in 
the Coq termination checker just a couple of weeks ago :)

     BTW, has anyone tried reproducing the bug in Agda?


Cody