`{Funext} (A : Sequence) (P : Type) `{IsHProp P} : (Colimit A -> P) <~> (forall n, A n -> P). Proof. symmetry. refine (equiv_colimit_rec P oE _). refine (issig_Cocone _ _ oE _). symmetry. srapply Build_Equiv. 1: exact pr1. exact _. 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.