coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] universe inconsistency

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] universe inconsistency
Date: Mon, 13 Jan 2020 13:27:47 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=Xpfk5o3VK3dzqNezmPuJNg7S2sjg5MIyU4zvCbIGKmE=; b=DPMi9/Xugbk041SmNmLH85lRVpTlErYQFkaWkF9tFuk44dnEorA96Ybj+httLpCsGaZhPpKBFxgO62V5PZdJNeiESaZYsZGcOTbAlPVnMEf/tM5ST8ovRI3kgviebDQL7w/vU639kxmHig3EdQwaU4TJkxoRCxueW2mqbR5Dj/MPALyZy/BUANpjDoG5Eo3x6utXc9KHLWpfIzlTtxoj86UGR4xVil8jJogIm2duCmR8zvGV6jyak0yz7YhunwtTwNWxPJluFKIgstttJZ3mkC4NsoZieZkn2NQ/qmB+AVRv5+MjJlRFXRqDCX+uHEGIkCJwsEor00+5mHGy9QPOMA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=kr4sbi84zruD7m477VgpKhMjKENj+YItiI1NsQnUZ88GjPJO4OHoPw9BHmtO7ldpURYljkUkxYOk6mLCn0GSI6e1OONOTBsx8aLpT9u7KR9lhY1jHsunIj1/kX8nfW/nVxU24o6BcC69ee8K/81y/oH5/NYdSUxjvPUf2dEEIC2BQzY57b2PjU/Ur/EU9jSKHWYOkccTg6xccfbbvZ7PsgInHf7Halid2Y7A3Z7V/heAb0y/MVtM2FvtXzlHOyvaM0xT/+2eyeV1C7swzm7dHJH74T2c9ohYNB940r+EnLZK934PenZfsgdZTc22FpODqnbNgu8xqsz6DftKivb18w==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:eYoSexBnXtSiKBOQhNWBUyQJP3N1i/DPJgcQr6AfoPdwSPT5ocbcNUDSrc9gkEXOFd2Cra4d0KyM7PirBDRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfL1/IA+ooQjTqsUajotvJroswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9VoAyvqQFjw4DaY4+VOvhxfqLBct0VSmVMRdpRWDdbD4+gc4cDE+gMMOBFpIf9vVsOqh6+CBGoCuzx0D9HmHr23K0n2OovCw7H0hcgH9UIsH/Jq9j7MLkdUfqrw6nNzTTPdf1Y1i3z6YjTdRAhp+qBUqh2ccrM00UgCR7KjkiKpYP/IjOYz+IAuHWY4ep4Te+ihHIrpxtsrjSzxMogkJTFi4wXx1ze8Sh0wJ45KNK8RUJhfNKpFJtduzuHO4Z4Qc4uWWNltSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wr/WemfPDl0mG9pdKuiiRmw/0Ws0+r8WdKq31pQqSpFj8XMuWsK1xzO7MiIV+Fx/l+72TaIywDc9P1LIVw1larcLZ4t2LkwlocPsUTHGS/2n0b2gLWKeUUj/+ik8+XnYrP4qZ+AL4J5hR3yPr4zlsCjA+k0KBUCUmaZ9Oim0LDu/VX1QLBQgf03lqnZvoraJcMepqOhBwFazJwj5Ai6DzamytgWk2MILVxeeBKAiYjkIEvBIPblDfulnVujjSpry+rcMb38GpnNNGTMkK/9fbZh7E5R0BY8zddG555NFr4BJO/zVVTqudzDDh45NhS0zPz9BNV80IMeQ2OPDbWDPKPcq1/brt4odqOHY5ZQszLgIdAk4eTvhDk3gxVVKaKuxN4cbG2yNvVgOUSQJ3T21IQvC2AP6ygzVuHvmRWuWCFIYHD6C4Ax/Dw+GcSKBJjYQYaFibqcmiq3A9tfezYVWRi3DX70etDcCL83YyWIL5o5y2BWZf2aU4YkkCqWmkri0bM+dLjd/DBeuJ7+ktFotbWKyEMCsAdsBsHY6FmjCmF5mmRUGG0f4Zsn+AlG+wzG1qJ1xftFCdZU+vVFFB8gMoLRxPB7DNa0XR/detCOSxCtRdD0WGhgHOJ0+McHZgNGI/vnixnC2ySwBLpMze6CAoFy/67BmXHsdZ9w

And perhaps I could ask a further specific question:

what does it mean to insert the word Polymorphic in front of Inductive
seqrel? While it removes an error that occurs somewhere else, it
creates the error quoted in the code below

Thanks

Jeremy

> Unable to unify
> "seqrel@{Top.598 Top.602 Top.600} (singleton_rel ([], [Imp C D]) ([C],
> [D]))
> c2 x" with"seqrel@{Top.775 Set Top.772} ?R c2 x"
>
> what does seqrel@{Top.598 Top.602 Top.600} mean?

Re: [Coq-Club] universe inconsistency, Jeremy Dawson, 01/13/2020
- Re: [Coq-Club] universe inconsistency, Christian Doczkal, 01/13/2020
  - Re: [Coq-Club] universe inconsistency, Jeremy Dawson, 01/13/2020