The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

The README links to the article giving background of the design of the 
library.
These issues are documented in sec6 here:
https://arxiv.org/abs/1610.04591

I'm not sure copying them to the README would clarify things.

On Sun, Feb 28, 2021 at 10:40 AM Vincent Semeria
<vincent.semeria AT gmail.com> wrote:
>
> Hi Hugo.
>
> Is indices-matter the only compiler switch in HoTT that makes it different 
> from standard Coq? It would be good to list all those switches in HoTT's 
> readme page
> https://github.com/HoTT/HoTT
> which currently only says
> "The HoTT library is a development of homotopy-theoretic ideas in the Coq 
> proof assistant."
>
> On Tue, Feb 23, 2021 at 4:03 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> 
> wrote:
>>
>> [Coq-Club] Parametricity Axiom
>> Reply-To:
>> In-Reply-To: 
>> <DB7PR06MB59609EB3EBDF565194064FDCA4809 AT DB7PR06MB5960.eurprd06.prod.outlook.com>
>>
>> Hi,
>>
>> Indeed that would be the case in HoTT but the thing here is that Coq
>> is unfortunately not "fully compatible" with HoTT, even with Prop =
>> HProp in mind, since by default, "indices do not matter": in vanilla
>> Coq, all equalities land in Prop, even say "bool = bool", while, to
>> comply with HoTT, equality should not be Prop-truncated. [To avoid
>> Prop-truncation, there is the option -indices-matter (used in the HoTT
>> library). In particular, it prevents proof-irrelevance to imply
>> UIP_refl.]
>>
>> Incidentally, there is an idea in the air to make Coq compatible with
>> univalence (and classical logic) without having to switch option
>> -indices-matter on. This would be to reinterpret each existing Type(n)
>> as HSet(n) and to add a new hierarchy, say Univ, standing for the
>> usual Martin-Löf's universes, so that indices matter can be on by
>> default without incompatibilities. Then, univalence would be stated in
>> Univ. I don't know what others think.
>>
>> Best,
>>
>> Hugo
>>
>> On Tue, Feb 23, 2021 at 01:44:26PM +0000, Thorsten Altenkirch wrote:
>> > No it doesn't as long as Prop means HProp (at most one inhabitant). 
>> > Classical logic is consistent with univalence.
>> >
>> > This is different if you say "forall P : Type, P \/ ~P, because then you 
>> > can use Hedberg's theorem to show that all tyoes have a propositional 
>> > equality and this does contradict univalence.
>> >
>> >
>> >
>> > On 20/02/2021, 22:06, "coq-club-request AT inria.fr on behalf of Daniel 
>> > Schepler" <coq-club-request AT inria.fr on behalf of dschepler AT gmail.com> 
>> > wrote:
>> >
>> >     On Fri, Feb 19, 2021 at 4:34 PM Maximilian Wuttke 
>> > <mwuttke97 AT posteo.de> wrote:
>> >     > >   Variable classic_dec : forall P : Prop, {P} + {~P}.
>> >     > >   Variable UIP_refl : forall (X : Type) (x : X) (H : x = x), H = 
>> > eq_refl.
>> >
>> >     Incidentally, classic : forall P : Prop, P \/ ~P implies proof
>> >     irrelevance, and therefore as a corollary classic_dec implies
>> >     UIP_refl.
>> >     --
>> >     Daniel Schepler