Library Containers.Cochain

Require Export HoTT.

Record Cochain := {
  coch_types : nat → Type;
  coch_funs : ∀ n, coch_types n → coch_types n.+1
}.

Definition cochain_limit cochain :=
  {x : ∀ n, coch_types cochain n &
     ∀ n, x n.+1 = coch_funs cochain n (x n)}.

Lemma equiv_cochain_limit_base_simpl `{Funext} X :
  {x : nat → X & ∀ n : nat, x n.+1 = x n} <~> X.
Proof.
  serapply equiv_adjointify.
  - exact (fun xp ⇒ xp.1 0).
  - exact (fun x ⇒ (fun _ ⇒ x; const idpath)).
  - intros x.
    reflexivity.
  - intros [x p].
    set (s := nat_rect (fun n ⇒ x 0 = x n) idpath (fun n IH ⇒ IH @ (p n)^)).
    set (s' := apD10^-1 s).
    serapply path_sigma; simpl.
    + exact s'.
    + apply apD10^-1; intros n.
      rewrite transport_forall_constant.
      rewrite transport_paths_FlFr.
      unfold const.
      rewrite concat_p1.
      change ((apD10 s' n.+1)^ @ apD10 s' n = p n).
      unfold s'.
      rewrite eisretr.
      unfold s; simpl.
      rewrite inv_pp.
      autorewrite with paths.
      reflexivity.
Defined.

Lemma equiv_cochain_limit_base `{Funext} cochain :
  cochain_limit cochain <~> coch_types cochain 0.
Proof.
  destruct cochain as [X l].
  serapply equiv_adjointify.
  - exact (fun xp ⇒ xp.1 0).
  - exact (
        fun x0 ⇒
          existT (fun x ⇒ ∀ n, x n.+1 = l n (x n))
                 (nat_rect X x0 l)
                 (fun _ ⇒ idpath)
      ).
  - done.
  - intros [x p].
    simpl.
    set (s :=
        nat_rect (fun n ⇒ nat_rect X (x 0) l n = x n)
          idpath
          (fun n IHn ⇒ ap (l n) IHn @ (p n)^)
      ).
    set (s' := apD10^-1 s).
    serapply path_sigma; simpl.
    + exact s'.
    + apply apD10^-1.
      intros n.
      rewrite transport_forall_constant.
      rewrite transport_paths_FlFr.
      rewrite concat_p1.
      rewrite (ap_compose (fun x : ∀ n : nat, X n ⇒ x n) (fun x ⇒ l n x)).
      change (
          (apD10 (apD10^-1 s) n.+1)^ @
          ap (l n) (apD10 (apD10^-1 s) n) =
          p n
        ).
      rewrite eisretr.
      simpl.
      rewrite inv_pp.
      rewrite <- concat_p_pp.
      rewrite concat_Vp.
      rewrite concat_p1.
      apply inv_V.
Defined.