The Coq mailing list

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

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.