coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
>
- [Coq-Club] what does this error message mean?, Andrew Polonsky, 03/13/2013
- Re: [Coq-Club] what does this error message mean?, Hugo Herbelin, 03/14/2013
Archive powered by MHonArc 2.6.18.