Library Containers.Chain

Require Import Containers.Equivalences.
Require Export Containers.Functor.
Require Import Containers.Cochain.
Require Export Containers.Container.

Record Chain := {
  ch_types : nat Type;
  ch_funs : n, ch_types n.+1 ch_types n
}.

Definition limit chain :=
  {x : n, ch_types chain n & n, ch_funs chain n (x n.+1) = x n}.

Definition Cone0' Y chain n :=
  Y ch_types chain n.

Definition Cone0 Y chain :=
   n, Cone0' Y chain n.

Definition Cone1' {Y} {chain} (f : Cone0 Y chain) n :=
  ch_funs chain n o (f n.+1) = f n.

Definition Cone1 {Y} {chain} (f : Cone0 Y chain) :=
   n, Cone1' f n.

Definition Cone Y chain :=
  {f : Cone0 Y chain & Cone1 f}.

Lemma limit_universal `{Funext} chain Y :
  (Y limit chain) <~> Cone Y chain.
Proof.
  destruct chain as [X pi].
  serapply equiv_adjointify.
  - exact (
      fun g
        existT
        Cone1
        (fun n y(g y).1 n)
        (fun napD10^-1 (fun y(g y).2 n))).
  - exact (
      fun fp y
        existT
        (fun x n : nat, pi n (x n.+1) = x n)
        (fun nfp.1 n y)
        (fun napD10 (fp.2 n) y)).
  - intros [f p].
    simpl.
    f_ap.
    apply apD10^-1.
    intros n.
    apply eissect.
  - intros f.
    simpl.
    apply apD10^-1.
    intros y.
    serapply path_sigma; simpl.
    + reflexivity.
    + simpl.
      apply apD10^-1.
      intros n.
      rewrite eisretr.
      reflexivity.
Defined.

Definition shift_chain chain :=
  Build_Chain (ch_types chain o S) (ch_funs chain o S).

Definition shift_preserves_limit `{Funext} chain :
  limit (shift_chain chain) <~> limit chain.
Proof.
  destruct chain as [X pi].
  unfold limit.
  simpl.
  transitivity {
        x : n, X n.+1 &
        {x0 : X 0 & pi 0 (x 0) = x0} ×
         n, pi n.+1 (x n.+1) = x n
      }. {
    apply equiv_functor_sigma_id.
    intros x.
    symmetry.
    transitivity (Unit × ( n : nat, pi n.+1 (x n.+1) = x n)). {
      apply equiv_functor_prod_r.
      apply equiv_contr_unit.
    }
    apply prod_unit_l.
  }
  transitivity {
      x : n, X n.+1 &
      {
        x0 : X 0 &
        (pi 0 (x 0) = x0) ×
         n, pi n.+1 (x n.+1) = x n
      }
    }. {
    apply equiv_functor_sigma_id.
    intros x.
    apply (equiv_composeR' (equiv_sigma_prod0 _ _)^-1).
    apply (equiv_composeR' (equiv_sigma_assoc _ _)^-1).
    apply equiv_functor_sigma_id.
    intros x0.
    apply equiv_sigma_prod0.
  }
  transitivity {
      x : X 0 × n, X n.+1 &
      (pi 0 (snd x 0) = fst x) ×
       n, pi n.+1 (snd x n.+1) = snd x n
    }. {
    apply (equiv_composeR' (equiv_sigma_symm _)).
    apply (equiv_composeR' (equiv_sigma_assoc (fun _ n, X n.+1)
      (fun x0xlet (x0, x) := x0x in
      (pi 0 (x 0) = x0) × ( n : nat, pi n.+1 (x n.+1) = x n)))).
    serapply equiv_functor_sigma'.
    - apply equiv_sigma_prod0.
    - intros x.
      apply reflexivity.
  }
  transitivity {
      x : n, X n &
      (pi 0 (x 1) = x 0) ×
       n, pi n.+1 (x n.+2) = x (n.+1)
    }. {
    serapply equiv_functor_sigma'.
    - apply equiv_nat_match.
    - intros x.
      apply reflexivity.
  }
  apply equiv_functor_sigma_id.
  intros x.
  rapply equiv_nat_match.
Defined.

Definition apply_on_chain (F : Functor) chain :=
  Build_Chain (F o ch_types chain) (fun nmap (ch_funs chain n)).

Definition polynomial_functors_commute_with_limit `{Funext}
    (c : Unary_Container) chain :
  limit (apply_on_chain (|c|) chain) <~> (|c|) (limit chain).
Proof.
  destruct c as [S P].
  destruct chain as [X pi].
  change (
      {x : n, {s : S & P s X n} &
         n, f_map (| S ||> P |) (pi n) (x n.+1) = x n} <~>
      (| S ||> P |) (limit {| ch_types := X; ch_funs := pi |})).
  transitivity {
      x : {s : nat S & n, P (s n) X n} &
         n, existT (fun sP s X n) (x.1 n.+1) (pi n o x.2 n.+1) =
          (x.1 n; x.2 n)
    }. {
    serapply equiv_functor_sigma'; simpl.
    - symmetry.
      erapply equiv_sigT_coind.
    - intros x.
      apply equiv_functor_forall_id; intros n.
      apply reflexivity.
  }
  transitivity {
      s : nat S & {
        l : n, P (s n) X n &
         n, existT (fun sP s X n) (s n.+1) (pi n o l n.+1) =
          (s n; l n)
      }
    }. {
    symmetry.
    erapply equiv_sigma_assoc.
  }
  transitivity {
      s : nat S & {
        l : n, P (s n) X n &
         n, {p : s n.+1 = s n &
          transport (fun aP a X n) p (pi n o l n.+1) = l n}
      }
    }. {
    apply equiv_functor_sigma_id; intros s.
    apply equiv_functor_sigma_id; intros l.
    apply equiv_functor_forall_id; intros n.
    symmetry.
    exact (equiv_path_sigma _
      (existT (fun sP s X n) (s n.+1)
      (fun x : P (s n.+1) ⇒ pi n (l n.+1 x)))
      (existT (fun sP s X n) (s n) (l n))).
  }
  transitivity {
      s : nat S & {
        l : n, P (s n) X n & {
          p : n, s n.+1 = s n &
             n, transport (fun aP a X n)
              (p n) (pi n o l n.+1) = l n
        }
      }
    }. {
    apply equiv_functor_sigma_id; intros s.
    apply equiv_functor_sigma_id; intros l.
    symmetry.
    erapply equiv_sigT_coind.
  }
  transitivity {
      s : nat S & {
        p : n, s n.+1 = s n & {
          l : n, P (s n) X n &
           n, transport (fun aP a X n)
            (p n) (pi n o l n.+1) = l n
        }
      }
    }. {
    apply equiv_functor_sigma_id; intros s.
    apply equiv_sigma_symm.
  }
  transitivity {
      sp : {s : nat S & n, s n.+1 = s n} & {
        l : n, P (sp.1 n) X n &
           n, transport (fun aP a X n)
            (sp.2 n) (pi n o l n.+1) = l n
      }
    }. {
    erapply equiv_sigma_assoc.
  }
  set (E := equiv_cochain_limit_base_simpl S).
  transitivity {
      a : S & {
        u : n, P a X n &
         n, pi n o u n.+1 = u n
      }
    }. {
    symmetry.
    serapply equiv_functor_sigma'.
    - symmetry. exact E.
    - intros s.
      apply reflexivity.
  }
  transitivity {s : S & P s limit (Build_Chain X pi)}. {
    apply equiv_functor_sigma_id; intros s.
    symmetry.
    apply limit_universal.
  }
  apply reflexivity.
Defined.