coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] question about universes and equalities
- Date: Sun, 8 May 2016 14:10:11 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f54.google.com
- Ironport-phdr: 9a23:pP+D1RyA9/S0HzfXCy+O+j09IxM/srCxBDY+r6Qd0e0SIJqq85mqBkHD//Il1AaPBtWKrascwLOM6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6DyZ3vnLnoo9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjUSrY9RTSr6e9PRR72hSEbf2o792fWicF0ga9zrxeophg5yInRNtLGfMFid7/QKItJDVFKWdxcAmkYWtux
I'm hitting some problems that I think are related to equalities in different universes. For example, consider:
Goal forall S1 S2:Set, @eq Type S1 S2 -> @eq Set S1 S2.
Is this provable in Coq? If not, then does that mean it is possible to have two Sets in Coq such that they are (@eq Type) but not (@eq Set)? What would that possibly mean?
-- Jonathan
- [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/08/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/08/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/08/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/08/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Matthieu Sozeau, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Matthieu Sozeau, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/08/2016
- Re: [Coq-Club] question about universes and equalities, Stefan Monnier, 05/09/2016
- Re: [Coq-Club] question about universes and equalities, Jonathan Leivent, 05/08/2016
- Re: [Coq-Club] question about universes and equalities, Jason Gross, 05/08/2016
Archive powered by MHonArc 2.6.18.