Library Containers.Container

Require Export Containers.Functor.
Require Import Containers.Equivalences.

Record Unary_Container := {
  uc_Shape : Type;
  uc_Positions : uc_Shape → Type
}.

Notation "S ||> P" :=
  (Build_Unary_Container S P) (at level 100).

Definition unary_container_functor (c : Unary_Container) : Functor.
Proof.
  serapply Build_Functor.
  - exact (fun X ⇒ {s : uc_Shape c & uc_Positions c s → X}).
  - exact (fun _ _ f sl ⇒ (sl.1; f o sl.2)).
  - reflexivity.
  - reflexivity.
Defined.

Notation "(| c |)" := (unary_container_functor c).

Record Container I := {
  c_Shape : Type;
  c_Positions : I → c_Shape → Type
}.

Arguments Build_Container {_} _ _.
Arguments c_Shape {_} _.
Arguments c_Positions {_} _ _ _.

Bind Scope container_scope with Container.

Notation "S |> P" :=
  (Build_Container S P) (at level 100).

Definition container_extension {I} (c : Container I) :=
  fun Γ ⇒ {s : c_Shape c & ∀ i : I, c_Positions c i s → Γ i}.

Notation "[[ c ]]" := (container_extension c).

Definition container_functor {I}
    (Γ : I → Type) (c : Container (option I)) :=
  (| {s : c_Shape c & ∀ i, c_Positions c (Some i) s → Γ i} ||>
    fun s' ⇒ c_Positions c None s'.1 |).

Notation "f ;; a" := (
  fun x ⇒
    match x with
      | Some x' ⇒ f x'
      | None ⇒ a
    end)
(at level 60).

Lemma container_functor_is_container_fun `{Univalence}
    I Γ (c : Container (option I)) :
  f_fun (container_functor Γ c) = fun X ⇒ [[c]] (Γ ;; X).
Proof.
  apply apD10^-1; intros X.
  unfold container_extension; simpl.
  apply path_universe_uncurried.
  transitivity {
      s : c_Shape c & {
        _ : ∀ i : I, c_Positions c (Some i) s → Γ i &
        c_Positions c None s → X
      }
    }. {
    symmetry.
    erapply equiv_sigma_assoc.
  }
  apply equiv_functor_sigma_id; intros s.
  transitivity (
      (∀ i : I, c_Positions c (Some i) s → Γ i) ×
      (c_Positions c None s → X)). {
    apply equiv_sigma_prod0.
  }
  erapply equiv_option_ind.
  Unshelve.
  exact _.
Qed.