Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] what does this error message mean?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] what does this error message mean?


Chronological Thread 
  • From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • To: Andrew Polonsky <andrew.polonsky AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] what does this error message mean?
  • Date: Thu, 14 Mar 2013 00:45:51 +0100

Hi Andrew,

You are apparently using HoTT Coq which includes an experimental
ongoing development of full universe polymorphism. Released Coq raised
a regular strict positivity error with respect to this example. For
support, you'd better report to the HoTT Coq mailing list.

Enjoy HoTT however!

Hugo

On Wed, Mar 13, 2013 at 04:12:26PM -0400, Andrew Polonsky wrote:
> Definition obs (Phi: Type -> Type -> Type) {A:Type} (a a': A) : Type :=
> forall P : A -> Type, Phi (P a) (P a').
>
> CoInductive eq (A B: Type) : Type :=
> | cons (f:A->B) (g:B->A)
>        (eta: forall (a:A) (b:B),
>                   (eq (obs eq a (g b)) (obs eq b (f a)))
>                 * (eq (obs eq b (f a)) (obs eq (g b) a)))
>        : eq A B.
>
>
>
> Anomaly: Trying to substitute an algebraic universe where only levels are
> allowed.
> Please report.
>



Archive powered by MHonArc 2.6.18.

Top of Page