Coq for HoTT: proving || P-> X || -> (P-> ||X||)

Question

I need to prove in Coq that for any type X and any proposition P (though I think it should work even if P is a type) there exists

trunc_impl: || P-> X || -> (P-> ||X||)

where ||_|| is the symbol used in HoTT book to indicate propositional truncation.

I demonstrated the statement in type theory: one gets the thesis by using the induction principle of propositional truncation, assuming from an H : || P-> X || and a p: P that H=|H'|, with H': P->X , and then defines trunc_impl(p):= |H'(p)|. (|-| indicates the constructor for the trucation, i.e. |_| : A -> ||A||).

By the way, I cannot write it in Coq! Any help would be very appreciated.

I am using the HoTT library available on GitHub.

Answer 1

You need to Require Import Basics. since coq doesn't know Trunc.TruncType can be coerced to Type otherwise. The tactics that you want to be aware of are apply Trunc_ind which will act on a goal like forall (x : Tr _ _), _.

intros x y and revert x will come in handy to get the goal into a form you want to apply trunc_ind to .

You also have the (custom) tactic strip_truncations which will search the context for any terms that are wrapped up with a truncation and try to do induction on them to remove them. This requires the goal to be as truncated but that shouldn't be a problem here.

Finally, the constructor for truncations is tr, so you can use apply there.