Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] a question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a question


Chronological Thread 
  • From: Andrew Polonsky <andrew.polonsky AT gmail.com>
  • To: Homotopy Type Theory <HomotopyTypeTheory AT googlegroups.com>
  • Cc: homotopytypetheory AT googlegroups.com, vladimir AT ias.edu, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] a question
  • Date: Mon, 28 Sep 2015 04:01:56 -0700 (PDT)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andrew.polonsky AT gmail.com; spf=Pass smtp.mailfrom=andrew.polonsky AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f56.google.com
  • Ironport-phdr: 9a23:h+S/0hZfXSHU3IKt12zR6Af/LSx+4OfEezUN459isYplN5qZpMy9bnLW6fgltlLVR4KTs6sC0LqK9f29Ejdbqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7z0psCYOF4ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5lH/Sl6v4X4bTmIOg1J0EhDIpC36U5Dro2Oulu143zWdJdzKXKg5ZTSv6L16YBDvjygDOjEj93zPkYp7i6cN8zy7oBkq6ojYeoyKfMJ5eqTbZtALDT5IWMpLWjMHGoS4aI0UDPspMuNRro27rFwL+0jtTTKwDf/in2cbzkT92rc3hqF4SVnL
On Monday, September 28, 2015 at 10:20:06 AM UTC+2, v v wrote:
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 
 
The cubical type theory is the first one that accomplishes both without assuming some form of truncation.  (Modulo normalization proof.)

Andrew


On Monday, September 28, 2015 at 10:20:06 AM UTC+2, v v wrote:
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.

Archive powered by MHonArc 2.6.18.

Top of Page