Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Diagrams.Graph.
Require Import Diagrams.Diagram.

Local Open Scope nat_scope.
Local Open Scope path_scope.

(** * Sequence *)

(** A Sequence is a sequence of maps from [X(n)] to [X(n+1)]. *)

Definition sequence_graph : Graph.
Graph
Proof.
Graph
  srapply (Build_Graph nat).
nat -> nat -> Type
  intros n m; exact (S n = m).
Defined.

Definition Sequence := Diagram sequence_graph.

Definition Build_Sequence
  (X : nat -> Type)
  (f : forall n, X n -> X n.+1)
  : Sequence.
X: nat -> Type
f: forall n : nat, X n -> X n.+1
Sequence
Proof.
X: nat -> Type
f: forall n : nat, X n -> X n.+1
Sequence
  srapply Build_Diagram.
X: nat -> Type
f: forall n : nat, X n -> X n.+1
sequence_graph -> Type
X: nat -> Type
f: forall n : nat, X n -> X n.+1
forall i j : sequence_graph,
sequence_graph i j -> ?obj i -> ?obj j
  1: exact X.
X: nat -> Type
f: forall n : nat, X n -> X n.+1
forall i j : sequence_graph,
sequence_graph i j -> X i -> X j
  intros ? ? p.
X: nat -> Type
f: forall n : nat, X n -> X n.+1
i, j: sequence_graph
p: sequence_graph i j
X i -> X j
  destruct p.
X: nat -> Type
f: forall n : nat, X n -> X n.+1
i: sequence_graph
X i -> X i.+1
  apply f.
Defined.

(** A useful lemma to show than two sequences are equivalent. *)

Definition equiv_sequence (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.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (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.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (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
  srapply (Build_diagram_equiv (Build_DiagramMap _ _)); intro n; simpl.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
D1 n -> D2 n
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
forall (j : nat) (g : n.+1 = j) (x : D1 n),
(D2 _f g) (?Goal x) = ?Goal@{n:=j} ((D1 _f g) x)
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
IsEquiv ?Goal
  -
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
D1 n -> D2 n apply equiv_fun.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
D1 n <~> D2 n
    induction n.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
D1 0 <~> D2 0
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: nat
IHn: D1 n <~> D2 n
D1 n.+1 <~> D2 n.+1
    +
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
D1 0 <~> D2 0 exact H0.
    +
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: nat
IHn: D1 n <~> D2 n
D1 n.+1 <~> D2 n.+1 exact (Hn n IHn).1.
  -
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
forall (j : nat) (g : n.+1 = j) (x : D1 n),
(D2 _f g)
  (nat_rect (fun n : nat => D1 n <~> D2 n) H0
     (fun (n : nat) (IHn : D1 n <~> D2 n) =>
      (Hn n IHn).1) n x) =
nat_rect (fun n : nat => D1 n <~> D2 n) H0
  (fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1)
  j ((D1 _f g) x) intros m q; destruct q.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
forall x : D1 n,
(D2 _f 1)
  (nat_rect (fun n : nat => D1 n <~> D2 n) H0
     (fun (n : nat) (IHn : D1 n <~> D2 n) =>
      (Hn n IHn).1) n x) =
nat_rect (fun n : nat => D1 n <~> D2 n) H0
  (fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1)
  n.+1 ((D1 _f 1) x)
    induction n; simpl.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
forall x : D1 0,
(D2 _f 1) (H0 x) = (Hn 0 H0).1 ((D1 _f 1) x)
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: nat
IHn: forall x : D1 n,
(D2 _f 1)
(nat_rect (fun n : nat => D1 n <~> D2 n) H0
(fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1) n x) =
nat_rect (fun n : nat => D1 n <~> D2 n) H0
(fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1) n.+1 ((D1 _f 1) x)
forall x : D1 n.+1,
(D2 _f 1)
  ((Hn n
      (nat_rect (fun n : nat => D1 n <~> D2 n) H0
         (fun (n : nat) (IHn : D1 n <~> D2 n) =>
          (Hn n IHn).1) n)).1 x) =
(Hn n.+1
   (Hn n
      (nat_rect (fun n : nat => D1 n <~> D2 n) H0
         (fun (n : nat) (IHn : D1 n <~> D2 n) =>
          (Hn n IHn).1) n)).1).1 ((D1 _f 1) x)
    +
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
forall x : D1 0,
(D2 _f 1) (H0 x) = (Hn 0 H0).1 ((D1 _f 1) x) exact (Hn 0 H0).2.
    +
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: nat
IHn: forall x : D1 n,
(D2 _f 1)
(nat_rect (fun n : nat => D1 n <~> D2 n) H0
(fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1) n x) =
nat_rect (fun n : nat => D1 n <~> D2 n) H0
(fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1) n.+1 ((D1 _f 1) x)
forall x : D1 n.+1,
(D2 _f 1)
  ((Hn n
      (nat_rect (fun n : nat => D1 n <~> D2 n) H0
         (fun (n : nat) (IHn : D1 n <~> D2 n) =>
          (Hn n IHn).1) n)).1 x) =
(Hn n.+1
   (Hn n
      (nat_rect (fun n : nat => D1 n <~> D2 n) H0
         (fun (n : nat) (IHn : D1 n <~> D2 n) =>
          (Hn n IHn).1) n)).1).1 ((D1 _f 1) x) simple refine (Hn n.+1 _).2.
  -
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: sequence_graph
IsEquiv
  (nat_rect (fun n : nat => D1 n <~> D2 n) H0
     (fun (n : nat) (IHn : D1 n <~> D2 n) =>
      (Hn n IHn).1) n) induction n; simpl.
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
IsEquiv H0
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: nat
IHn: IsEquiv
(nat_rect (fun n : nat => D1 n <~> D2 n) H0
(fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1) n)
IsEquiv
  (Hn n
     (nat_rect (fun n : nat => D1 n <~> D2 n) H0
        (fun (n : nat) (IHn : D1 n <~> D2 n) =>
         (Hn n IHn).1) n)).1
    +
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
IsEquiv H0 apply H0.
    +
D1, D2: Sequence
H0: D1 0 <~> D2 0
Hn: forall (n : sequence_graph) (e : D1 n <~> D2 n),
{e' : D1 n.+1 <~> D2 n.+1 &
D2 _f 1 o e == e' o D1 _f 1}
n: nat
IHn: IsEquiv
(nat_rect (fun n : nat => D1 n <~> D2 n) H0
(fun (n : nat) (IHn : D1 n <~> D2 n) => (Hn n IHn).1) n)
IsEquiv
  (Hn n
     (nat_rect (fun n : nat => D1 n <~> D2 n) H0
        (fun (n : nat) (IHn : D1 n <~> D2 n) =>
         (Hn n IHn).1) n)).1 apply (Hn n _ ).1.
Defined.