{A : Sequence} E (F G : Colimit A -> E) (h : forall n, F o inj A n == G o inj A n) (H : forall n a, ap F (glue A n a) @ h n a = h n.+1 a^+ @ ap G (glue A n a)) : F == G. Proof. srapply (Colimit_ind _ h); intros n m p a; destruct p. generalize (H n a); generalize (h n a); destruct (glue A n a). intros p q; srefine ((concat_p1 _)^ @ _); srefine (_ @ (concat_1p _)); exact q^. 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.