coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Parametricity Axiom

From: Maximilian Wuttke <mwuttke97 AT posteo.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Parametricity Axiom
Date: Sun, 21 Feb 2021 00:53:56 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mwuttke97 AT posteo.de; spf=Pass smtp.mailfrom=mwuttke97 AT posteo.de; spf=None smtp.helo=postmaster AT mout01.posteo.de
Ironport-phdr: 9a23:vcUjZxXcxvHQ/3quXAqml+5iSFXV8LGtZVwlr6E/grcLSJyIuqrYbBWBt8tkgFKBZ4jH8fUM07OQ7/mxHzNRqs3b+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiyoAnLtMQbhYRuJ6gvxhDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuA+vqQJxw4DUY4+bOvRxcazfctwGSmRMRdpRWi5bD4+gc4cCAegMMOBFpIf9vVsOqh6+CBGrCuz1xT5Ih3r23aw+0+QgCw7G2hErENITsHTIsNX1N7kdWv2ywanNwzTDcu9W2Sv+6IfWdh0so+qBXap3ccrK1UkgCQTFgk+NpoP7Jj6Y0PkGvGeH4eR6T+2vl3InpB9rojip3sohlInHi4wax1zY+yh13YQ4KN24RUB7fNOpEIdduj+eOoZ4QM4sTWFmtDs7x7AGp5K2cjQGxZY7yhPeavGKfIaG7xT+X+iSOTd1nG9pdbG/ihqo8EWtyPfwW8e13VpQrydIksHAu3MJ2hDJ98SKRfpw8l2/1TqRywzf8PxILE4omafdNpUv2KQ/loAJvkTGBiL2mFv5jKuRdkg8/+io7PnnYqn6qpOBLYN0kgb+Mr8ymsOhBuQ0KBUBUHaD9eS90r3s41H5Ta1XgvA1kqTVqpHXKMYBqqO3AgJZyIcu5hanAzejytsYnH0HLFxfeBKAiojkI1TOIf7lDfejn1SskylkyvTEM7D6GpXNKWPDkKv/crZ68UJT1RQ8wchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgzYwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zFQaZOyi2YYdQHG+BPVvZUuDMlT2hdJUNG4avw8/SO3jjhW9TCJPZHv6C6cj+y0nC4/3Uq/bQZuxjbvH0CrtTc4eXXxPFl3ZSSSgTI6DQfpZMHvDcP8kqSQNUP2ac6Fk0BivsAHgzL8+d7jM/TYEuJWl2NUnvrSPxyF3ziR9CoGm60/IV3t9xzpaXzgtwK1450BwmA/ajPpIxsdAHNkW3MtnFwc3MZmFn75/DM3uAluHZtCSVFuhBNmrU2k8

On 19/02/2021 16:18, Hugo Herbelin wrote:
> So, using Set instead of Type would prevent the counterexample? Hugo

Well, actually the counterexample by Daniel Schepler only works for Set
and not for Type, due to a universe inconsistency:

> Variable classic_dec : forall P : Prop, {P} + {~P}.
> Fail Check forall (X : Type), classic_dec (bool = X).
> (* The term "X" has type "Type" while it is expected to have type Set *)

I think this is because bool has sort Set and we thus can't compare bool
and Type. I don't know enough about universes, but maybe there is
something like a universe polymorphic version of bool, such that this
equality is well-typed?

[Coq-Club] Parametricity Axiom, Maximilian Wuttke, 02/18/2021
- Re: [Coq-Club] Parametricity Axiom, Dominique Larchey-Wendling, 02/18/2021
  - Re: [Coq-Club] Parametricity Axiom, Maximilian Wuttke, 02/19/2021
    - Re: [Coq-Club] Parametricity Axiom, Dominique Larchey-Wendling, 02/19/2021
    - Re: [Coq-Club] Parametricity Axiom, Pierre-Marie Pédrot, 02/19/2021
      - Re: [Coq-Club] Parametricity Axiom, Hugo Herbelin, 02/19/2021
        
        Re: [Coq-Club] Parametricity Axiom, Maximilian Wuttke, 02/21/2021
        
        Re: [Coq-Club] Parametricity Axiom, Christian Doczkal, 02/21/2021
      - Re: [Coq-Club] Parametricity Axiom, Maximilian Wuttke, 02/19/2021
        
        Re: [Coq-Club] Parametricity Axiom, Daniel Schepler, 02/20/2021
        
        Re: [Coq-Club] Parametricity Axiom, Maximilian Wuttke, 02/20/2021
        
        Re: [Coq-Club] Parametricity Axiom, Daniel Schepler, 02/20/2021
        Re: [Coq-Club] Parametricity Axiom, Thorsten Altenkirch, 02/23/2021