coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Cody Roux <cody.roux AT andrew.cmu.edu>
To: Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>, "homotopytypetheory AT googlegroups.com" <homotopytypetheory AT googlegroups.com>
Cc: "agda AT lists.chalmers.se" <agda AT lists.chalmers.se>, coq-club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq
Date: Mon, 06 Jan 2014 11:54:07 -0500

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

Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/06/2014
- Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/06/2014
  - Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/06/2014
    - Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Maxime Dénès, 01/06/2014
      - Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Maxime Dénès, 01/06/2014
        
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/07/2014
        
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/07/2014
        
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Vladimir Voevodsky, 01/07/2014
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/07/2014
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Vladimir Voevodsky, 01/07/2014
        
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/07/2014
        Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Frédéric Blanqui, 01/07/2014