{A : Sequence} (a : A 0) k : (0;a)^++k = (k;a^+k). Proof. induction k as [ | k q]. - reflexivity. - exact (ap seq_pair_shift 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.