coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Going from \/ to +

From: Andrej Bauer <andrej.bauer AT andrej.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Going from \/ to +
Date: Sun, 8 Dec 2013 20:58:44 +0100

I thought so, and I do not see how to play a trick with singleton
elimination to get it done (that's the only chance to eliminate from
Prop into Type, as far as I know). In homotopy type theory this should
be doable. There \/ is interpreted as the propositional truncation of
+.

With kind regards,

Andrej

[Coq-Club] Going from \/ to +, Andrej Bauer, 12/08/2013
- Re: [Coq-Club] Going from \/ to +, Arthur Azevedo de Amorim, 12/08/2013
  - Re: [Coq-Club] Going from \/ to +, Jason Gross, 12/08/2013
- Re: [Coq-Club] Going from \/ to +, Abhishek Anand, 12/08/2013
  - Re: [Coq-Club] Going from \/ to +, Andrej Bauer, 12/08/2013
    - Re: [Coq-Club] Going from \/ to +, Jason Gross, 12/08/2013
      - Re: [Coq-Club] Going from \/ to +, Vladimir Voevodsky, 12/08/2013
        
        Re: [Coq-Club] Going from \/ to +, Jason Gross, 12/08/2013
        
        Re: [Coq-Club] Going from \/ to +, Jason Gross, 12/08/2013