{A} (B : FibSequence A) (x : sig A) : fib_seq_to_seq B x ~d~ fib_seq_to_seq' B x. Proof. srapply Build_diagram_equiv. + srapply Build_DiagramMap. * intro n; revert x; induction n as [ | n e]. - exact (fun _ => idmap). - exact (fun x => coe (ap B (seq_pair_shift_assoc x n)) o e x^++). * intros n m p; destruct p; revert x; induction n as [ | n p]. - exact (fun _ _ => idpath). - exact (fun x b => K _ _ _ @ (ap _ (p (x^++) b))). + intro n; revert x; induction n as [ | n e]. * exact (fun _ => isequiv_idmap _). * intro x; srapply isequiv_compose. 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.