# Library Containers.Mu_Container

Require Export Containers.Container.
Require Export Containers.Initial_Algebra.
Require Export Containers.W.

Section Mu_Container.

Hypothesis funext : Funext.

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

Definition mu_positions {I}
(c : Container (option I)) (i : I)
(s : W (c_Shape c) (c_Positions c None)) :=
{a : c_Shape c & W_Address s a × c_Positions c (Some i) a}.

Definition mu_container {I : Type} (c : Container (option I)) :
Container I :=
mu_shape c |> mu_positions c.

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

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

Definition mu_W {I} (c : Container (option I)) Γ :=
W (mu_A c Γ) (mu_B c Γ).

Lemma mu_container_correct I Γ (c : Container (option I)) :
[[mu_container c]] Γ <~> mu_W c Γ.
Proof.
intros.
symmetry.
unfold mu_W, mu_A, mu_B.
apply (equiv_composeR' equiv_decorate^-1).
unfold mu_container, mu_shape, mu_positions, container_extension; simpl.
apply equiv_functor_sigma_id; intros w.
transitivity ( a1 i, W_Address w a1 c_Positions c (Some i) a1 Γ i). {
apply equiv_functor_forall_id; intros a1.
apply equiv_flip.
}
transitivity ( i a1, W_Address w a1 c_Positions c (Some i) a1 Γ i). {
apply equiv_flip.
}
transitivity ( i a1, W_Address 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 Mu_Container.