`{Funext} (A P : Type) `{IsHProp P} : (PropTrunc A -> P) <~> (A -> P). Proof. refine (_ oE equiv_colim_seq_rec _ P). srapply equiv_iff_hprop. { intros h. exact (h 0). } intros f. induction n. - exact f. - cbn. srapply Join_rec. 1,2: assumption. intros a b. rapply path_ishprop. Defined.
Require Import Basics Types. Require Import Diagrams.Sequence. Require Import Homotopy.Join.Core. Require Import Colimits.Colimit Colimits.Sequential.