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.