(D1 D2 : Sequence) (H0 : (D1 0) <~> (D2 0)) (Hn: forall n (e: (D1 n) <~> (D2 n)), {e' : (D1 n.+1) <~> (D2 n.+1) & (D2 _f 1) o e == e' o (D1 _f 1)}) : D1 ~d~ D2. Proof. srapply (Build_diagram_equiv (Build_DiagramMap _ _)); intro n; simpl. - apply equiv_fun. induction n. + apply H0. + exact (Hn n IHn).1. - intros m q; destruct q. induction n; simpl. + exact (Hn 0 H0).2. + simple refine (Hn n.+1 _).2. - induction n; simpl. + apply H0. + apply (Hn n _ ).1. Defined.
Require Import Basics. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.