coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gert Smolka <smolka AT ps.uni-saarland.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Historical question related to K
- Date: Sat, 5 May 2018 11:30:41 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=smolka AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=smolka AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT thyone.hiz-saarland.de
- Ironport-phdr: 9a23:X6rwqBcuAHPSanCG97axsQKAlGMj4u6mDksu8pMizoh2WeGdxcS6Zx7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H3YhMN/g6xGrhyhqQJxzIzXbo+SL/d+YrrdfdYGSWpBQspcVSpMCZ68YYsVCOoBOP5VoYjjqFsUsRu1GBSiBOboyj9MhX/5x7Ax3uM6EQHD2wwgG9EOv27PodXtL6ceS/21zK/JzTnadPNZwy3y6JLMch87p/GDQKh8ftfPxkQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7+pnVeKqjG4ntwZxoiCvx8cwiojJnpwaykzE9Spnx4Y1P925RFR8Yd6+H5tdsTyROYhuQs46Xm1ltik3xqcCtJO6ZiQHyo4rywDRZvCZa4SF5hzuWPyMLTp8h39pYqyziha9/ES6yuDxVc+520tQoCVfiNnDrHUN2gTT6seZTvt9+V+s2SqP1wHT7eFEJ147mbDbK54gw788j4ETvl7ZES/snEX5lqmWeVg+9ue19evrerTmppmCOI9okgzyL6ojl8OlDek8MwUCRWqW9f6i2LDt40H1WLBKgec3kqndvpDaP8MbpquhDg9O14Yj7BK/DzS839kDhXkHN0hJeA+Bj4joIl3OO+r3Au2lg1Soijhrwe3JMqf8DZrTNnTDiqvufa5h605Azwo+1cxQ55VNCr0YPP3zXlLxu8fDAx8iMw20xv7nB89n2oMfX2KPGK6ZP7nIvV+G/OJ8a9WLMYQSoXP2L+Uvz//ol34w31EHLoez2p5CR32iArxdJkKdYnOk1swEFmMJtyImV6r3jlzHSjdafXK7Wa566jxtW9HuNpvKWo342O/J5yy8BJADPjkXWGDJKm/hcsC/Y9lJbSuTJsF7lTleDeq5UMk80xDrrwbz0b5uKOaS9iBK7Mu/hugw3PXakFQJzRIxF96UiTnfV3oyg2UJAiQ/1bp7qEpxjFuOg/Ah3q5oUOdL7vYMaT8UcJ7Ry+sgV4LuWhPGeNrPSFe0B86vCCs1R9Q9hdMDMR5w
Sorry for the silly question, the answer can be found here, for instance:
https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/
In short: UIP does not follow from the elimination scheme from eq, as proved
by Hofmann and Streicher.
A surprising and counterintuitive fact at first, one could call Streicher’s
paradox.
Gert
> On 4. May 2018, at 17:01, Gert Smolka
> <smolka AT ps.uni-saarland.de>
> wrote:
>
> I have a historical question regarding elimination
> for inductive predicates with indices in Coq.
> What was the reason for providing only weak elimination that,
> for instance, cannot derive UIP?
>
> I know that UIP conflicts with univalence, but univalence wasn’t there
> when Coq was designed.
>
> Thanks for answers,
> Gert
>
> PS: Two example may help to make my point:
>
> Section UIP.
> Variable X: Type.
> Variable x: X.
>
> Inductive eq : X -> Prop := Q : eq x.
>
> Goal forall p: eq x -> Type,
> p Q -> forall y, p y.
> Proof.
> refine (fun p H y => match y with Q => _ end).
> Abort all.
> End UIP.
>
> but the following goes through:
>
> Inductive unit: Prop := U: unit.
>
> Goal forall p: unit -> Type,
> p U -> forall x, p x.
> Proof.
> refine (fun p H x => match x with U => _ end).
> exact H.
> Qed.
- [Coq-Club] Historical question related to K, Gert Smolka, 05/04/2018
- Re: [Coq-Club] Historical question related to K, Gert Smolka, 05/05/2018
- Re: [Coq-Club] Historical question related to K, Thorsten Altenkirch, 05/05/2018
- Re: [Coq-Club] Historical question related to K, Gert Smolka, 05/05/2018
Archive powered by MHonArc 2.6.18.