The Coq mailing list

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

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.
>