# 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 aB 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 aB 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 lB 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 aB 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' : AB 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 aB 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.
- 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' {_ _ _} _ _.