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.