{A} : A -> PropTrunc A := colim (D:=Join_seq A) 0.
Require Import Basics Types. Require Import Diagrams.Sequence. Require Import Homotopy.Join.Core. Require Import Colimits.Colimit Colimits.Sequential.