The Coq mailing list

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

Hi,

Thanks for the reference. If I understand correctly, it relies on
classical logic in the meta-language, right (their step "we decompose
Γ (...) and work over each component separately"), but even so, it is
reassuring that we are not doing anything wrong wrt to a trusted
meta-language which has the same feature as the one we want to
justify.

In an alternative direction, I remain optimistic that an intrinsic
relative-consistency-style justification (i.e. syntactic models)
leading to a type theory with computational classical logic can
eventually be found (renouncing to the "observable effect" criterion
of Pédrot-Tabareau's triangle of fire, by using an impredicative type
theory as target, as well as bar recursion techniques and Krivine's
"quote").

Best,

Hugo

On Sun, Feb 28, 2021 at 02:54:32PM +0100, Bas Spitters wrote:
> Chris and Peter once worked out the interpretation of Prop in the
> simplicial model. It is consistent with classical logic:
> https://arxiv.org/abs/2006.13694
> 
> On Sun, Feb 28, 2021 at 2:42 PM Pierre-Marie Pédrot
> <pierre-marie.pedrot AT inria.fr> wrote:
> >
> > On 28/02/2021 13:57, Hugo Herbelin wrote:
> > > 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).
> >
> > I am not an expert of the various cubical models out there, but they are
> > all based on presheaf semantics. There is a straightforward
> > interpretation of impredicative Prop as a degenerate universe of
> > (proof-irrelevant) presheaves. Since Prop-valued presheaves are quite
> > degenerate it should actually be *easier* to equip them with the
> > required glueing structure.
> >
> > I'd be curious to see if somebody already studied this in detail.
> > Unfortunately the Swedish school of intuitionistic mathematics is not
> > very fond of impredicativity, so it's not the kind of stuff they would
> > usually consider :/
> >
> > PMP
> >