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 ivar_container i
    | pe_const kconst_container k
    | pe_sum e1 e2pe_to_container e1 + pe_to_container e2
    | pe_prod e1 e2pe_to_container e1 × pe_to_container e2
    | pe_expo e1 e2pe_to_container e1 pe_to_container e2
    | pe_mu emu_container (pe_to_container e)
    | pe_nu enu_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.