(A : Sequence) (a1 a2 : A 0) := Build_Sequence (fun k => a1^+k = a2^+k) (fun k p => ap (fun a => a^+) p).
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.