Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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/



Archive powered by MHonArc 2.6.18.

Top of Page