coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Parametricity Axiom

From: Thorsten Altenkirch <t.altenkirch AT googlemail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Parametricity Axiom
Date: Tue, 23 Feb 2021 13:44:26 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=t.altenkirch AT googlemail.com; spf=Pass smtp.mailfrom=t.altenkirch AT googlemail.com; spf=None smtp.helo=postmaster AT mail-wr1-f43.google.com
Ironport-phdr: 9a23:aV6RshfLzZ9xlmkjPPUJPVGjlGMj4u6mDksu8pMizoh2WeGdxcW7bR7h7PlgxGXEQZ/co6odzbaP4uawBSdZu87JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRG7oR/Su8QZjoduN7g9xgfUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vpwJxzZPIYI+bN/R+cKHScs8VS2VORctRSzdODYygY4cTE+YMP+BVpJT9qVsUqhu+ABGhCv3vyj9PnH/2xrE63PonEQrbwAEgG84Ov2rSrNX2NacSS/y6zKnVxjjEc/Nawy3y6IzUch8/p/GMXrNwcdDNxkkvDA7FgVKQqYvqPzORyOsNtnKU7+tkVe61l2EnrARxryGpy8wxhYbHmpgbxUrY9SVl3ok1P9u4RVZ4bNOgEJVduDyXOoV1T84mQmxkpic3xqEatZC0fSUHyIoqywDbZvKId4WF5hLuWfuMLTl4inxoZrKxihas/ES8zOD3S8q60E5SoyZbjtXBsmoB2h/T58SdVPdx4Fqt1SyA2g3d8u1IP0E5mbbVJpMk37I8ioQfvEXGEyDqhEn6kqqbelsn9+Wo9ejqZ7Drq5+aOoRpkA/xKL4ulda6AekgMggBQWyb+eOk2b3m50L5QbFKguQ4k6nDrZzWPMobq6G3DgNP3YYj7BG/Dzii0NsGh3UIMFVFeBefg4joPVHBPuz4AO+hj1iwlDpn3fPLM737DpnTMHTPja3tcLlz5kJEzQo819Ff55ZaCrEbJ/LzX1f8tMDCAhAjNwy03/joCNN+1oMfQ2KAHq+ZPbjdsV+P4eIvLO2Ma5EQuDnnKvgl4+TigmM+mV8YZaWpx4cYaGikHvR6JEWUeWbjgtAYEWsTogU+SPHqh0aZXD5IZ3eyWro86SshBIKnC4fDXIGtj6ab0Ce1BJ0FLlxBXxqHFm6tfIGZUd8NbjiTK4lviHZMAbOmUsoq0QyknA780btuaOTOrH42r5XmgeR14PfIiRw0vRVwE8mb0GCXRGE8yn9OTjsq0aZ8oFZ2yn+M1q93h/FdHN1XofhOV1FpZtbn0+VmBoWqCUr6ddCTRQP+G4n0MXQKVts0huQ2TQNlAdz70ELM2C2lB7IQnr2PQpcz9/CEhiWjF4NG03/DkZIZoRwmT89IbzD0g6d+803MHdeMnRnC0amtcqsY0WjG82LRlTPf7nEdaxZ5VOD+ZV5aY0LXqdrj4UabEe2hDrMoNgZEwM+GbKBNb4+wgA==

No it doesn't as long as Prop means HProp (at most one inhabitant). Classical
logic is consistent with univalence.

This is different if you say "forall P : Type, P \/ ~P, because then you can
use Hedberg's theorem to show that all tyoes have a propositional equality
and this does contradict univalence.

On 20/02/2021, 22:06, "coq-club-request AT inria.fr on behalf of Daniel
Schepler" <coq-club-request AT inria.fr on behalf of dschepler AT gmail.com> wrote:

On Fri, Feb 19, 2021 at 4:34 PM Maximilian Wuttke <mwuttke97 AT posteo.de>
wrote:
> > Variable classic_dec : forall P : Prop, {P} + {~P}.
> > Variable UIP_refl : forall (X : Type) (x : X) (H : x = x), H =
eq_refl.

Incidentally, classic : forall P : Prop, P \/ ~P implies proof
irrelevance, and therefore as a corollary classic_dec implies
UIP_refl.
--
Daniel Schepler

Re: [Coq-Club] Parametricity Axiom, (continued)