coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq + higher inductive types + proof irrelevance?

From: Steven Schäfer <s.schaefer89 AT googlemail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] coq + higher inductive types + proof irrelevance?
Date: Fri, 27 Jul 2018 09:32:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=s.schaefer89 AT googlemail.com; spf=Pass smtp.mailfrom=s.schaefer89 AT googlemail.com; spf=None smtp.helo=postmaster AT mail-it0-f47.google.com
Ironport-phdr: 9a23:iOvjBROjWHFGOfSCePQl6mtUPXoX/o7sNwtQ0KIMzox0Lfv5rarrMEGX3/hxlliBBdydt6oazbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlJiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAB/z5LObY2JKPZyYqHQcNUHTmRBRMZRUClBD5uhYYsTEeUBI/hXr4/lqFUTsRS+BQyrBO3xxT9Sm3T72rY63/46EQ7a3AwvBcwBsHrKo9XvN6ofVfu4zKbPzTXEYPNW3Sny6I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW4PZnVeK1jW4otQVxojy1ysgyl4bJm4QYwU3H+yVh2Is5O8G0RUphbdOnEJZcrT+WO5Z5T884TGxluiA3waAct5GhZigF0pEnygbfa/OZd4iI5QruVOOLLjd5gHJpYbO/hwqu/US5xO3xWcu53ExFripCldnMuXQN2ALJ5sebTft9+1+t2TeJ1w/N9uFJOV44mbbfJpI7wbM9loAfvVreEiL5gkn7g62bel0h+uey6uTnZrvmpoWbN49xkgz+Kb4imtejDuQ4KAcBQWab9vqm1LDg+UD0W7pKjvoxkqnWtJDVO8EbqbS4Aw9RyIos9xG/DzK+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmUUjo8dfcExURMgquwu+hBs8u+JkZXDe0HqKHPaXlilSIauwiOaHYf8kOszb0JvYo/a6/pXA+nlAZcKyg3J9RY3e9SKc1a36FaGbh149SWVwBuRAzGbSz2Q+yFAVLbnP3ZJoSozQyCYaoF4DGH97/j7uG0yO2G5RXYiZNDVXeSC60JbXBYO8FbWepGuEkiiYNDObzRIgm2hWjsQb7z/xsKe+GonRF56Km78B84qjorT939TFwCJ7AgWSETmUxn39QAjFqg+ZwpktyzlrF2q990aRV

Hi Abhishek,

Quotient types exist and proof irrelevance (along with propositional
and functional extensionality) holds in the setoid model of type
theory. The difference to higher-inductive types is that you cannot
add computation rules on paths, since that would give you homotopy
pushouts and thus also the circle and other non-hsets.

If you are worried about consistency you could also just axiomatize
the "propositional trunctation" (or rather, squash types as in NuPRL)
and then derive quotient types from that together with funext/propext.

- Steven

2018-07-26 23:27 GMT+02:00 Abhishek Anand
<abhishek.anand.iitg AT gmail.com>:
> I understand that UIP (implied by proof irrelevance) is inconsistent with
> univalence.
>
> Can higher inductive types (or just some kind of "level 1" quotients where I
> don't care about distinguishing equality proofs) be added to Coq without
> needing to blacklist the proof irrelevance axiom?
>
> --
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

[Coq-Club] coq + higher inductive types + proof irrelevance?, Abhishek Anand, 07/26/2018
- Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Jason -Zhong Sheng- Hu, 07/27/2018
- Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Steven Schäfer, 07/27/2018
  - Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Bas Spitters, 07/27/2018
    - Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Siddharth Bhat, 07/27/2018
      - Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Steven Schäfer, 07/27/2018
        
        Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Bas Spitters, 07/27/2018