The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/28/2016 10:26 PM, Jason Gross wrote:
> Have you considered LEM on hProps?
>    forall P, (forall x y : P, x = y) -> P \/ ~P
> Together with propositional truncation / quotient types, this may give you
> want you want.  (I think these are similar to your irrelevant_sibling; you
> do:
>    Module Export Trunc.
>      Private Inductive PropTrunc A := tr : A -> PropTrunc A.
>      Axiom PropTrunc_trunc : forall {A} (x y : PropTrunc A), x = y.
>      Definition Trunc_ind {A}
>        (P : PropTrunc A -> Type) {Pt : forall x y, P x = P y}
>      : (forall a, P (tr a)) -> (forall aa, P aa)
>      := (fun f aa => match aa with tr a => fun _ => f a end Pt).
>    End Trunc.
> )
> Does this do what you want?

So, this relies on the semantics of Private to prevent 
discrimination/destruction of PropTrunc instances outside the module.  
This trick scares me a bit.  Does native_compute always obey this 
restriction?  It disobeys opaqueness, so that's why I'm suspicious.  How 
does this mix with extraction - will PropTruncs get erased as well as Props?

As for having an induction scheme - that might be useful...

-- Jonathan