Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.

Inductive Types :=
| Pos : PosTypes → Types
| Neg : NegTypes → Types
with PosTypes :=
| Prod : Types → Types → PosTypes
with NegTypes :=
| To : Types → Types → NegTypes.

Coercion Pos : PosTypes >-> Types.
Coercion Neg : NegTypes >-> Types.

Notation "A ⇒ B" := (To A B)
  (at level 70, right associativity).
Notation "A ⋆ B" := (Prod A B)
  (at level 65, right associativity).

Definition context := nat → option Types.
Definition ext_context (Γ: context)(A: Types): context
  := fun n =>
       match n with
         | 0 => Some A
         | S k => Γ k
       end.
Notation "Γ ▹ A" := (ext_context Γ A)
  (at level 73, left associativity).

Definition intCtxt (Γ: context)(I: Types → Type): Type
  := forall v T, Γ(v) = Some T → I T.

Definition lookup {Γ n T I} (ρ: intCtxt Γ I)(q: Γ n = Some T): I T
  := ρ n T q.

Definition ext_int {Γ I T}(ρ: intCtxt Γ I)(t: I T): intCtxt (Γ ▹ T) I.
intro n; case n.
- intros T' q.
  simpl in q.
  inversion q as [q'].
  rewrite q' in t.
  exact t.
- intros n' T' q.
  eapply ρ; exact q.
Defined.

Inductive Ty (Γ Δ: context): Type:=
| ty_cut: ∀ A,
(*  Γ ⊢ p:A | Δ  →  Γ | e:A ⊢ Δ → <p|e>: (Γ⊢Δ)  *)
   Ty_r Γ Δ A → Ty_l Γ Δ A → Ty Γ Δ
with Ty_r (Γ Δ: context): Types → Type :=
| ty_var_r : ∀ k A,
(*  (a:A) ∈ Γ     →  Γ ⊢ a:A | Δ *)
    Γ(k) = Some A → Ty_r Γ Δ A
| ty_app_r: ∀ A B,
(*  Γ,a:A ⊢ p:B | Δ  →  Γ ⊢ λa.p:(A ⇒ B)  *)
    Ty_r (Γ ▹ A) Δ B → Ty_r Γ Δ (A ⇒ B)
| ty_pair_r: ∀ A B,
(*  Γ ⊢ p:A | Δ  →  Γ ⊢ q:B | Δ → Γ ⊢ (p,q):A x B | Δ  *)
    Ty_r Γ Δ A → Ty_r Γ Δ B → Ty_r Γ Δ (A ⋆ B)
| ty_mu_r: ∀ A,
(*  c: (Γ ⊢ Δ,α:A)  →  Γ ⊢ µα.c:A | Δ  *)
    Ty Γ (Δ ▹ A) → Ty_r Γ Δ A
with Ty_l (Γ Δ:context): Types → Type :=
| ty_var_l: ∀ k A,
    Δ(k) = Some A →
    Ty_l Γ Δ A
| ty_app_l: ∀ A B,
    Ty_r Γ Δ A →
    Ty_l Γ Δ B →
    Ty_l Γ Δ (A ⇒ B)
| ty_mut_l: ∀ A,
    Ty (Γ ▹ A) Δ →
    Ty_l Γ Δ A
| ty_pair_l:∀ A B,
    Ty (Γ ▹ A ▹ B) Δ →
    Ty_l Γ Δ (A ⋆ B)
.

Notation "Γ ⊢t A § Δ" := (Ty_r Γ Δ A) (at level 74, no associativity).
Notation "Γ $ A ⊢e Δ" := (Ty_l Γ Δ A) (at level 74, no associativity).
Notation "Γ ⊢c Δ" := (Ty Γ Δ) (at level 75, no associativity).

Parameter pole: Type.

 Definition pole := False. 

 Definition pole := { c: Tm & value c }. 

Definition orth (T: Type): Type := T → pole.

Definition biorth {T} : T → orth (orth T) := fun t k => k t.

Module Type Rea.
Parameter intCV : Types → Type.
Parameter intTV : Types → Type.
Parameter env_r : context → Type.
Parameter env_l : context → Type.
Parameter rea_r : forall Γ Δ A, Ty_r Γ Δ A → env_r Γ → env_l Δ → orth (intCV A).
Parameter rea_l : forall Γ Δ A, Ty_l Γ Δ A → env_r Γ → env_l Δ → orth (intTV A).
End Rea.

Reserved Notation "'intT' T"
    (at level 10, no associativity).
Reserved Notation "'intC' T"
    (at level 10, no associativity).

  || A → B ||_E = | A | × || B ||
   | A × B |_V  = | A | × | B |

Module Rea1 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intT A * intC B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intT A * intT B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).

Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorthC {T} : intCV T → intC T
  := match T return intCV T → intC T with
       | Pos _ => fun t => t
       | Neg _ => biorth
     end.

Definition biorthT {T} : intTV T → intT T
  := match T return intTV T → intT T with
       | Pos _ => biorth
       | Neg _ => fun t => t
     end.

Definition cut {T} : intT T → intC T → pole
  := match T with
       | Pos P => fun t e => t e
       | Neg N => fun t e => e t
     end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intT T).
Definition env_l (Δ: context): Type
  := intCtxt Δ (fun T => intC T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => lookup ρ a
    |ty_app_r t =>
     fun π =>
       let (u,e) := π in
       (* This suggests that: 
              <λx.t|u.e> → <t[u/x]|e> 
          for any u, this is call-by-name fashion *)
       cut (rea_r t (ext_int ρ u) σ) e
    |ty_mu_r c=>
        fun α => rea c ρ (ext_int σ (biorthC α))
    |ty_pair_r p q =>
     fun π => π (rea_r p ρ σ, rea_r q ρ σ)
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A:=
  match H with
    |ty_var_l _ α => lookup σ α
    |ty_app_l u π =>
     fun t =>
       t (rea_r u ρ σ, rea_l π ρ σ)
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ (biorthT a)) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
      (* This suggests that:
               <(t,u)|µ~(x,y).c> → c[t/x,u/x]
        for any t,u, this is again call-by-name fashion *)
       (rea c (ext_int (ext_int ρ p) q) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea1.

  || A → B ||_E = | A |_V × || B ||
   | A × B |_V  = | A | × | B |

Module Rea2 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intTV A * intC B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intT A * intT B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).

Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorth {T} : T → orth (orth T) := fun t k => k t.

Definition biorthT {T} : intTV T → intT T :=
  match T return intTV T → intT T with
    | Pos _ => biorth
    | Neg _ => fun t => t
  end.
Definition biorthC {T} : intCV T → intC T :=
  match T return intCV T → intC T with
    | Pos _ => fun t => t
    | Neg _ => biorth
  end.

Definition cut {T} : intT T → intC T → pole :=
  match T with
    | Pos P => fun t e => t e
    | Neg N => fun t e => e t
  end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intT T).
Definition env_l (Δ: context): Type
  := intCtxt Δ (fun T => intCV T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => lookup ρ a
    |ty_app_r t =>
     fun π =>
       let (u,e) := π in
       (* This suggests that:
               <λx.t|V.e> → <t[V/x]|e> 
       for values V (this is witnessed by the fact that u is applied biorthT): 
       this is a call-by-value fashion for the arrow type. *)
       cut (rea_r t (ext_int ρ (biorthT u)) σ) e
    |ty_mu_r c=>
       fun α => rea c ρ (ext_int σ (α))
    |ty_pair_r p q =>
     fun π => π (rea_r p ρ σ, rea_r q ρ σ)
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A :=
  match H with
    |ty_var_l _ α => biorthC (lookup σ α)
    |ty_app_l u π =>
    (* This suggests that when considering a context |u.e>, u has to be evaluated first:
     this is a call-by-value fashion. Given as a CPS translation, this would give:
           [u.e] f = [u]  (λV. f V [e]) 
    *)
     (fun f => cut (rea_r u ρ σ) (fun vu => f (vu,(rea_l π ρ σ))))
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ (biorthT a)) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
    (* This suggests that:
              <(t,u)|µ~(x,y).c> → c[t/x,u/y]
       for any t,u, this is a call-by-name fashion for the product type.*)
       (rea c (ext_int (ext_int ρ p) q) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea2.

  || A → B ||  = | A | × || B ||
   | A × B |V  = | A |V × | B |V

Module Rea3 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intT A * intC B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intTV A * intTV B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).

Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorthC {T} : intCV T → intC T :=
  match T return intCV T → intC T with
    | Pos _ => fun t => t
    | Neg _ => biorth
  end.
Definition biorthT {T} : intTV T → intT T :=
  match T return intTV T → intT T with
    | Pos _ => biorth
    | Neg _ => fun t => t
  end.

Definition cut {T} : intT T → intC T → pole :=
  match T with
    | Pos P => fun t e => t e
    | Neg N => fun t e => e t
  end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intT T).

Definition env_l (Δ: context): Type
  := intCtxt Δ (fun T => intC T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => (lookup ρ a)
    |ty_app_r t =>
     fun π => let (u,e) := π in
      (* This suggests that:
                <λx.t|u.e> → <t[u/x]|e> 
         for any u, this is call-by-name fashion for the arrow type. *)
       cut (rea_r t (ext_int ρ u) σ) e
    |ty_mu_r c=>
     fun α => rea c ρ (ext_int σ (biorthC α))
    |ty_pair_r p q =>
    (* This suggests that when considering pairs, each of their components have to be evaluated first: 
    this is a call-by-value fashion (for positive types).
    Given as a CPS translation, this would give:
           [(p,q)] k = [p] (λa. [q]  (λb. k (a,b) )) 
    *)
     fun π =>
       cut (rea_r p ρ σ) (fun va => cut (rea_r q ρ σ) (fun vb => π (va,vb)))
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A:=
  match H with
    |ty_var_l _ α => lookup σ α
    |ty_app_l u π =>
     (fun f => f (rea_r u ρ σ,rea_l π ρ σ))
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ (biorthT a)) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
    (* We observe here that contexts of the shape µ~(x,y).c indeed expect pairs of values to reduce,
       as witnessed by the fact that this values are applied biorthT *)
       (rea c (ext_int (ext_int ρ (biorthT p)) (biorthT q)) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea3.

  || A → B ||_E = | A |_V × || B ||
   | A × B |_V  = | A |_V × | B |_V

Module Rea4 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intTV A * intC B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intTV A * intTV B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).
Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorthC {T} : intCV T → intC T :=
  match T return intCV T → intC T with
    | Pos _ => fun t => t
    | Neg _ => biorth
  end.
Definition biorthT {T} : intTV T → intT T :=
  match T return intTV T → intT T with
    | Pos _ => biorth
    | Neg _ => fun t => t
  end.

Definition cut {T} : intT T → intC T → pole :=
  match T with
    | Pos P => fun t e => t e
    | Neg N => fun t e => e t
  end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intTV T).

Definition env_l (Δ: context): Type
  := intCtxt Δ (fun T => intC T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => biorthT (lookup ρ a)
    |ty_app_r t =>
     fun π =>
       let (u,e) := π in
       cut (rea_r t (ext_int ρ u) σ) e
    |ty_mu_r c=>
     fun α => rea c ρ (ext_int σ (biorthC α))
    |ty_pair_r p q =>
    (* We recognize the call-by-value fashion for the product type. *)
     fun π =>
       cut (rea_r p ρ σ) (fun va => cut (rea_r q ρ σ) (fun vb => π (va,vb)))
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A:=
  match H with
    |ty_var_l _ α => lookup σ α
    |ty_app_l u π =>
      (* We recognize the call-by-value fashion for the arrow type. *)
     (fun f => cut (rea_r u ρ σ) (fun r => f (r,rea_l π ρ σ)))
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ a) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
       (rea c (ext_int (ext_int ρ p) q) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea4.

(* We can also imagine many different ways to define truth and falsity values
by mixing the previous definitions. We give a few more definitions to illustrate this. *)

  || A → B ||_E = | A |_V × || B ||_E
   | A × B |V  = | A | × | B |

Module Rea2bis <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intTV A * intCV B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intT A * intT B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).

Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorth {T} : T → orth (orth T) := fun t k => k t.

Definition biorthT {T} : intTV T → intT T :=
  match T return intTV T → intT T with
    | Pos _ => biorth
    | Neg _ => fun t => t
  end.
Definition biorthC {T} : intCV T → intC T :=
  match T return intCV T → intC T with
    | Pos _ => fun t => t
    | Neg _ => biorth
  end.

Definition cut {T} : intT T → intC T → pole :=
  match T with
    | Pos P => fun t e => t e
    | Neg N => fun t e => e t
  end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intT T).
Definition env_l (Δ: context): Type
  := intCtxt Δ (fun T => intCV T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => lookup ρ a
    |ty_app_r t =>
     fun π =>
       let (u,e) := π in
       (* This suggests that:
        <λx.t|V.e> → <t[V/x]|e> 
        for values V*)
       (rea_r t (ext_int ρ (biorthT u)) σ) e
    |ty_mu_r c=>
       fun α => rea c ρ (ext_int σ (α))
    |ty_pair_r p q =>
     fun π => π (rea_r p ρ σ, rea_r q ρ σ)
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A :=
  match H with
    |ty_var_l _ α => biorthC (lookup σ α)
    |ty_app_l u π =>
    (* This suggests that when considering a context |u.e>, 
    u and e have to be evaluated first: this is a call-by-value fashion.
    Given as a CPS translation, this would give:
           [u.e] f = [e] (λE. [u]  (λV. f V E)) 
    *)
     (fun f =>
       cut (fun ve => cut (rea_r u ρ σ) (fun vu => f (vu,ve))) (rea_l π ρ σ))
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ (biorthT a)) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
       (* This suggests that:
                <(t,u)|µ~(x,y).c> → c[t/x,u/y]
         for any t,u, this is again call-by-name fashion *)
       (rea c (ext_int (ext_int ρ p) q) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea2bis.

  || A → B ||_E = | A | × || B ||_E
   | A × B |_V  = | A | × | B |

Module Rea1bis <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intT A * intCV B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intT A * intT B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).

Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorthT {T} : intTV T → intT T :=
  match T return intTV T → intT T with
    | Pos _ => biorth
    | Neg _ => fun t => t
  end.

Definition biorthC {T} : intCV T → intC T
  := match T return intCV T → intC T with
       | Pos _ => fun t => t
       | Neg _ => biorth
     end.

Definition cut {T} : intT T → intC T → pole :=
  match T with
    | Pos P => fun t e => t e
    | Neg N => fun t e => e t
  end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intT T).

Definition env_l (Delta: context): Type
  := intCtxt Delta (fun T => intCV T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => lookup ρ a
    |ty_app_r t =>
     fun π =>
       let (u,e) := π in
       (* This suggests that <λx.t|u.E> → <tu/x | E> for any u but only for E. *)
       (rea_r t (ext_int ρ u) σ) e
    |ty_mu_r c=>
     fun α => rea c ρ (ext_int σ α)
    |ty_pair_r p q =>
     fun π => π (rea_r p ρ σ, rea_r q ρ σ)
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A:=
  match H with
    |ty_var_l _ α => biorthC (lookup σ α)
    |ty_app_l u π =>
     (fun f =>
       cut (fun r => f (rea_r u ρ σ,r)) (rea_l π ρ σ))
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ (biorthT a)) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
     (* This suggests that <(t,u)|µ~(x,y).c> → ct/x,u/x* for any t,u, this is again call-by-name fashion *)
       (rea c (ext_int (ext_int ρ p) q) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea1bis.

  || A → B ||_E = | A |V × || B ||_E
   | A × B |V  = | A |V × | B |V

Module Rea4bis <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
    | A ⇒ B => (intTV A * intCV B)%type
  end
with intTP (P : PosTypes): Type :=
  match P with
    | Prod A B => (intTV A * intTV B)%type
  end
with intCV T :=
  match T with
    | Neg N => intCN N
    | Pos P => orth (intTP P)
  end
with intTV T :=
  match T with
    | Pos P => intTP P
    | Neg N => orth (intCN N)
  end
where "'intT' T" := (orth (intCV T))
  and "'intC' T" := (orth (intTV T)).

Notation "'|' A '|_V'":=(intTV A) (at level 80, no associativity).
Notation "'‖' A '‖_E'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

Definition biorthC {T} : intCV T → intC T :=
  match T return intCV T → intC T with
    | Pos _ => fun t => t
    | Neg _ => biorth
  end.
Definition biorthT {T} : intTV T → intT T :=
  match T return intTV T → intT T with
    | Pos _ => biorth
    | Neg _ => fun t => t
  end.

Definition cut {T} : intT T → intC T → pole :=
  match T with
    | Pos P => fun t e => t e
    | Neg N => fun t e => e t
  end.

Definition env_r (Γ: context): Type
  := intCtxt Γ (fun T => intTV T).

Definition env_l (Δ: context): Type
  := intCtxt Δ (fun T => intCV T).

Fixpoint rea_r (Γ Δ:context) (A:Types) (H: Γ ⊢t A § Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intT A :=
  match H with
    |ty_var_r _ a => biorthT (lookup ρ a)
    |ty_app_r t =>
     fun π =>
       let (u,e) := π in
       (rea_r t (ext_int ρ u) σ) e
    |ty_mu_r c=>
     fun α => rea c ρ (ext_int σ α)
    |ty_pair_r p q =>
     fun π =>
       cut (rea_r p ρ σ) (fun va => cut (rea_r q ρ σ) (fun vb => π (va,vb)))
  end
with rea_l (Γ Δ:context) (A:Types) (H: Γ $ A ⊢e Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: intC A:=
  match H with
    |ty_var_l _ α => biorthC (lookup σ α)
    |ty_app_l u π =>
     (fun f =>
       cut (rea_r u ρ σ) (fun r => cut (fun ve => f (r,ve)) (rea_l π ρ σ)))
    |ty_mut_l c=>
     fun a => rea c (ext_int ρ a) σ
    |ty_pair_l c =>
     fun pair =>
       let (p,q):= pair in
       (rea c (ext_int (ext_int ρ p) q) σ)
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_r Γ) (σ: env_l Δ) {struct H}: pole :=
  match H with
    | ty_cut t π =>
      cut (rea_r t ρ σ) (rea_l π ρ σ)
  end
.
End Rea4bis.