`{Univalence} {A : Sequence} n (a1 a2 : A n) : (inj A n a1 = inj A n a2) <~> Colimit (path_seq (shift_seq A n) a1 a2). Proof. srefine (transitivity _ (equiv_path_colim_zero _ _)); symmetry. srapply (@equiv_ap _ _ (colim_shift_seq_to_colim_seq A n)). 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.