fact: Definition seq_colim_sum_rec_beta_glue : 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.
imports: Basics Types Diagrams.Diagram Diagrams.Sequence Diagrams.Cocone Colimits.Colimit Spaces.Nat.Core PathAny