# Library Containers.Nu_Container

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

Section Nu_Container.

Hypothesis funext : Funext.

Definition nu_shape {I} (c : Container (option I)) : Type :=
M (c_Shape c) (c_Positions c None).

Definition nu_positions {I}
(c : Container (option I)) (i : I)
(s : M (c_Shape c) (c_Positions c None)) :=
{a : c_Shape c & Addr s a × c_Positions c (Some i) a}.

Definition nu_container {I : Type} (c : Container (option I)) :
Container I :=
nu_shape c |> nu_positions c.

Definition nu_A {I} (c : Container (option I)) Γ :=
{s : c_Shape c & i, c_Positions c (Some i) s Γ i}.

Definition nu_B {I} (c : Container (option I)) Γ : nu_A c Γ Type :=
c_Positions c None o pr1.

Definition nu_M {I} (c : Container (option I)) Γ :=
M (nu_A c Γ) (nu_B c Γ).

Lemma nu_container_correct I Γ (c : Container (option I)) :
[[nu_container c]] Γ <~> nu_M c Γ.
Proof.
intros.
symmetry.
unfold nu_M, nu_A, nu_B.
apply (equiv_composeR' (equiv_decorate_M _ (c_Shape c)
(fun s i, c_Positions c (Some i) s Γ i)
(c_Positions c None))).
unfold nu_container, nu_shape, nu_positions, container_extension; simpl.
apply equiv_functor_sigma_id; intros w.
transitivity ( a1 i, Addr w a1 c_Positions c (Some i) a1 Γ i). {
apply equiv_functor_forall_id; intros a1.
apply equiv_flip.
}
transitivity ( i a1, Addr w a1 c_Positions c (Some i) a1 Γ i). {
apply equiv_flip.
}
transitivity ( i a1, Addr w a1 × c_Positions c (Some i) a1 Γ i). {
apply equiv_functor_forall_id; intros i.
apply equiv_functor_forall_id; intros a1.
erapply equiv_prod_ind.
}
apply equiv_functor_forall_id; intros i.
erapply equiv_sigT_ind.
Qed.

End Nu_Container.