forall n a b, ap seq_colim_sum_rec (ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n (a;b))) = t n a b. Proof. intros n a b; srapply (cancelL _ _ _ ((apD_const _ _)^ @ _)). srapply seq_colim_sum_ind_beta_glue. 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.