proposition: Lemma equiv_colim_seq_rec `{Funext} (A : Sequence) (P : Type) `{IsHProp P} : (Colimit A -> P) <~> (forall n, A n -> P).
proof: Proof. symmetry. refine (equiv_colimit_rec P oE _). refine (issig_Cocone _ _ oE _). symmetry. srapply Build_Equiv. 1: exact pr1. exact _. Defined.
imports: Basics Types Diagrams.Diagram Diagrams.Sequence Diagrams.Cocone Colimits.Colimit Spaces.Nat.Core PathAny