Library Containers.M_with_Conversion

Require Export Containers.Final_Coalgebra.
Require Export Containers.Container.

Section M_with_Conversion.
Context {funext : Funext}.

Variable A : Type.
Variable B : A → Type.

Axiom M : Coalgebra (| A ||> B |).
Axiom m_corec : ∀ X, (X → {a : A & B a → X}) → X → M.
Arguments m_corec {_} _ _.
Definition m_label : M → A :=
pr1 o M.
Definition m_arg : ∀ m, B (m_label m) → M :=
pr2 o M.
Axiom m_beta_label :
  ∀ X step (x : X), m_label (m_corec step x) = (step x).1.
Arguments m_beta_label {_} _ _.
Axiom m_beta_arg :
  ∀ X step (x : X),
    transport (fun a ⇒ B a → M) (m_beta_label step x)
      (m_arg (m_corec step x)) =
    m_corec step o (step x).2.
Variable m_eta_id :
  m_corec M = idmap.

Definition M' :=
{m : M &
  merely {C : Coalgebra (| A ||> B |) & {x : C & m_corec C x = m}}}.

Definition m_corec' {X} (step : X → (| A ||> B |) X) (x : X) : M'.
Proof.
  unfold M'.
  ∃ (m_corec step x).
  apply tr.
  ∃ (Build_Coalgebra _ X step).
  ∃ x.
  reflexivity.
Defined.

Local Definition m_out_p' (m : M') : {
  af : {a : A & B a → M'} &
    M m.1 =
    existT (fun a ⇒ B a → M) af.1 (pr1 o af.2)}.
Proof.
  apply (@Trunc_rec -1
      {C : Coalgebra (|A ||> B|) & {c : C & m_corec C c = m.1}} _).
  - serapply (trunc_equiv' {
        ap : {a : A & m_label m.1 = a} &
          ∀ b : B ap.1, {
            mp : {m' : M &
                transport (fun l ⇒ B l → M) ap.2 (m_arg m.1) b = m'} &
              merely {C : Coalgebra (|A ||> B|) &
                {c : C & m_corec C c = mp.1}}}}).
    refine (equiv_compose' _ (equiv_sigma_assoc _ _)^-1).
    refine (equiv_compose' (equiv_sigma_assoc _ _) _).
    apply equiv_functor_sigma_id; intros a.
    transitivity {
        f : B a → M' & {
          p : m_label m.1 = a &
            transport (fun a ⇒ B a → M) p (m_arg m.1) = pr1 o f}}. {
      refine (equiv_compose' (equiv_sigma_symm _) _).
      apply equiv_functor_sigma_id; intros p.
      transitivity {
          f : B a → M' &
            ∀ b, transport (fun a' ⇒ B a' → M) p (m_arg m.1) b =
              (f b).1}. {
        refine (equiv_compose' (equiv_sigT_coind (fun _ ⇒ M')
            (fun b m' ⇒ transport (fun a' : A ⇒ B a' → M) p (m_arg m.1) b =
              m'.1))^-1 _).
        apply equiv_functor_forall_id; intros b.
        refine (equiv_compose' _ (equiv_sigma_assoc _ _)^-1).
        refine (equiv_compose' (equiv_sigma_assoc _ _) _).
        apply equiv_functor_sigma_id; intros m0.
        simpl.
        apply equiv_sigma_symm0.
      }
      apply equiv_functor_sigma_id; intros f.
      apply equiv_path_forall.
    }
    apply equiv_functor_sigma_id; intros f.
    simpl.
    exact (equiv_path_sigma (fun a ⇒ B a → M) (m_label m.1; m_arg m.1)
            (a; pr1 o f)).
  - destruct m as [m0 pre]; simpl.
    intros [C [c p] ].
    serapply existT.
    + ∃ (C c).1.
      exact (m_corec' C o (C c).2).
    + simpl.
      apply (transitivity (ap M p^)).
      serapply path_sigma'.
      × apply m_beta_label.
      × apply m_beta_arg.
  - exact m.2.
Defined.

Definition m_out' (m : M') :=
(m_out_p' m).1.

Definition m_label' (m : M') : A :=
(m_out' m).1.

Definition m_arg' (m : M') (b : B (m_label' m)) : M' :=
(m_out' m).2 b.

Goal ∀ X step (x : X),
  m_label' (m_corec' step x) = (step x).1.
Proof.
  reflexivity.
Qed.

Goal ∀ X step (x : X) b,
  m_arg' (m_corec' step x) b = m_corec' step ((step x).2 b).
Proof.
  reflexivity.
Qed.

Lemma M'_equiv_M : M' <~> M.
Proof.
  serapply equiv_adjointify.
  - exact pr1.
  - intros m.
    ∃ m.
    apply tr.
    ∃ M.
    ∃ m.
    exact (ap10 m_eta_id m).
  - intros m.
    reflexivity.
  - intros [m p].
    simpl.
    serapply path_sigma'.
    + reflexivity.
    + simpl.
      apply path_ishprop.
Defined.


Definition M_coalg' := Build_Coalgebra (| A ||> B |) M' m_out'.
Axiom is_final_M' : is_final M_coalg'.

End M_with_Conversion.

Arguments M' _ _.
Arguments m_label' {_ _ _} _.
Arguments m_arg' {_ _ _} _ _.
Arguments m_corec' {_ _ _} _ _.