Library Containers.Basic_Containers

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

Definition var_container {I} (i : I) :=
  Unit |> fun i' s ⇒ i' = i.

Lemma var_container_correct `{Funext} {I} (i : I) (Γ : I → Type) :
  [[var_container i]] Γ <~> Γ i.
Proof.
  unfold container_extension; simpl.
  serapply equiv_adjointify.
  - exact (fun uf ⇒ uf.2 i idpath).
  - intros a.
    ∃ tt.
    intros i' p.
    destruct p.
    exact a.
  - done.
  - intros [u f].
    destruct u.
    f_ap.
    by_extensionality i'.
    by_extensionality p.
    destruct p.
    done.
Qed.

Definition const_container {I} (K : Type) : Container I :=
  K |> fun _ _ ⇒ Empty.

Lemma const_container_correct `{Funext} {I} (K : Type) (Γ : I → Type) :
  [[const_container K]] Γ <~> K.
Proof.
  unfold container_extension; simpl.
  erapply equiv_sigma_contr.
Defined.

Definition sum_container {I} (c1 c2 : Container I) :=
  c_Shape c1 + c_Shape c2 |>
    fun i shape ⇒
      match shape with
        | inl s1 ⇒ c_Positions c1 i s1
        | inr s2 ⇒ c_Positions c2 i s2
      end.

Notation "c1 + c2" := (sum_container c1 c2) : container_scope.

Lemma sum_container_correct {I} (c1 c2 : Container I) (Γ : I → Type) :
  [[c1 + c2]] Γ <~> [[c1]] Γ + [[c2]] Γ.
Proof.
  unfold container_extension.
  simpl.
  serapply equiv_adjointify.
  - exact (
      fun sf ⇒
        match sf with
          | (inl s1; f1) ⇒ inl (s1; f1)
          | (inr s2; f2) ⇒ inr (s2; f2)
        end).
  - exact (
      fun sfsf ⇒
        match sfsf with
          | inl (s1; f1) ⇒ (inl s1; f1)
          | inr (s2; f2) ⇒ (inr s2; f2)
        end).
  - intros [ [s1 f1] | [s1 f1] ]; done.
  - intros [ [s1 | s2] f]; done.
Defined.

Definition product_container {I} (c1 c2 : Container I) :=
  c_Shape c1 × c_Shape c2 |>
    fun i s ⇒ c_Positions c1 i (fst s) + c_Positions c2 i (snd s).

Notation "c1 * c2" := (product_container c1 c2) : container_scope.

Lemma product_container_correct `{Funext} {I}
      (c1 c2 : Container I) (Γ : I → Type) :
  [[c1 × c2]] Γ <~> [[c1]] Γ × [[c2]] Γ.
Proof.
  symmetry.
  unfold container_extension; simpl.
  apply (transitivity equiv_intensional_choice_finite).
  apply equiv_functor_sigma_id; intros [s1 s2]; simpl.
  apply (transitivity (equiv_prod_coind _ _)).
  apply equiv_functor_forall_id; intros i.
  apply equiv_sum_distributive.
Defined.

Definition expo_container {I}
  (c1 : Container Empty) (c2 : Container I) :=
  (c_Shape c1 → c_Shape c2) |>
  fun i s ⇒ ∃ s1 : c_Shape c1, c_Positions c2 i (s s1).

Notation "c1 -> c2" := (expo_container c1 c2) : container_scope.

Lemma expo_container_correct `{Funext} {I}
      (c1 : Container Empty) (c2 : Container I) Γ :
  [[c1 → c2]] Γ <~> ([[c1]] (const Empty) → [[c2]] Γ).
Proof.
  destruct c1 as [S1 P1].
  destruct c2 as [S2 P2].
  unfold container_extension.
  simpl.
  unfold const.
  serapply equiv_adjointify.
  - intros [s f] [s1 f1].
    ∃ (s s1).
    exact (fun i p2 ⇒ f i (s1; p2)).
  - intros f.
    serapply existT.
    + intros s1.
      eapply projT1.
      apply f.
      ∃ s1.
      intros i.
      destruct i.
    + intros i.
      simpl.
      intros [s1 p2].
      destruct (f (s1; fun i : Empty ⇒
        match i as e return (P1 e s1 → Empty) with end)) as [s2 f2].
      apply f2.
      apply p2.
  - intros f.
    by_extensionality sf1.
    destruct sf1 as [s1 f1].
    f_ap; f_ap.
    by_extensionality i.
    done.
  - done.
Qed.