# Limits of chains and cochains in the precategory of types

The shifted chain (X', π') from (X, π) is one where Xₙ' = Xₙ₊₁ and πₙ' = πₙ₊₁.
Definition shift_chain (cha : chain type_precat) : chain type_precat.
Proof.
use tpair.
- exact (dob cha S).
- exact (λ _ _ path, dmor cha (maponpaths S path)).
Defined.

The shifted cochain (X', π') from (X, π) is one where Xₙ' = Xₙ₊₁ and πₙ' = πₙ₊₁.
Definition shift_cochain {C : precategory} (cochn : cochain C) : cochain C.
Proof.
use cochain_weq; use tpair.
- exact (dob cochn S).
- intros n; cbn.
apply (dmor cochn).
exact (idpath _).
Defined.

Interaction between transporting over (maponpaths S ed) and shifting the cochain
Definition transport_shift_cochain :
cochn ver1 ver2 (ed : ver1 = ver2)
(stdlim_shift : standard_limit (shift_cochain cochn)),
transportf (dob cochn) (maponpaths S ed) (pr1 stdlim_shift ver1) =
transportf (dob (shift_cochain cochn)) ed (pr1 stdlim_shift ver1).
Proof.
intros cochn ver1 ver2 ed stdlim_shift.
induction ed.
reflexivity.
Defined.

Ways to prove that dmors are equal on cochains
Lemma cochain_dmor_paths {C : precategory} {ver1 ver2 : vertex conat_graph}
(cochn : cochain C) (p1 p2 : edge ver1 ver2) : dmor cochn p1 = dmor cochn p2.
Proof.
apply maponpaths, proofirrelevance, isasetnat.
Defined.

More ways to prove that dmors are equal on cochains
Lemma cochain_dmor_paths_type {ver1 ver2 ver3 : vertex conat_graph}
(cochn : cochain type_precat) (p1 : edge ver1 ver3) (p2 : edge ver2 ver3)
(q1 : ver1 = ver2) :
v1 : dob cochn ver1, dmor cochn p1 v1 = dmor cochn p2 (transportf _ q1 v1).
Proof.
intro v1; cbn in ×.
induction q1.
cbn; unfold idfun.
exact (toforallpaths _ _ _ (cochain_dmor_paths cochn p1 p2) v1).
Defined.

We use the following tactic notations to mirror the "equational style" of reasoning used in Ahrens, Capriotti, and Spadotti.
Local Tactic Notation "≃" constr(H) "by" tactic(t) := intermediate_weq H; [t|].
Local Tactic Notation "≃'" constr(H) "by" tactic(t) := intermediate_weq H; [|t].
Local Tactic Notation "≃" constr(H) := intermediate_weq H.
Local Tactic Notation "≃'" constr(H) := apply invweq; intermediate_weq H.

Local Lemma combine_over_nat_basic {X Y Z : nat UU} :
X 0 Z 0 ( n : nat, Y (S n) Z (S n))
(X 0 × n : nat, Y (S n)) n : nat, Z n.
Proof.
intros x0z0 yszs.
≃ (Z 0 × ( n : nat, Z (S n))).
- apply weqdirprodf; [apply x0z0|].
apply weqonsecfibers, yszs.
- use weq_iso.
+ intros z0zs.
intros n; induction n.
× exact (dirprod_pr1 z0zs).
× apply (dirprod_pr2 z0zs).
+ intros xs; use make_dirprod.
× apply xs.
× exact (xs S).
+ reflexivity.
+ intros xs.
apply funextsec; intros n.
induction n; reflexivity.
Defined.

Local Lemma combine_over_nat {X : nat UU} {P : (X 0 × ( n : nat, X (S n))) UU} :
( x0 : X 0, xs : n : nat, X (S n), P (make_dirprod x0 xs))
( xs : n : nat, X n, P (make_dirprod (xs 0) (xs S))).
Proof.
≃ ( pair : (X 0 × n : nat, X (S n)), P pair) by apply weqtotal2asstol.
use weqbandf.
- apply (@combine_over_nat_basic X X X); intros; apply idweq.
- intros x0xs; cbn.
apply idweq.
Defined.

Local Lemma combine_over_nat' {X : nat UU} {P : X 0 ( n : nat, X (S n)) UU} :
( x0 : X 0, xs : n : nat, X (S n), P x0 xs)
( xs : n : nat, X n, P (xs 0) (xs S)).
Proof.
≃ ( (x0 : X 0) (xs : n : nat, X (S n)), (uncurry (Z := λ _, UU) P)
(make_dirprod x0 xs)) by apply idweq.
≃' ( xs : n : nat, X n, uncurry P (Z := λ _, UU)
(make_dirprod (xs 0) (xs S))) by apply idweq.
apply combine_over_nat.
Defined.

If the base type is contractible, so is the type of sections over it.
Definition weqsecovercontr_uncurried {X : UU} {Y : X UU}
(P : x : X, Y x UU) (isc : iscontr ( x : X, Y x)) :
( (x : X) (y : Y x), P x y) (P (pr1 (iscontrpr1 isc)) (pr2 (iscontrpr1 isc))).
Proof.
≃ ( pair : ( x : X, Y x), uncurry (Z := λ _, UU) P pair) by
apply invweq, weqsecovertotal2.
≃' (uncurry (Z := λ _, UU) P (iscontrpr1 isc)) by (apply idweq).
apply weqsecovercontr.
Defined.

Shifted cochains have equivalent limits. (Lemma 12 in Ahrens, Capriotti, and Spadotti)

Definition shifted_limit (cocha : cochain type_precat) :
standard_limit (shift_cochain cocha) standard_limit cocha.
Proof.
pose (X := dob cocha); cbn in X.
posen := (@dmor _ _ cocha (S n) n (idpath _))).
unfold standard_limit, shift_cochain, funcomp, idfun; cbn.

assert (isc : x : v : nat, dob cocha (S v),
iscontr ( x0 : X 0, (π 0 (x 0)) = x0)).
{
intros x.
apply iscontr_paths_from.
}

Step (2) This is the direct product with the type proven contractible above
≃ ( xs : v : nat, X (S v),
( (u v : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, X (S o) X (S (S v))) e
(idfun (X (S (S v))))) (xs u) = xs v)
× ( x0 : X 0, (π 0 (xs 0)) = x0)) by
(apply weqfibtototal; intro; apply dirprod_with_contr_r; apply isc).

Now, we swap the components in the direct product.
≃ ( xs : v : nat, X (S v),
( x0 : X 0, π 0 (xs 0) = x0) ×
( (u v : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, X (S o) X (S (S v))) e
(idfun (X (S (S v))))) (xs u) = xs v)) by
(apply weqfibtototal; intro; apply weqdirprodcomm).

Using associativity of Σ-types,
≃ ( xs : v : nat, X (S v),
x0 : X 0,
(π 0 (xs 0) = x0) ×
( (u v : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, X (S o) X (S (S v))) e
(idfun (X (S (S v))))) (xs u) = xs v)) by
(apply weqfibtototal; intro; apply weqtotal2asstor).

And again by commutativity of ×, we swap the first components
≃ ( x0 : X 0,
xs : n : nat, X (S n),
(π 0 (xs 0) = x0) ×
( (u v : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, X (S o) X (S (S v))) e
(idfun (X (S (S v))))) (xs u) = xs v)) by (apply weqtotal2comm).

Step 3: combine the first bits
≃ ( xs : n : nat, X n,
(π 0 (xs 1) = xs 0) ×
( (u v : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, dob cocha (S o) dob cocha (S (S v))) e
(idfun (dob cocha (S (S v))))) (xs (S u)) = xs (S v))).
apply (@combine_over_nat' X
(λ x0 xs,
π 0 (xs 0) = x0
× ( (u v : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, X (S o) X (S (S v))) e (idfun (X (S (S v)))))
(xs u) = xs v))).

Now the first component is the same.
apply weqfibtototal; intros xs.

≃ (π 0 (xs 1) = xs 0
× ( (v u : nat) (e : S v = u),
(dmor cocha (idpath (S (S v)))
transportf (λ o : nat, dob cocha (S o) dob cocha (S (S v))) e
(idfun (dob cocha (S (S v))))) (xs (S u)) = xs (S v))) by
apply weqdirprodf; [apply idweq|apply flipsec_weq].

≃' ( (v u : nat) (e : S v = u), dmor cocha e (xs u) = xs v) by
apply flipsec_weq.

Split into cases on n = 0 or n > 0. Coq is bad about coming up with these implicit arguments, so we have to be very excplicit.
apply (@combine_over_nat_basic
(λ n, π n (xs (S n)) = xs n)
(λ v, (u : nat) (e : v = u),
(dmor cocha (idpath (S v))
_ (idfun (dob cocha (S v)))) (xs (S u)) = xs v)
(λ v, (u : nat) (e : S v = u), dmor cocha e (xs u) = xs v)).

We use the following fact over and over to simplify the remaining types: for any x : X, the type ∑ y : X, x = y is contractible.
- apply invweq.
apply (@weqsecovercontr_uncurried
nat (λ n, 1 = n) (λ _ _, _ = xs 0) (iscontr_paths_from 1)).
- intros u.
≃ ((dmor cocha (idpath (S (S u)))
transportf (λ o : nat, dob cocha (S o) dob cocha (S (S u)))
(idpath (S u)) (idfun (dob cocha (S (S u))))) (xs (S (S u))) =
xs (S u)).
+ apply (@weqsecovercontr_uncurried
nat (λ n, (S u) = n) (λ _ _, _ _ = xs (S u)) (iscontr_paths_from _)).
+ cbn; unfold funcomp, idfun.
apply invweq.
apply (@weqsecovercontr_uncurried
nat (λ n, (S (S u)) = n) (λ _ _, _ = xs (S u)) (iscontr_paths_from _)).
Defined.

Lemma 11 in Ahrens, Capriotti, and Spadotti
Local Definition Z X l :=
(x : n, X n), n, x (S n) = l n (x n).
Local Lemma lemma_11 (X : nat UU) (l : n, X n X (S n)) : Z X l X 0.
Proof.
set (f (xp : Z X l) := pr1 xp 0).
transparent assert (g : (X 0 Z X l)). {
intros x.
(nat_rect _ x l).
exact (λ n, idpath _).
}
apply (make_weq f).
apply (isweq_iso f g).
- cbn.
intros xp; induction xp as [x p].
transparent assert ( q : (nat_rect X (x 0) l ¬ x )). {
intros n; induction n; cbn.
× reflexivity.
× exact (maponpaths (l n) IHn @ !p n).
}
set (q' := funextsec _ _ _ q).
use total2_paths_f; cbn.
+ exact q'.
+ rewrite transportf_sec_constant. apply funextsec; intros n.
intermediate_path (!maponpaths (λ x, x (S n)) q' @
maponpaths (λ x, l n (x n)) q'). {
use transportf_paths_FlFr.
}
intermediate_path (!maponpaths (λ x, x (S n)) q' @
maponpaths (l n) (maponpaths (λ x, x n) q')). {
apply maponpaths. symmetry. use maponpathscomp.
}
intermediate_path (! q (S n) @ maponpaths (l n) (q n)). {
unfold q'.
repeat rewrite maponpaths_funextsec.
reflexivity.
}
intermediate_path (! (maponpaths (l n) (q n) @ ! p n) @
maponpaths (l n) (q n)). {
reflexivity.
}
rewrite pathscomp_inv.
rewrite <- path_assoc.
rewrite pathsinv0l.
rewrite pathsinv0inv0.
rewrite pathscomp0rid.
reflexivity.
- cbn.
reflexivity.
Defined.

Local Definition lemma_11_unfolded (X : nat UU) (l : n, X n X (S n)) :
( (x : n, X n), n, x (S n) = l n (x n)) X 0 := lemma_11 X l.

Lemma cochain_limit_standard_limit_weq (cha cha' : cochain type_precat) :
cochain_limit cha cochain_limit cha' standard_limit cha standard_limit cha'.
Proof.
intro f.
apply (weqcomp (invweq (lim_equiv _))).
apply (weqcomp f).
apply (lim_equiv _).
Defined.

Local Open Scope cat.
Section CochainCone.

Context (A C : UU) (B : A UU).

Definition terminal_cochain : cochain type_precat :=
termCochain (TerminalType) (polynomial_functor A B).

Definition m_type := standard_limit terminal_cochain.

Definition apply_on_chain (cha : cochain type_precat) : cochain type_precat :=
mapcochain (polynomial_functor A B) cha.

Definition terminal_cochain_shifted_lim :
standard_limit (shift_cochain terminal_cochain)
standard_limit (apply_on_chain terminal_cochain).
Proof.
apply cochain_limit_standard_limit_weq.
unfold shift_cochain, apply_on_chain, cochain_limit.
apply weqfibtototal;intros.
apply weqonsecfibers; intro n.
apply idweq.
Defined.

Let W n := iter_functor (polynomial_functor A B) n unit.
Let Cone0' := λ n : nat, C W n.
Let Cone0 := n : nat, Cone0' n.
Let π := λ n : nat, dmor terminal_cochain (idpath (S n)).

Definition simplified_cone : UU :=
( (u : Cone0), n : nat, (π n u (S n))%functions = u n).

Lemma simplify_cochain_cone :
cone terminal_cochain C simplified_cone.
Proof.
unfold cone, Cone0.
apply weqfibtototal; intro f.
intermediate_weq (
( (u v : vertex conat_graph) (e0 : edge u v),
f _ · dmor terminal_cochain e0 ¬ f v)
). {
do 3 (apply weqonsecfibers; intro).
apply invweq.
apply weqfunextsec.
}
apply invweq.
intermediate_weq ( u, (π u f (S u))%functions ¬ f u). {
apply invweq.
apply weqonsecfibers; intro.
apply weqfunextsec.
}
unfold homotsec.
apply invweq.
intermediate_weq (
( (u v : vertex conat_graph) (c : C) (e0 : edge u v),
(f u · dmor terminal_cochain e0) c = f v c)). {
do 2 (apply weqonsecfibers; intro).
apply flipsec_weq.
}
intermediate_weq (
( (c : C) (u v : vertex conat_graph) (e0 : edge u v),
(f u · dmor terminal_cochain e0) c = f v c)). {
intermediate_weq (
( (u : vertex conat_graph) (c : C) (v : vertex conat_graph) (e0 : edge u v),
(f u · dmor terminal_cochain e0) c = f v c)). {
apply weqonsecfibers; intro.
apply flipsec_weq.
}
apply flipsec_weq.
}
apply invweq.
intermediate_weq (( (x : C) (u : nat), (π u f (S u))%functions x = f u x));
[apply flipsec_weq|].
apply weqonsecfibers; intro c.
apply invweq.
use weq_iso.
- intros eq; intro; apply eq.
- intros eq.
intros ? ? e.
induction e; apply eq.
- abstract ( intro;
do 2 (apply funextsec; intro);
apply funextsec; intro e;
induction e;
reflexivity ).
- abstract ( intro; apply funextsec; intro; reflexivity ).
Defined.

End CochainCone.