`{Univalence} {A : Sequence} (a1 a2 : A 0) : (inj A 0 a1 = inj A 0 a2) <~> Colimit (path_seq A a1 a2). Proof. pose (B := Build_FibSequence A (fun x => a1^+(x.1) = x.2) (fun x => ap (fun a => a^+))). transitivity (fib_seq_to_type_fam B (inj A 0 a2)). + symmetry; srapply equiv_path_from_contr. - exact (inj (fib_seq_to_seq B (0;a1)) 0 idpath). - srefine (contr_equiv _ (seq_colim_sum_to_sum_seq_colim B)). srapply contr_colim_contr_seq; intro k; srapply contr_basedpaths. + srapply equiv_functor_colimit; srefine (transitivity (equiv_fib_seq_to_seq B (0;a2)) _). srapply Build_diagram_equiv. * srapply Build_DiagramMap. - exact (fun n => coe (ap B (seq_shift_pair_from_zero a2 n))). - intros n m p b; destruct p; srapply (K _ _ (seq_shift_pair_from_zero a2 n)). * exact _. 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.