The Coq mailing list

[Steven Schäfer <s.schaefer89 AT googlemail.com>]

I don't remember what I had in mind, but I'm almost sure that it was wrong.

For example, in the presence of UIP, the unit type satisfies the induction principle for the circle (trivially, since "base = base" is equivalent to "unit"). So in fact, the opposite should be true: in the presence of UIP, the path computation rules hold vacuously, since paths are proof irrelevant...

Am Do., 18. Okt. 2018 um 00:03 Uhr schrieb Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

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/