In Homotopy Type Theory there exists a function:
|| P + ~P || -> P + ~P,
for any mere proposition P (||_|| denotes the propositional truncation). This function is defined by proving that P + ~P is a mere proposition and using the propositional truncation elimination principle.
An equivalent in the Coq (without the HoTT library) would be:
Conjecture or_to_sumbool : forall P : Prop, P \/ ~P -> { P } + { ~P }.
It cannot be proven in a straightforward manner, because case analysis on a disjunction is forbidden when the goal has sort Set. Is there any way of proving this statement in Coq or is it impossible?
In Homotopy Type Theory there exists a function:
|| P + ~P || -> P + ~P,
for any mere proposition P (||_|| denotes the propositional truncation). This function is defined by proving that P + ~P is a mere proposition and using the propositional truncation elimination principle.
An equivalent in the Coq (without the HoTT library) would be:
Conjecture or_to_sumbool : forall P : Prop, P \/ ~P -> { P } + { ~P }.
It cannot be proven in a straightforward manner, because case analysis on a disjunction is forbidden when the goal has sort Set. Is there any way of proving this statement in Coq or is it impossible?
I know that names are a bit confusing for newcomers, but Prop is not the counterpart of hProp of HoTT in Coq.
Prop corresponds to what can be erased at extraction. So if you could eliminate P \/ ~P to {P} + {~P} you would extract computational content from sth that is going to be erased, so it does not work.
To do HoTT in Coq, you need axioms, which is fine as long as you stay consistent. There are a few libraries that do that, like the Coq-Hott library or the Unimath library.