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.