coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] coq + higher inductive types + proof irrelevance?
Date: Thu, 26 Jul 2018 17:27:33 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f169.google.com
Ironport-phdr: 9a23:UTJ+oBzBr09zPRzXCy+O+j09IxM/srCxBDY+r6Qd1OMRIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDniCkJOT03/nzJhMNsl69Uug6tqgZlzoLIfI2YNvxzdb7dc9MAQmpBW95cWjBaDYO8bosPFOoBMvhbr4Lgu1YOqwGxBQ+xC+jyzTJHnGT53a070+Q6EQHJwg8gE8gUv3TSttr1MrodXfq0zKnJ0TXDYOhb2Tj46IfScxAhpeuAUq53ccrU0EQiER7OgFuXqYzgJTyV1+INvnCH4OpnT+KvjXAoqwV1ojS12Mgjl5TJi4QIwV7H7SV02Jg5KcG8RUJhYtOpEIFcuzybOodrWM8uXmBltSI8x7Ybo5C0ZjIKx44ixxPHa/yIbYyI4hX7WeaUOzh4hXZldKu/hhe87USs0+P8WtS13VtOtCZFnd7MtncC1xzX9MeLUOdy/kCk2TqX1gDT7P9LIVwsmKbFN5IsxqQ8m5kTvEjZAyP7mVj6gLWLekgl/uWk8+Hnba/npp+YOY90kAb+MqE2l8OlGus4MgkOX3Ob+eui173v51f2QLNQgf0wj6bVqpHaJcUHpq62GAJV3YMj5Ay+DzeiytgXgX4HLFdddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd81gogZQCeEBrKTGKLUq16BoOw1dbqifogQ7R/3K/k+5/PtxVY/kFkRNf2g15sWc3C1HbJvJUyfbTztg8sOOWgPtws6CuftjQvRAnZoe3+uUvdktXkAA4W8ANKbH9H/sPm6xC6+W6ZuSCVDA1GIH23vctzdCfgJYSOWZMRml25dDOTze8oazRir8TTC5f9/NOONo38XsJvi0J5+4OiBzUhvpwwxNNyU1iS2d08xnm4MQGVojqV2oEg420jblKYh3a0eGttU6PdEFAw9MMyEwg==

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