(X : nat -> Type) (f : forall n, X n -> X n.+1) : Sequence. Proof. srapply Build_Diagram. 1: exact X. intros ? ? p. destruct p. apply f. Defined.
Require Import Basics. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.