Library Containers.M

Require Export Containers.Final_Coalgebra.
Require Export Containers.Container.
Require Import Containers.Equivalences.
Require Import Containers.Chain.
Require Import Containers.Cochain.

Section M.

Context {funext : Funext}.

Variables (A : Type) (B : A Type).

Local Definition W : nat Type :=
nat_rec Type Unit (fun _ X(| A ||> B |) X).

Local Definition pi : n, W n.+1 W n :=
nat_rect (fun iW (S i) W i) (fun _tt) (fun _ fmap f).

Local Definition chain : Chain :=
Build_Chain W pi.

Definition M : Type :=
limit chain.

Local Definition in_ : (| A ||> B |) M M :=
shift_preserves_limit chain oE
(polynomial_functors_commute_with_limit (A ||> B) chain)^-1.

Definition m_out := in_^-1.

Definition M_coalg := Build_Coalgebra _ M m_out.

Lemma is_final_M : is_final M_coalg.
Proof.
intros C.
apply contr_equiv_unit.
transitivity {h : _ & m_out o h = map h o coalg_fun C}. {
symmetry. exact (issig_Coalgebra_Hom C M_coalg).
}
set (step := fun B (h : C B) ⇒ map h o C).
change ({h : _ & m_out o h = step M h} <~> Unit).
set (Ψ := fun hin_ o step M h).
transitivity {h : _ & in_ o m_out o h = Ψ h}. {
apply equiv_functor_sigma_id; intros h.
unfold Ψ.
apply (equiv_ap (fun hin_ o h)).
}
transitivity {h : _ & h = Ψ h}. {
apply equiv_functor_sigma_id; intros h.
apply equiv_concat_l.
apply apD10^-1; intros y.
unfold m_out.
rewrite eisretr.
reflexivity.
}
set (e := (@limit_universal _ chain C)^-1 % equiv).
transitivity {cone : Cone C chain & e cone = Ψ (e cone)}. {
symmetry.
serapply equiv_functor_sigma'.
- exact e.
- intros cone.
apply reflexivity.
}
set (Φ := e^-1 o Ψ o e).
set (Φ0' := fun n fnstep (W n) fn).
set (Φ0 :=
fun f n y
match n return W n with
| 0 ⇒ tt
| n'.+1Φ0' n' (f n') y
end).
set (Φ1' :=
fun u n (pn : pi n o u n.+1 = u n) y
match apD10^-1 (apD10 (pn) o (C y).2) in (_ = v2)
return (((C y).1; pi n o u n.+1 o (C y).2) =
((C y).1; v2))
with
| idpathidpath
end : (pi n.+1 o step (W n.+1) (u n.+1)) y = Φ0 u n.+1 y).
set (Φ1 :=
fun (u : Cone0 C chain) (p : Cone1 u) n
apD10^-1 (fun y
match n return (pi n o step (W n) (u n)) y = Φ0 u n y with
| 0 ⇒ idpath
| n'.+1Φ1' u n' (p n') y
end)).
assert ( u p, (Φ (u; p)) = (Φ0 u; Φ1 u p)). { reflexivity. }
transitivity {cone : Cone C chain & e cone = e (Φ cone)}. {
apply equiv_functor_sigma_id; intros cone.
apply equiv_concat_r.
unfold Φ.
exact (eisretr e _)^.
}
transitivity {cone : Cone C chain & cone = Φ cone}. {
apply equiv_functor_sigma_id; intros cone.
symmetry.
apply equiv_ap'.
}
transitivity {
cone : Cone C chain & {
p : cone.1 = Φ0 cone.1 &
p # cone.2 = Φ1 cone.1 cone.2}}. {
apply equiv_functor_sigma_id; intros cone.
symmetry. exact (equiv_path_sigma _ cone (Φ cone)).
}
transitivity {
u : Cone0 C chain & {
q : Cone1 u & {
p : u = Φ0 u &
p # q = Φ1 u q}}}. {
unfold Cone.
symmetry.
erapply equiv_sigma_assoc.
}
transitivity {
u : Cone0 C chain & {
p : u = Φ0 u & {
q : Cone1 u &
p # q = Φ1 u q}}}. {
apply equiv_functor_sigma_id; intros u.
apply equiv_sigma_symm.
}
transitivity {
up : {
u : Cone0 C chain &
u = Φ0 u} & {
q : Cone1 up.1 &
transport Cone1 up.2 q = Φ1 up.1 q}}. {
erapply equiv_sigma_assoc.
}
transitivity {_ : Unit & Unit}. {
erapply equiv_functor_sigma'.
- unfold Φ0, Cone0.
transitivity {u : Cone0 C chain & n, u n = Φ0 u n}. {
apply equiv_functor_sigma_id; intros u.
apply equiv_apD10.
}
transitivity {u : Cone0 C chain & n, u n.+1 = Φ0 u n.+1}. {
apply equiv_functor_sigma_id; intros u.
rapply equiv_shift_sequence_contr_base.
}
transitivity (Cone0' C chain 0). {
unfold Φ0.
change (
cochain_limit (Build_Cochain (Cone0' C chain) Φ0') <~>
Cone0' C chain 0).
apply equiv_cochain_limit_base.
}
unfold Cone0'; simpl.
apply equiv_contr_contr.
- intros [u p]; simpl.
transitivity {q : Cone1 u & q = p^ # Φ1 u q}. {
apply equiv_functor_sigma_id; intros q.
apply equiv_moveL_transport_V.
}
transitivity {
q : Cone1 u &
n, q n = (transport Cone1 p^ (Φ1 u q)) n}. {
apply equiv_functor_sigma_id; intros q.
apply equiv_apD10.
}
transitivity {
q : Cone1 u &
n, q n = transport (fun uCone1' u n) p^ (Φ1 u q n)}. {
apply equiv_functor_sigma_id; intros q.
apply equiv_functor_forall_id; intros n.
apply equiv_concat_r.
erapply transport_forall_constant.
}
transitivity {
q : Cone1 u &
n, q n.+1 =
transport (fun uCone1' u n.+1) p^ (Φ1 u q n.+1)}. {
apply equiv_functor_sigma_id; intros q.
rapply equiv_shift_sequence_contr_base.
}
unfold Φ1.
transitivity (Cone1' u 0). {
change (
cochain_limit (Build_Cochain
(Cone1' u)
(fun n qntransport (fun uCone1' u n.+1) p^
(apD10^-1 (Φ1' u n qn)))) <~>
Cone1' u 0).
apply equiv_cochain_limit_base.
}
unfold Cone1'; simpl.
apply equiv_contr_contr.
}
apply equiv_contr_contr.
Qed.

Instance contr_hom_to_M_coalg (C : Coalgebra (| A ||> B |)) :
Contr (Coalgebra_Hom C M_coalg) :=
is_final_M C.

Definition m_label : M A :=
pr1 o M_coalg.

Definition m_arg : m, B (m_label m) M :=
pr2 o M_coalg.

Section Corecursion.

Context {X : Type}.
Variable step : X {a : A & B a X}.

Local Definition H :=
@center _ (is_final_M (Build_Coalgebra (| A ||> B |) X step)).

Definition m_corec (x : X) : M :=
H x.

Definition m_beta_label (x : X) : m_label (m_corec x) = (step x).1 :=
(ap10 (coalg_hom_path H) x)..1.

Definition m_beta_arg (x : X) :
transport (fun aB a M) (m_beta_label x)
(m_arg (m_corec x)) =
m_corec o (step x).2 :=
(ap10 (coalg_hom_path H) x)..2.

Lemma m_eta (h' : X M) (label_h' : x, m_label (h' x) = (step x).1)
(arg_h' : x, transport (fun aB a M) (label_h' x) (m_arg (h' x)) =
h' o (step x).2) :
h' = m_corec.
Proof.
set (X_coalg := Build_Coalgebra (| A ||> B |) X step).
transparent assert (H' : (Coalgebra_Hom X_coalg M_coalg)). {
apply (Build_Coalgebra_Hom X_coalg M_coalg h').
apply path_forall; intros x.
change ((m_label (h' x); m_arg (h' x)) = map h' (X_coalg x)).
serapply path_sigma'.
- apply label_h'.
- apply arg_h'.
}
change (coalg_hom_fun H' = coalg_hom_fun H).
f_ap.
apply path_contr.
Qed.

End Corecursion.

End M.

Arguments m_label {_ _ _} _.
Arguments m_arg {_ _ _} _ _.
Arguments m_corec {_ _ _ _} _ _.
Arguments m_beta_label {_ _ _ _} _ _.
Arguments m_beta_arg {_ _ _ _} _ _.
Arguments m_eta {_ _ _ _} _ _ _ _.

Global Opaque M.
Global Opaque m_out.
Global Opaque is_final_M.