The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

Maybe others know better, but I'm not aware of inconsistencies between
Coq's impredicative Prop and Homotopy Type Theory (the latter being
taken in the sense of Martin-Löf's type theory + univalence + HITs,
possibly extended with resizing, classical logic, axiom of choice, as
discussed in the HoTT Book). From what I'm aware of, my own bet is
that HoTT and Prop-impredicativity is not a problem and that what
makes hesitating is more that it is understudied territory, i.e. that
the relations between propositional resizing, impredicativity,
hProp-truncation, Prop-truncation, sProp-truncation, classical logic,
etc. need to be investigated more.

In particular, not using Prop in the HoTT library is to my eyes more a
design choice than a real constraint.

Making HoTT compatible with Coq prelude (e.g. by rethinking the
intended model of Type as a hierarchy of hSet and adding a new
univalent hierarchy, as in my previous mail) would have some
advantages as HoTT is one of these developments which contains quite a
lot of contents worth being considered as standard (starting with
useful basic notations, basic properties of equality, basic category
theory, ...).

[More generally, I don't know exactly how to proceed to collect
standard contents dispatched here and there into a single collective
ideally unified place, but it seems to me that for the benefit of the
whole Coq ecosystem, this is something that needs to be done.]

Best,

Hugo

On Sun, Feb 28, 2021 at 11:31:57AM +0100, Vincent Semeria wrote:
> Copying section 6 in the readme would clarify things indeed. The readme is
> currently misleading, because Coq without Prop and without the standard 
> library
> is not Coq.
> 
> Besides section 6 can be rephrased shortly, with something like "HoTT is not
> compatible with Coq's Prop sort, so equality was redefined in sort Type
> (compiler switch indices-matter) and the standard library is not usable".
> 
> On Sun, Feb 28, 2021 at 11:06 AM Bas Spitters <b.a.w.spitters AT gmail.com> 
> wrote:
> 
>     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
>