The Coq mailing list

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

So, using Set instead of Type would prevent the counterexample? Hugo

On Fri, Feb 19, 2021 at 03:20:36PM +0100, Pierre-Marie Pédrot wrote:
> Hi Maximilian,
> 
> On 19/02/2021 00:18, Maximilian Wuttke wrote:
> > Let's consider the easy case ϕ1=ϕ2=0 again (where I simplified `Vector.t
> > X 0` to unit):
> 
> I think that your theorem is false even with the unit type as argument,
> because of universes. There is a counter-example in the introduction of
> the Nuyts et al. paper "Parametric Quantifiers for Dependent Type Theory",
> 
> http://publications.lib.chalmers.se/records/fulltext/252073/local_252073.pdf
> 
> PMP
>