coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] injectivity of inductive type implies False
Date: Wed, 1 Mar 2017 12:40:43 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f171.google.com
Ironport-phdr: 9a23:o0I41xJAPnk0l1ESr9mcpTZWNBhigK39O0sv0rFitYgXI/jxwZ3uMQTl6Ol3ixeRBMOAuq8C0LKd6vi5ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJG80Pn38JnOaU0cjz2kJLh2MR+erAPLt8BQj5E0eYgrzR6ci3FIev9WyGAgDFSamRq0ss66/J948ylT/fsn/shMF6T7Y6sQQrlRDTBgOGcwsp64/SLfRBeCsyNPGl4dlQBFVlDI

Inductive array (A:Type):nat->Type:=
|nil : array A 0
|cons : forall n:nat, A -> array A n -> array A (S n).

array m A=array n A -> m=n?

(Assuming you meant array A m instead of array m A)

I think that using something like the univalence axiom, you can prove:

array False 2 = array False 4

Then it would be bad to conclude 2=4.

-- Abhishek

Re: [Coq-Club] injectivity of inductive type implies False, Cristóbal Camarero Coterillo, 02/28/2017
- Re: [Coq-Club] injectivity of inductive type implies False, Abhishek Anand, 03/01/2017
- <Possible follow-up(s)>
- Re: [Coq-Club] injectivity of inductive type implies False, Cristóbal Camarero Coterillo, 03/02/2017
  - Re: [Coq-Club] injectivity of inductive type implies False, Thorsten Altenkirch, 03/03/2017
    - Re: [Coq-Club] injectivity of inductive type implies False, Marco Servetto, 03/03/2017
      - Re: [Coq-Club] injectivity of inductive type implies False, Greg Morrisett, 03/03/2017
        
        Re: [Coq-Club] injectivity of inductive type implies False, Thorsten Altenkirch, 03/17/2017
        
        Re: [Coq-Club] injectivity of inductive type implies False, Marco Servetto, 03/20/2017