Library Containers.Strictly_Positive_Types

Require Export Containers.Container.
Require Import Containers.Basic_Containers.
Require Import Containers.Mu_Container.
Require Import Containers.Nu_Container.

Inductive PE I :=
| pe_var : I → PE I
| pe_const : Type → PE I
| pe_sum : PE I → PE I → PE I
| pe_prod : PE I → PE I → PE I
| pe_expo : PE Empty → PE I → PE I
| pe_mu : PE (option I) → PE I
| pe_nu : PE (option I) → PE I.

Inductive type_implements_pe {I} :
  (I → Type) → PE I → Type → Type :=
| tipe_var Γ i : type_implements_pe Γ (pe_var I i) (Γ i)
| tipe_const Γ k : type_implements_pe Γ (pe_const I k) k
| tipe_sum Γ e1 e2 x1 x2 :
  type_implements_pe Γ e1 x1 →
  type_implements_pe Γ e2 x2 →
  type_implements_pe Γ (pe_sum I e1 e2) (x1 + x2)
| tipe_prod Γ e1 e2 x1 x2 :
  type_implements_pe Γ e1 x1 →
  type_implements_pe Γ e2 x2 →
  type_implements_pe Γ (pe_prod I e1 e2) (x1 × x2)
| tipe_expo Γ e1 e2 x1 x2 :
  @type_implements_pe Empty (const Empty) e1 x1 →
  type_implements_pe Γ e2 x2 →
  type_implements_pe Γ (pe_expo I e1 e2) (x1 → x2)
| tipe_mu Γ e F (A : Algebra F) :
  (∀ x, @type_implements_pe (option I) (Γ ;; x) e (F x)) →
  is_initial A →
  type_implements_pe Γ (pe_mu I e) A
| tipe_nu Γ e F (A : Coalgebra F) :
  (∀ x, @type_implements_pe (option I) (Γ ;; x) e (F x)) →
  is_final A →
  type_implements_pe Γ (pe_nu I e) A.

Notation "Γ |- e ~> A" := (type_implements_pe Γ e A) (at level 50).

Fixpoint pe_to_container {I} (exp : PE I) : Container I :=
  match exp with
    | pe_var i ⇒ var_container i
    | pe_const k ⇒ const_container k
    | pe_sum e1 e2 ⇒ pe_to_container e1 + pe_to_container e2
    | pe_prod e1 e2 ⇒ pe_to_container e1 × pe_to_container e2
    | pe_expo e1 e2 ⇒ pe_to_container e1 → pe_to_container e2
    | pe_mu e ⇒ mu_container (pe_to_container e)
    | pe_nu e ⇒ nu_container (pe_to_container e)
  end.

Lemma container_implements_pe `{Univalence} {I} (e : PE I) :
  ∀ Γ, Γ |- e ~> ([[pe_to_container e]] Γ).
Proof.
  induction e; intros Γ; simpl.
  - rewrite (path_universe (var_container_correct _ _)).
    by constructor.
  - rewrite (path_universe (const_container_correct _ _)).
    by constructor.
  - rewrite (path_universe (sum_container_correct _ _ _)).
    by constructor.
  - rewrite (path_universe (product_container_correct _ _ _)).
    by constructor.
  - rewrite (path_universe (expo_container_correct _ _ _)).
    by constructor.
  - rewrite (path_universe_uncurried (mu_container_correct _ _ _ _)).
    apply (tipe_mu Γ e (container_functor Γ (pe_to_container e))
        (W_alg _ _)).
    + intros x.
      rewrite container_functor_is_container_fun.
      apply IHe.
    + apply W_initial.
  - rewrite (path_universe_uncurried (nu_container_correct _ _ _ _)).
    apply (tipe_nu Γ e (container_functor Γ (pe_to_container e))
        (m_coalg _ _)).
    + intros x.
      rewrite container_functor_is_container_fun.
      apply IHe.
    + apply is_final_m.
Qed.