(A : Type) : Sequence. Proof. srapply Build_Sequence. 1: exact (iterated_join A). intros n. exact joinr. Defined.
Require Import Basics Types. Require Import Diagrams.Sequence. Require Import Homotopy.Join.Core. Require Import Colimits.Colimit Colimits.Sequential.