coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] UIP and decidable equality

From: Alan Schmitt <alan.schmitt AT polytechnique.org>
To: Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>
Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>, Jason Gross <jasongross9 AT gmail.com>
Subject: Re: [Coq-Club] UIP and decidable equality
Date: Tue, 13 Sep 2016 08:29:22 +0200

On 2016-09-12 17:57, Thorsten Altenkirch
<Thorsten.Altenkirch AT nottingham.ac.uk>
writes:

> The proof by Hedberg only requires that there is a constant endofunction
>
> Pi x,y:A. x=y -> x=y

Very nice! This is what I meant by “canonical nu”.

Thanks,

Alan

--
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2016-08: 402.25, 2015-08: 398.93

Attachment: signature.asc
Description: PGP signature

[Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
- Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
    - Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/12/2016
      - Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/12/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/12/2016
        
        Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/13/2016
      - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/13/2016
- RE: [Coq-Club] UIP and decidable equality, Soegtrop, Michael, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
- Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
    - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
      - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
        
        Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/12/2016