The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

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.