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 n ⇒ apD10^-1 (fun y ⇒ (g y).2 n))).
- exact (
fun fp y ⇒
existT
(fun x ⇒ ∀ n : nat, pi n (x n.+1) = x n)
(fun n ⇒ fp.1 n y)
(fun n ⇒ apD10 (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 x0x ⇒ let (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 n ⇒ map (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 s ⇒ P 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 s ⇒ P 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 a ⇒ P 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 s ⇒ P s → X n) (s n.+1)
(fun x : P (s n.+1) ⇒ pi n (l n.+1 x)))
(existT (fun s ⇒ P 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 a ⇒ P 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 a ⇒ P 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 a ⇒ P 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.
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 n ⇒ apD10^-1 (fun y ⇒ (g y).2 n))).
- exact (
fun fp y ⇒
existT
(fun x ⇒ ∀ n : nat, pi n (x n.+1) = x n)
(fun n ⇒ fp.1 n y)
(fun n ⇒ apD10 (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 x0x ⇒ let (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 n ⇒ map (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 s ⇒ P 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 s ⇒ P 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 a ⇒ P 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 s ⇒ P s → X n) (s n.+1)
(fun x : P (s n.+1) ⇒ pi n (l n.+1 x)))
(existT (fun s ⇒ P 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 a ⇒ P 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 a ⇒ P 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 a ⇒ P 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.