Library Containers.Substitution

Require Export Containers.Container.
Require Import Containers.Equivalences.

Definition subst_functor {I J}
  (f : (I → Type) → Type) (σ : I → (J → Type) → Type) :=
  fun X ⇒ f (fun i ⇒ σ i X).

Definition subst_container {I J}
  (c : Container I) (σ : I → Container J) :=
  let (S, P) := c in
  {s : S & ∀ i : I, P i s → c_Shape (σ i)} |>
  fun j sf ⇒ {i : I & {p : P i (sf.1) & c_Positions (σ i) j (sf.2 i p)}}.

Lemma subst_container_correct `{Univalence} {I J}
  (c : Container I) (σ : I → Container J) :
  subst_functor [[c]] (container_extension o σ) = [[subst_container c σ]] .
Proof.
  destruct c as [S P].
  by_extensionality X.
  apply path_universe_uncurried.
  unfold subst_functor.
  unfold container_extension.
  simpl.
  refine (transitivity _ (equiv_sigma_assoc _ _)).
  apply equiv_functor_sigma_id.
  intros s.
  transitivity (
      ∀ i : I,
        {s0 : P i s → c_Shape (σ i) &
        ∀ p, ∀ i0 : J, c_Positions (σ i) i0 (s0 p) → X i0}). {
    apply equiv_functor_forall_id; intros i.
    symmetry. exact (equiv_sigT_coind _ _).
  }
  apply (equiv_composeR' (equiv_sigT_coind _ _)^-1).
  apply equiv_functor_sigma_id.
  intros f.
  apply (transitivity (equiv_functor_forall_id (
      fun _ ⇒ equiv_flip _))).
  apply (transitivity (equiv_flip _)).
  apply equiv_functor_forall_id.
  intros j.
  apply (transitivity (equiv_functor_forall_id
      (fun _ ⇒ equiv_sigT_ind (const _)))).
  erapply equiv_sigT_ind.
Qed.