`{Funext} (A : Sequence) : (forall k, Contr (A k)) -> Contr (Colimit A). Proof. intro h_seqcontr; pose (unit_seq := Build_Sequence (fun _ => Unit) (fun _ _ => tt)). srapply (contr_equiv' (Colimit unit_seq)). - symmetry; srapply equiv_functor_colimit. srapply Build_diagram_equiv; srapply Build_DiagramMap. * exact (fun _ _ => tt). * intros n m p a; destruct p; reflexivity. - srapply (Build_Contr _ (inj unit_seq 0 tt)); intro y; symmetry; revert y. srapply seq_colimit_uniq. * intros n a; destruct a; induction n as [ | n r]. + reflexivity. + exact (glue unit_seq n tt @ r). * intro n; destruct a; rewrite ap_idmap, ap_const, concat_p1; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Sequence. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Spaces.Nat.Core. Require Import Homotopy.IdentitySystems.