coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Prop / Type (again)

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Prop / Type (again)
Date: Sat, 14 Dec 2019 13:01:54 +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=twUERYp9jvSbVNelYgxwZTf/9a/Uj5ZvdrDBpOLYngQ=; b=WQjXh+JdA9afaWlrIy8jlrQrcFr5gqeUEAbjcyNKNbKB5XlCqebXLinb2SJydn6949R0Fd2DTMuXIc1xyFIrwGkdygybLuGRu0gdM7Pfdh25Otl+K/z2XvvaCQ11eKllsg6ZSm4yNH5MCAwrxyMXN+Zm9RnsgLYBOzhFshyKElUJwtoG4bIKMAgpFFkDdK82giU0VvGHq1iBWTeznOQsZS6Hed6gNjlNmVTTP9IJRQW7nBSSZQkc5w4ptSl5NXNUPJgTd6H4hYMVbbfNwLaXxZB5xRkqkvhvJloEQbp+1hvI6OL+Ssv3wGNOHnsLeb5JowW8o7B8UmrTFZplgF6yCw==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=PyZO6bXORnSnlWT29CKZrr/Zbx0QGAYEAzm1NL+87hKFnTcD+3Dk8nFPml2wTJtkqfUdnQlLwNFB1gPy21//W/t9LxJPeoLlL7Qlnueo7I8+er1AiljMKH7bUmNYxNj1SIasMNxpWTuyrKOTC111sUUtig5PWeuSuAWvTblAmTGOX7K0JIDQiVpkSRKc3uCuijopbUyaPkOUzv6F2UGNNfodE0+1p27O9OhvYIIdLkB3e3onoQBvwWfZI0fQystKLZlfsRd5s4RD7V5HApaa8p3ThXC5r60k3Mj71lAkcOAM5hSZWu3CigA25yMkoMCgmZAjiOnHufQCECevxC58Pg==
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-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:QRzX3R1M/G4sMAwosmDT+DRfVm0co7zxezQtwd8ZseIeKPad9pjvdHbS+e9qxAeQG9mCsLQe07Od7/2ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbalsIBmqsAnducYbjIt/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+jLxVrg+9pxJxwIDUYZ2aOvVxca7GYdMVXnBMUtpNWyBdAI6xaZYEAeobPeZfqonwv18AogWkBQayAePuyiJDiHHs0qw0yOQhFgfG1xEnEtwKrnvUtsv6NKISUOyvwqfH1zvCb+hR2Tf784XHaBYhoeyWUb1ubMXR1FMjGBnYjliJr4HuIjCb1vwVvmWU8+ZsT/+jh3Ilpg1rvzSiyMYhhpPUio4J11zI7Sp0zYIvKdGlTEN2YcSoHIZQuiyZLYd6X90uTmJwtCY01LILuoK3cS0PxZkmxBPSaP2Kfo2I7x79T+meOjJ1i2l5d7+7iRa/9Eagxff/W8au1ltBszBLncPWtn8X0hze8siHReV5/kemwTuCyw7c5PxYLUwpjKbVLJEvzqMpmpoUqkvMADX6mELrjK+KbUok/fWo6+L6bbn8vp+cLYh0ih3gPasyhsy/AOM4Mg4UU2ic5OS8yLnj/Ur+QLVJlPE5jq7ZsJXCKcQaoK62HRNV354s5hqjFTuqzcgUkHsdIF5Ydh+KjpLlN0zSLPzlFfu/hk6jkDZvx/DIJL3hBZDNI2DHnrj/Z7Zy9UtcyQopwd5R/Z1VBKoBIPX1WkLqrtPYCAI5PxaqzOn6FdVxzJkRWX+XDq+DLKzSqUOI5v4oI+SUeIAVvy/9J+E56P7qkH82gkQQfbKp3JsScHC3BO5qI0SfYXr2g9cOC30GvgQkTL+itFrXGzVUfjO5W782zjA9EoOvS4nZDMj5i7uYmSy/A5d+Z2ZcC1nKH22+JKueXPJZSi+IL8pw2hANSqOmTcd19xy0uQrrjZZuMfHT/AURs4+l2dRooeTOw0JhvQdoBtiQhjneB1p/mXkFEmdvgfJP5Hdlw1LG6pBWxvxVEdsPuKFgbzxibNv54rU/DNr/HAXcYt2OVVCqBM28Bi08Rc4wxNlIZFthH9KljVbI2C/4WuZExYzOP4Q99+fn51a0Is98z3jc06x41QsvRNYJOGG7wKdipVGKW9z51n6BnqPvTpwymTbX/T7Zn2OIoQdVXBM2WLiXBX0=

Hi,

In contrast to my last query on this general topic, when it seemed that
(sometimes) Set, Type and Prop were interchangeable, here coq changes
Type in my definition to Prop, and so when singleton_rel is given as
argument to a function which requires its argument to be (... -> ... ->
Type), it fails.

(* this definition replaces Type by Prop - why?
Inductive singleton_rel U V u v : U -> V -> Type :=
| srI : @singleton_rel U V u v u v : Type.
*)

Thanks for any help

Jeremy

[Coq-Club] Prop / Type (again), Jeremy Dawson, 12/14/2019
- Re: [Coq-Club] Prop / Type (again), Gaëtan Gilbert, 12/14/2019
  - Re: [Coq-Club] Prop / Type (again), Jeremy Dawson, 12/15/2019