`{Funext} A n : Colimit (shift_seq A n) <~> Colimit A := Build_Equiv _ _ (colim_shift_seq_to_colim_seq A n) _.
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.