coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] a question

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Homotopy Type Theory <homotopytypetheory AT googlegroups.com>
Cc: "Prof. Vladimir Voevodsky" <vladimir AT ias.edu>, Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] a question
Date: Mon, 28 Sep 2015 04:20:03 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vladimir AT ias.edu; spf=None smtp.mailfrom=vladimir AT ias.edu; spf=None smtp.helo=postmaster AT pps3.ias.edu
Ironport-phdr: 9a23:pSameBA+pZr3uaKLlo8lUyQJP3N1i/DPJgcQr6AfoPdwSP/7psbcNUDSrc9gkEXOFd2CrakU16yL7uu4ACQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkb3vsMWKKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WbQyK4WcbSnRergtQDkD57Bz9RIa55iv9s+1h3zGLIdzuQKw0VDO4/o9kTxjnjCoILTkk6HqRgct12vF1uhWk8iJ7yoLVZYCPfMR5c73accgZVCIVQMJYWy1EA5mUboIUSecNILAL/MHGu1ISoE7mVkGXD+T1x2oN3yeu0A==

Is it correct to say that the main problem in constructive type theory is to
create a type theory that simultaneously satisfies two conditions:

1. the function extensionality principle
2. the principle of decidability of typing judgements

?

Is it right that no such theory exists?

Vladimir.

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

Re: [Coq-Club] a question, Pierre Courtieu, 09/01/2015
- <Possible follow-up(s)>
- [Coq-Club] a question, Vladimir Voevodsky, 09/28/2015
  - Re: [Coq-Club] a question, Peter LeFanu Lumsdaine, 09/28/2015
    - Re: [Coq-Club] [HoTT] Re: a question, Bas Spitters, 09/28/2015
      - Re: [Coq-Club] [HoTT] Re: a question, Martin Escardo, 09/28/2015
  - Re: [Coq-Club] a question, Jean-Francois Monin, 09/28/2015
    - Re: [Coq-Club] a question, Thorsten Altenkirch, 09/28/2015
    - Re: [Coq-Club] a question, Gabriel Scherer, 09/28/2015
  - Re: [Coq-Club] a question, Andrew Polonsky, 09/28/2015