coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] coq + higher inductive types + proof irrelevance?
Date: Wed, 17 Oct 2018 15:02:23 -0700
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-yw1-f44.google.com
Ironport-phdr: 9a23:u0UPsRbXkaopX0kqh1BJMzD/LSx+4OfEezUN459isYplN5qZoMS+bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b44XAucdJulYr4j9p0AOrRSgBgmnGf/iyjlSiX/wwKIxzuMsHhvd0wwgHtIOq3TUo8v2NKsIS++1yrPHzTPeYP9M2Df96ZTIch86rPGDWLJ/a8vRyU01GwzZiVWQrJXoMjWI3eoDtGib6vBvVeOpi2M/tw5xpSKvxsEyhYnNgoIZ0E7L+jhkwIszONa2S1Z7bMa6HJdMsyyWLYh7T8M4T211uSs216cKtJG0cSUM1Z8p3QTQa+adfIiN+h/jVPieITN/hH99fbKwnRey8Uy5xuz8WMi4zU9GriRKn9TDrHwN2BvT6s+ISvt54EitwyqA1wfW6u1cIEA0k7TUK4I5z7IuipYetV7PEyz2lUnskaObd1go9vKn5unoernmo4WTN45wigHwKKQuncm/DPwiPQcVX2ib+P+81L398k36WrlFlPs2nbPfsJ/HP8gbp6+5AxNa0os45Ba/Ci2p0NUcnXUdMF1FfxeHg5DzO17SOPD4Eeu/g1O0nTh3wPDGJ6TtDYnJLnjei7jsZq196k5ZyAor199T/ZNUCrcbIPLyQED9rtLYDgVqezCzlu3gEZB20p4UcWOJGK6Qdq3I4nGS4ed6CuOMZZQVtTW1Av4s4fKm2XYzmV4GfaSqm5IRYXa0WPVnP0qxbn/lg9NHGmAP6FltBNf2gUGPBGYAL025WLgxs2liWdCWSLzbT4Xou4SvmSKyH5lYfGdDUwneHnLhdoHCUPAJOnvLfp1R1wccXL3kcLcPkAm0vVajmbViJ+vQvCYfsMC7jYUn16jojRg3sAdMIYGd3mWKFTwmm2oJQ3onw/k6rxAhjFiE1qd8jrpTEtkBv/4=

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.

I do want computation rules on paths (I mean inductive constructors of equality). I don't understand how computation on paths violates UIP in the absence of univalence.

Is there an easy construction demonstrating the problem without needing to understand scary-sounding concepts such as homotopy pushouts.

- 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/

-- Abhishek

http://www.cs.cornell.edu/~aa755/

Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Abhishek Anand, 10/18/2018
- Re: [Coq-Club] coq + higher inductive types + proof irrelevance?, Steven Schäfer, 10/18/2018