coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] coq + higher inductive types + proof irrelevance?
Date: Fri, 27 Jul 2018 01:02:52 +0000
Accept-language: en-CA, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-BY2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:0fIYlBG9NZXi2rFhrwYJV51GYnF86YWxBRYc798ds5kLTJ7zocmwAkXT6L1XgUPTWs2DsrQY07SQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDuwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBNjzIHZe5uaOOZicq7HYd8WWXRNU8BMXCJBGIO8aI4PAvIFM+lCtIn9oF0OpganCQavBOPvzTlIhnDr1qMn0+QuDwfG3AM5E9kTsnrUscj+OaAcUe+ozKnJzC7DY+1K1Tvg9ITFaRAhofaQXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkDvWic6upvT+Ovi2g/pg5tpTiv3MEshZfNhoIR0FzL6zh2wJszKNalS0B7ecapHZRMuy2AM4Z6XNkuTmBytCokybAKoZC7czYJxZg7whPSbvKHfJWK7x/nUeudPDd1iXxrdb+6nRm97FOvxfH5W8S7zFlFtTFKn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lcL00okqTXN5Aszqctm5URr0jPByj2l17og6OMcUUk5/So5P/gYrX7oJ+TKpV4ihnkMqQphsywH/g3MhQPX2ic/+Swzrrj/VDlQLVOif02larZvIrGKsQco661Gw5V0oA95BajFzqr38gUkWMDIV5bYh6KjpLlN0/NLfzgCPewmVWskDNlx/DcOb3hB43ALnben7fhfLd98FBQxBYuwdxD/J9UCrYBIO72WkDrtdzYCgU1PBCzw+biENl9zJ8RWXqTAq+FN6PfqUOH5uU2I+WVeIAVvCv9JOM+6v71jX45nEcdcrOz0ZsWbnC4BPVmLF+DbXrimNdSWVsN6wE5VanhjECIGWpYYG/3VKYh7Bk6DpinBMHNXNb+rqaG2XKZF4ZRYCgDOFCLF3igTIWJXfhJIAKPaptvnjwWTuL5EtcJ1RaysQb7z/xsKe+CqX5Qjo7qyNUgv76brho17zEhV53MgVHIdHl9myYzfxFz2al+pUJnzVLaivp4hOBdHN1XofhOV1VjbMKO/6lBE9n3Hzn5UJKRUl//GYemBi00R9M1hdQJZhQlQojwvlX4xyOvRoQtufmLCZgzrv2O+VHUf5044Uecka4rgh8hX9dFMnCgiuhn7Q/PCoXVkkKf0aG3aaAb2y2L/2CGnzOD

Can I read the question as asking if axiom K/UIP consistent with CIC? Or are you asking if `forall (P Q : Prop), (P <-> Q) <-> (P = Q)` is consistent with CIC?

- Jason

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Sent: July 26, 2018 5:27:33 PM
To: coq-club
Subject: [Coq-Club] coq + higher inductive types + proof irrelevance?

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