coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about inhabited

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about inhabited
Date: Fri, 28 Apr 2017 14:17:13 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f170.google.com
Ironport-phdr: 9a23:H+tz0xAhzR6Q+Vd601BcUyQJP3N1i/DPJgcQr6AfoPdwSPvzpcbcNUDSrc9gkEXOFd2CrakV16yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMizexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzZhMx3j6xUrh2uqABwzYPPfIGVLeBzcr/Bcd4AR2dMWNtaWSxbAoO7aosCF+QNM+Jfr4n9oVsFsBuxBQiyC+Pgzj9HmH/30aMn2OkmEwHG2wwgH9QAsXnPqtX6KqkTXvqvzKnUzDXDdOlZ2THm6ITSbh8hpvSMUKt2fMHMx0cvEAbFgU+RqYzjJz6V0PoCsmaB4Op6SeKvinUnpBt3oji03Msjlo7JhocTx1vZ9it52J44KcOkREN/e9KpE5tduzuHO4ZyXM8uWXxktSQmxrEeu5O3YDIGxIo6yxPQcfCKfYuF7gj+WOufLzp1gm9udqiliBao60egz/XxVsmq31ZOqSpIitzMuWoM1xzX88SHUvV98lu41TaBygze6P1ILVo7larcLJ4hzbowmYQJvUvfGS/2nV36jK6Qdko65uil8/rrbqniq5OGNIJ5ihvyPrkql8ChG+g0LwoDU3SD9eS5zrLj/En5QLtQjv0xl6nUqJLaJMoapqGnDA9V1pgs6hakAjep1dQXh3gHLFZfdB2biIjpPknCIOrkAvenn1SsjDBryujaMb3mG5XBN2TMkLP8fblm8ENc0woyzdVH551OEL0BIfTzWlXwtNPCFBM5PRa0kK7bD4B20ZpbUmaSCIeYNrnTuBmG/LEBOe6JMcU3vzb7Y8ck6vHqgG5z0QsfeqmvwrMRZW+xBOhnOEyfejznhdJXQjRChRY3UOG/0A7KajVUfXvnB68=
Organization: New Artisans LLC

Is there any way to prove the following, or reduce it to a consistent axiom?

Theorem inhabited_forall :
∀ A (P : A -> Type), (∀ x, inhabited (P x)) -> inhabited (∀ x, P x).

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Question about inhabited, John Wiegley, 04/28/2017
- Re: [Coq-Club] Question about inhabited, Gaetan Gilbert, 04/28/2017
  - Re: [Coq-Club] Question about inhabited, John Wiegley, 04/29/2017