coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Strange subtyping

From: Helmut Brandl <helmut.brandl AT gmx.net>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Strange subtyping
Date: Thu, 7 Jun 2018 09:31:57 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-phdr: 9a23:yZMOgBIfzBgStBdEJtmcpTZWNBhigK39O0sv0rFitYgRLvjxwZ3uMQTl6Ol3ixeRBMOHs68C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwVFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygdNzA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoGyYJULD+oEIOZYs5T2qkYUrRSkAwmjGefvwSJPi3/2w6I61+EhERza3AA6BN0Oqm7brNPoO6cWSu21w6zIzDrZY/NQxzj99JHFfxY8qv+PRbJ9adTdxVQxGw/fkFmct47oMymI2ukPqWSX8fZsWfqthmMosQ19vyajy8c2hoTKmI4Z0FDJ+Tt/zY0oP9O3UlR7bsShEJZItyGVKY92QsQ6TmFtvyY616EGtYS0fCgPx5Ur3RjfZOKbc4SQ4xLjUvieIStgiX57Zb6zmQy+/Va+xuD+TMW4zVRHojBbntXQrnwN0gbc6smDSvtz5Eeh3jOP2hjT6u5aJUA0kLfbK4I7zrErjJocq0LDETLymEjtg6+Wc0ol9vKu6+v5frXqvoWcOJNsigHiLqQundSyDvg/MggXRmSU5eC81KD48kDiW7VLjvg2krHDv5zAJMQboLS5Aw5P3Yo55Ra/FWTu7NNNtn4eaXlBZRjP24PuIhTFJO3yJfa5mVWl1jlxkaP8M6XlE6nKe3jOlLL8YfB38UdaxA4bwtVPoZRZFuIvOvX2D2/8sNnFElcTKQWyz+KvXNVw0oYDRSSFGKafPKf6vlqYoOQiP7/fN8cupD/hJq19tLbVhngjlApFJPj77d4scHm9W89eDQCcaHvojM0GFDZYsQ8uCurnlA/bCGIBVzOJR6s5owoDJse+F46SFI+okPqH0TvpRsQLNFADMUiFFDLTT6vBW/oIb3vOcMpmjyBCWr2xDYksyUP2uQ==

Hi.

I am confused by a subtyping rule mentioned in chapter 4.4 of the reference manual.

It says that Prop is a subtype of Set. I checked it with the identity function

Definition id {T:Set} (x:T):= x.

And indeed the _expression_ "id I" is well typed.

I always thought that both Set and Prop are subtypes of Type(i) for any i but are not related in the subtyping relation.

What is the reason for this subtyping rule? Can anybody explain?

Thanks

Helmut

[Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Matthieu Sozeau, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
    - Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
      - Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
        
        Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/09/2018
    - Re: [Coq-Club] Strange subtyping, Théo Zimmermann, 06/09/2018
      - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/15/2018