(* Set Universe Polymorphism. *)
(* Set Primitive Projections. *)
(* Set Polymorphic Inductive Cumulativity. *)
Require Import List.
Require Import Streams.
Require Import ssreflect.
Set Implicit Arguments.
Set Primitive Projections.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section DialogueTrees.

Variables (X Y : Type).
Implicit Type (A B : Type).

(* Escardo's dialogue monad *)
Inductive Dialogue A : Type :=
 | êta : A -> Dialogue A
 | bêta : (Y -> Dialogue A) -> X -> Dialogue A.

(* Interpretation of a dialogue tree d as a function (X -> Y) -> A.
  The first argument of the latter function is an oracle used to decode
  the dialogue tree into an inhabitant of A. *)
(* !!! swapped arguments from previous version *)

Fixpoint dialogue A (d : Dialogue A) (oracle : X -> Y) : A :=
  match d with
  | êta  z => z
  | bêta f y => dialogue (f (oracle y)) oracle
  end.


Definition eloquent A (f : (X -> Y) -> A) :=
  {d : Dialogue A & forall alpha, f alpha = (dialogue d) alpha}.


Fixpoint Mu A (d : Dialogue (Dialogue A)) : Dialogue A :=
  match d with
  | êta d' => d'
  | bêta g n => bêta (fun m => Mu (g m)) n
  end.


Fixpoint Bind A B (f : A -> Dialogue B)  (d : Dialogue A) : Dialogue B :=
  match d with
  | êta z => f z
  | bêta g n => bêta (fun m => Bind f (g m)) n
end.


Lemma NaturBindDialogue A B (f : A -> Dialogue B) (oracle : X -> Y) (d : Dialogue A) :
  (dialogue (Bind f d) oracle) = (dialogue (f (dialogue d oracle)) oracle).
Proof.
induction d as [| d ihd x]; trivial.
now simpl; rewrite (ihd (oracle x)).
Qed.


Definition Map A B (f : A -> B) (d : Dialogue A) : Dialogue B :=
  Bind (fun x => êta (f x)) d.


Lemma NaturMapEta (f : X -> Y) :
  ((fun x => Map f (êta x)) = (fun x => (êta (f x)))).
Proof. reflexivity. Qed.


Lemma NaturMapDialogue A B (f : A -> B) (oracle : X -> Y) (d : Dialogue A) :
  (f (dialogue d oracle)) = (dialogue (Map f d) oracle).
Proof.
  induction d as [| d ihd x]; trivial.
now simpl; rewrite (ihd (oracle x)).
Qed.

(* From mathcomp Require Import all_ssreflect. *)


(* Definition EqList X (Y : eqType) (alpha : X -> Y) (s : seq (X * Y)) := *)
(*   all (fun u => u.2 == alpha u.1) s.   *)

(*Inductive EqList : (list (X * Y)) -> (X -> Y) -> Type :=
| EqNil : forall (alpha : X -> Y), EqList nil alpha
| EqCons : forall (l : list (X * Y)) (x : X) (alpha : X -> Y),
    (EqList l alpha) -> (EqList ((x, alpha x) :: l) alpha).


Lemma EqList_invcons (l : list (X * Y)) (x : X) (y : Y) (p : X -> Y) :
  EqList ((x, y) :: l) p -> (p x = y) * EqList l p.
Proof.
  intro EqListp.
  split ; by inversion EqListp.
Qed.

Lemma EqList_Eq : forall (l : list (X * Y)) (alpha : X -> Y),
    EqList l alpha -> forall (x : X) (y : Y),
      In (x,y) l -> alpha x = y.
Proof.
  intros l alpha Heq x y HIn.
  induction Heq.
  - exfalso.
    exact (in_nil HIn).
  - apply in_inv in HIn.  
    case HIn.
    + intro Eq.
      inversion Eq.
      reflexivity.
    + assumption.
Qed.  *)


End DialogueTrees.



Section DialogueStreams.

Variable (Y : Type).
Implicit Type (A B : Type).

(* Dialogue trees with nat labelled inner nodes *)
Definition StreamDialogue := Dialogue nat Y.

Definition stream_dialogue A (d : StreamDialogue A) (alpha : Stream Y) :=
  dialogue d (fun n =>  Str_nth n alpha).

(* analogue of eloquent, but for functions on streams *)
Definition stream_eloquent A (f : (Stream Y) -> A) := 
  {d : StreamDialogue A & forall alpha, f alpha = (stream_dialogue d) alpha}.

End DialogueStreams.



Section NatDialogueStreams.

Variable (Y : Type).

(* Dialogue trees with nat labelled inner nodes and nat labelled leaves*)
Definition NatStreamDialogue := StreamDialogue Y nat.

(* Possibly define a constant for the êta of NatStreamDialogue, so as to get
   rid of the two _ *)

(* Single leaf dialogue labelled with 0 *)
Definition zero' : NatStreamDialogue := êta _ _ 0.

Definition S' : NatStreamDialogue -> NatStreamDialogue := Map S.

End NatDialogueStreams.


Section BranchingNaturalNumbers.

Variable (X Y : Type).

(* A variant of the dialogue monad, for branching natural numbers *)

Inductive BranchingNat :=
| B0 : BranchingNat
| BS : BranchingNat -> BranchingNat
| Bêtanat : (Y -> BranchingNat) -> X -> BranchingNat.

Implicit Type (b : BranchingNat).
Implicit Type oracle : X -> Y.

Fixpoint BNdialogue b oracle : nat :=
  match b with
  | B0 => 0
  | BS b' => S (BNdialogue b' oracle)
  | Bêtanat f x => BNdialogue (f (oracle x)) oracle
  end.


(* would it make sense to abstract BNeloquent and eloquent in a single parameterized
  definition? *)
Definition BNeloquent (f : (X -> Y) -> nat) := 
  {d : BranchingNat & forall alpha, f alpha = (BNdialogue d) alpha}.


Fixpoint BNEta (n : nat) : BranchingNat :=
  match n with
  | 0 => B0
  | S k => BS (BNEta k)
  end.

Lemma NaturBNEtaDialogue (n : nat) alpha : BNdialogue (BNEta n) alpha = n.
Proof.
  induction n as [ | n ihn].
  - reflexivity.
  - now apply eq_S.
Qed.


Fixpoint BNBind (f : nat -> BranchingNat)  b : BranchingNat :=
  match b with
  | B0 => f 0
  | BS bn => (BNBind (fun m => f (S m)) bn)
  | Bêtanat g n => Bêtanat (fun m => BNBind f (g m)) n
  end.


Lemma NaturBNBindDialogue (g : nat -> BranchingNat) oracle b :
  BNdialogue (BNBind g b) oracle = BNdialogue (g (BNdialogue b oracle)) oracle.
Proof.
  elim: b g => [ | b' ihb g | f ihb x g ]; simpl; trivial.
  now rewrite ihb.
Qed.


Definition BNMap (f : nat -> nat) b : BranchingNat :=
  BNBind (fun x => BNEta (f x)) b.

Lemma NaturBNMap_BNEta (f : nat -> nat) (n : nat) :
   BNMap f (BNEta n) = BNEta (f n).
Proof.
  (* have H (g : nat -> nat) (m : nat) : (Bnatun_fun g (Bnatun_Eta m)) = (Bnatun_Eta (g m)). *)
  elim: n f => [ | m ihm f] //.
  now apply: ihm.
Qed.

Lemma NaturBNMap_Dialogue (f : nat -> nat) oracle b :
  f (BNdialogue b oracle) = BNdialogue (BNMap f b) oracle.
Proof.
  elim: b f => [ f | b' ihb f | f ihb x g ].
  - now rewrite NaturBNEtaDialogue.
  - exact: ihb. 
  - exact: ihb. 
Qed.

(*Definition of the Devale function, which travels down the nodes of a branching natural numbers until it gets to a 0 or Successor. Necessary for the definition of Pnat*)

Fixpoint Devale b oracle :=
  match b with
  | B0 => B0
  | BS k => BS k
  | Bêtanat f x => Devale (f (oracle x)) oracle
  end.


Lemma Devale_notBranching b oracle (f : Y -> BranchingNat) (x : X) :
    Devale b oracle <> Bêtanat f x.
Proof.
  elim: b => [ | | f' Hyp x'] //.
  exact: (Hyp (oracle x')).
Qed.


Lemma Devale_BNdialogue b (oracle : X -> Y) :
    BNdialogue b oracle = BNdialogue (Devale b oracle) oracle.
Proof.
  induction b as [ | | f Hyp x ] ; trivial; exact: Hyp. 
Qed.


Lemma Devale_BNEta (n : nat) (oracle : X -> Y) :
  Devale (BNEta n) oracle = BNEta n. 
Proof.
  now induction n.
Qed.

(*Ways to go from Dialogue nat to BNDialogue*)

Fixpoint DialoguetoBN (d : Dialogue X Y nat) : BranchingNat :=
  match d with
  | êta _ _ n => BNEta n
  | bêta g n => Bêtanat (fun m => DialoguetoBN (g m)) n
  end.


Fixpoint BNtoDialogue b : Dialogue X Y nat :=
  match b with
  | B0 => êta _ _ 0
  | BS bn => Map S (BNtoDialogue bn)
  | Bêtanat g n => bêta (fun m => BNtoDialogue (g m)) n
  end.

(*If FunExt holds on Y -> Dialogue X Y nat, DialoguetoBN is a retraction*)

Lemma Retract_Dialogue_BNdialogue (d : Dialogue X Y nat) :
  (forall f g : Y -> Dialogue X Y nat, (forall y : Y, f y = g y) -> f = g) -> 
  BNtoDialogue (DialoguetoBN d) = d.
Proof.
  intro FunExt.
  induction d as [ n | f ihd x ].
  - induction n as [ | m ihm] ; trivial.
    now simpl ; rewrite ihm.
  - simpl. congr bêta. 
    exact: FunExt.
Qed.

(*DialoguetoBN and BNtoDialogue preserve the dialogue function*)

Lemma EqDialogueBNdialogue (oracle : X -> Y) (d : Dialogue X Y nat) :
  dialogue d oracle = BNdialogue (DialoguetoBN d) oracle.
Proof.
  induction d as [ n | f ihd x ] ; simpl.
  - induction n as [ | n' ihn] ; trivial.
    now rewrite /= - ihn.
  - now rewrite (ihd (oracle x)).
Qed.  


Lemma EqBNdialogueDialogue (oracle : X -> Y)  b :
  BNdialogue b oracle = dialogue (BNtoDialogue b) oracle.
Proof.
  induction b as [ | b' ihb | f ihb x ] ; trivial ; simpl.
  - rewrite - (NaturMapDialogue S oracle (BNtoDialogue b')).
    now rewrite ihb.
  - now rewrite ihb. 
Qed.    


End BranchingNaturalNumbers.


Section BranchingNatStreams.

Variable (Y : Type).

(* Branching natural numbers with nat labelled inner nodes *)
Definition StreamBranchingNat := BranchingNat nat Y.

Definition stream_BNdialogue (d : StreamBranchingNat) (alpha : Stream Y) :=
  BNdialogue d (fun n =>  Str_nth n alpha).

Definition stream_BNeloquent (f : (Stream Y) -> nat) :=
  {d : StreamBranchingNat & forall alpha, f alpha = (stream_BNdialogue d) alpha}.

End BranchingNatStreams.


Section Continuity.
  
Variable (X Y : Type).
Implicit Type (A B : Type).

(* Definition EqFin (f : X -> Y) (l : list X) (g : X -> Y) := *)
(*   List.map f l = List.map g l. *)

(* Lemma Eqnil (alpha bêta : X -> Y) : EqFin alpha nil bêta. *)
(* Proof. by []. Qed. *)

(* Lemma Eqcons (alpha bêta : X -> Y) (l : list X) (x : X) : *)
(*   (alpha x = bêta x) -> (EqFin alpha l bêta) -> (EqFin alpha (x :: l) bêta). *)
(* Proof. by move=> ex ih; rewrite /EqFin /= ex ih. Qed. *)

(* Lemma EqFin_Cons (alpha : X -> Y) (l : list X) (bêta : X -> Y) (x : X) : *)
(*    (EqFin alpha (x :: l) bêta) -> (alpha x = bêta x) /\ (EqFin alpha l bêta). *)
(* Proof. by rewrite /EqFin /=; case=> ex el; split. Qed. *)

(* Lemma Dialogue_Continuity A : forall (d : Dialogue X Y A) (alpha : X -> Y), *)
(*     continuous (dialogue d) alpha. *)
(* Proof. *)
(*   intros d alpha. *)
(*   induction d as [ | f ihd x] ; simpl. *)
(*   - now exists nil. *)
(*   - destruct (ihd (alpha x)) as [l ihcontinuity]. *)
(*     exists (cons x l) ; move=> bêta /EqFin_cons [<- el]. *)
(*     exact: ihcontinuity. *)
(* Qed. *)


Inductive EqFin : (X -> Y) -> (list X) -> (X -> Y) -> Type :=
| Eqnil : forall (alpha bêta : X -> Y), EqFin alpha nil bêta
| Eqcons : forall (alpha bêta : X -> Y) (l : list X) (x : X),
    (alpha x = bêta x) -> (EqFin alpha l bêta) -> (EqFin alpha (x :: l) bêta).


Definition continuous A (f : (X -> Y) -> A) (alpha : X -> Y) :=
  {l : list X & forall bêta, EqFin alpha l bêta -> (f alpha = f bêta)}.


Lemma Dialogue_Continuity A : forall (d : Dialogue X Y A) (alpha : X -> Y),
    continuous (dialogue d) alpha.
Proof.
  intros d alpha.
  induction d as [ | f ihd x] ; simpl.
  - now exists nil.
  - destruct (ihd (alpha x)) as [l ihcontinuity].
    exists (cons x l) ; intros bêta Eqlist.
    inversion_clear Eqlist as [ | a b c d Eqhd Eqcons].
    rewrite - Eqhd.
    exact: ihcontinuity.
Defined.


Lemma BNDialogue_Continuity (b : BranchingNat X Y) (alpha : X -> Y) :
    continuous (BNdialogue b) alpha.
Proof.
  unshelve refine (let fix aux b := match  b as b1
                                           return
                                           {l : list X &
                                                forall bêta : X -> Y,
                                                  EqFin alpha l bêta ->
                                                  BNdialogue b1 alpha = BNdialogue b1 bêta}
                                    with
                                    | B0 _ _ => (existT _ nil (fun _ _ => eq_refl))
                                    | BS bn => existT _ (projT1 (aux bn)) _
                                    | Bêtanat g x => existT _ (cons x (projT1 (aux (g (alpha x))))) _
                                    end in aux b).
  - now intros bêta Eqlist ; simpl ; rewrite (projT2 (aux bn) bêta).
  - intros bêta Eqlist.
    inversion_clear Eqlist as [ | a q c d Eqhd Eqcons].
    simpl ; rewrite - Eqhd.
    exact (projT2 (aux (g (alpha x))) bêta Eqcons).
Defined.
Print BNDialogue_Continuity.

Lemma eloquent_continuous A (f : (X -> Y) -> A) (alpha : X -> Y) :
    eloquent f -> continuous f alpha.
Proof.
  intro Hyp ; destruct Hyp as [d Heqd].
  destruct (Dialogue_Continuity d alpha) as [l Eqlist].
  exists l ; intros bêta HeqFin.
  rewrite !Heqd.
  exact: Eqlist.
Qed.  

Lemma BNeloquent_continuous (f : (X -> Y) -> nat) (alpha : X -> Y) :
    BNeloquent f -> continuous f alpha.
Proof.
  intro Hyp ; destruct Hyp as [b Heqb].
  destruct (BNDialogue_Continuity b alpha) as [l Eqlist].
  exists l ; intros bêta HeqFin.
  rewrite !Heqb.
  exact: Eqlist.
Qed.  

End Continuity.



Section StreamContinuity.
  
Variable (X Y : Type).
Implicit Type (A B : Type).


Inductive StreamEqFin : (Stream Y) -> (list nat) -> (Stream Y) -> Type :=
| StrEqnil : forall (alpha bêta : Stream Y), StreamEqFin alpha nil bêta
| StrEqcons : forall (alpha bêta : Stream Y) (l : list nat) (n : nat),
    (Str_nth n alpha = Str_nth n bêta) -> (StreamEqFin alpha l bêta) ->
    (StreamEqFin alpha (n :: l) bêta).


Definition stream_continuous A (f : (Stream Y) -> A) (alpha : Stream Y) :=
  {l : list nat & forall bêta, StreamEqFin alpha l bêta -> (f alpha = f bêta)}.


(*The two following lemmas indicate that we could get read of the StreamEqFin definition*)

Lemma StreamEqFin_EqFin (l : list nat) (alpha bêta : Stream Y) :
    StreamEqFin alpha l bêta ->
    EqFin (fun n : nat => Str_nth n alpha) l
          (fun n : nat => Str_nth n bêta).
Proof.
  intro StrEqlist.
  induction l as [ | x q ihl].
  - exact: Eqnil.
  - inversion_clear StrEqlist as [ | a b c d Heqhd Heqcons ].
    apply Eqcons ; trivial.
    exact: ihl.
Qed.


Lemma EqFin_StreamEqFin (l : list nat) (alpha bêta : Stream Y) :
    EqFin (fun n : nat => Str_nth n alpha) l
          (fun n : nat => Str_nth n bêta) ->
    StreamEqFin alpha l bêta.
Proof.
  intro Eqlist.
  induction l as [ | x q ihl].
  - exact: StrEqnil.
  - inversion_clear Eqlist as [ | a b c d Heqhd Heqcons ].
    apply StrEqcons ; trivial.
    exact: ihl.
Qed.

    
Lemma StreamDialogue_Continuity A (d : StreamDialogue Y A) (alpha : Stream Y) :
    stream_continuous (stream_dialogue d) alpha.
Proof.
  destruct (Dialogue_Continuity d (fun n => Str_nth n alpha)) as [l Eqlist].
  exists l.
  intros bêta StrEqlist.
  apply (Eqlist (fun n => Str_nth n bêta)).
  exact: StreamEqFin_EqFin.
Qed.


Lemma StreamBNDialogue_Continuity (b : StreamBranchingNat Y) (alpha : Stream Y) :
    stream_continuous (stream_BNdialogue b) alpha.
Proof.
  destruct (BNDialogue_Continuity b (fun n => Str_nth n alpha)) as [l Eqlist].
  exists l.
  intros bêta StrEqlist.
  apply Eqlist.
  exact: StreamEqFin_EqFin.
Qed.


Lemma stream_eloquent_continuous A (f : (Stream Y) -> A) (alpha : Stream Y) :
    stream_eloquent f -> stream_continuous f alpha.
Proof.
  intro Hyp ; destruct Hyp as [d Heqd].
  destruct (StreamDialogue_Continuity d alpha) as [l Eqlist].
  exists l.
  intros bêta HeqFin.
  rewrite !Heqd.
  exact: Eqlist.
Qed.  


Lemma stream_BNeloquent_continuous A (f : (Stream Y) -> nat) (alpha : Stream Y) :
    stream_BNeloquent f -> stream_continuous f alpha.
Proof.
  intro Hyp ; destruct Hyp as [b Heqb].
  destruct (StreamBNDialogue_Continuity b alpha) as [l Eqlist].
  exists l.
  intros bêta HeqFin.
  rewrite !Heqb.
  exact: Eqlist bêta HeqFin.
Qed.  

End StreamContinuity.











(*Definition Ctx :=
  triple (fun (A : ACtx) (B : BCtx) =>
            forall (alpha : X -> Y),  A alpha -> B -> Type).

Definition Ctx_El (Gamma : Ctx) (alpha : X -> Y) :=
    triple (fun (a : Gamma.(q1) alpha) (b : Gamma.(q2)) =>
              Gamma.(q3) alpha a b).


Definition Ty (Gamma : Ctx) : Type :=
    triple (fun (A :  ATy Gamma.(q1)) (B : BTy Gamma.(q2)) =>
              forall (alpha : X -> Y) (gamma : Ctx_El Gamma alpha),
                A alpha (gamma.(q1)) -> BEl (B gamma.(q2)) -> Type).


Definition REl (Gamma : Ctx) (R : Ty Gamma) : Type :=
    triple (fun (a : AEl R.(q1)) (b : BEl' R.(q2)) =>
              forall (alpha : X -> Y) (gamma : Ctx_El Gamma alpha),
                R.(q3) alpha gamma (a alpha gamma.(q1)) (b gamma.(q2))).

Notation "[| A |]a" := (AEl A).
Notation "[| A |]b" := (BEl' A).
Notation "[| A |]r" := (REl A).

Definition Ty_inst (Gamma : Ctx) (R : Ty Gamma) (alpha : X -> Y) (gamma : Ctx_El Gamma alpha) :=
  triple (fun (a : R.(q1) alpha gamma.(q1)) (b : BEl (R.(q2) gamma.(q2))) =>
            R.(q3) alpha gamma a b).


Definition Inst (Gamma : Ctx) (R : Ty Gamma) (r : REl R)
           (alpha : X -> Y) (gamma : Ctx_El Gamma alpha) : Ty_inst R gamma.
Proof.
  exists (r.(q1) alpha gamma.(q1)) (r.(q2) gamma.(q2)).
  exact (r.(q3) alpha gamma).
Defined.  


Notation "r ® gamma" := (Inst r gamma) (at level 10, left associativity).


Definition Ctx_nil : Ctx.
Proof.
  exists (ACtx_nil) (BCtx_nil).
  apply (fun _ _ _ => unit).
Defined.



Definition Ctx_cons (Gamma : Ctx) (R : Ty Gamma) : Ctx.
Proof.
  destruct Gamma as [Ga Gb Ge] ; unfold Ctx ; simpl.
  exists (ACtx_cons R.(q1)) (BCtx_cons R.(q2)).
  intros alpha Acons Bcons.
  apply (@tsig (Ge alpha Acons.(fst) Bcons.(fst))).
  intro gammae.
  exact (R.(q3) alpha (exist3 gammae) Acons.(snd) Bcons.(snd)).
Defined.

Notation "Γ · A" := (@Ctx_cons Γ A) (at level 50, left associativity).


Definition ctx_cons (Gamma : Ctx) (R : Ty Gamma) (alpha : X -> Y)
           (gamma : Ctx_El Gamma alpha) (x : Ty_inst R gamma) :
  Ctx_El (Ctx_cons R) alpha.
Proof.
  unfold Ctx_El ; simpl.
  destruct x as [xa xb xe].
  exists (Actx_cons xa) (Bctx_cons xb).
  exists gamma.(q3).
  exact xe.
Defined.


Definition Ctx_tl (Gamma : Ctx) (R : Ty Gamma) (alpha : X -> Y)
           (gamma : Ctx_El (Gamma · R) alpha) : Ctx_El Gamma alpha.
Proof.
  exists gamma.(q1).(fst) gamma.(q2).(fst).
  exact (gamma.(q3).(fst)).
Defined.


Notation "◊ g" := (Ctx_tl g) (at level 10).

Definition Ctx_hd (Gamma : Ctx) (R : Ty Gamma) (alpha : X -> Y)
           (gamma : Ctx_El (Gamma · R) alpha) : Ty_inst R (◊ gamma).
Proof.
  exists gamma.(q1).(snd) gamma.(q2).(snd).
  exact gamma.(q3).(snd).
Defined.

Notation "¿ g" := (Ctx_hd g) (at level 10).


Definition Lift (Gamma : Ctx) (R1 R2 : Ty Gamma) : Ty (Gamma · R1).
Proof.
  exists (@Aweak _ R1.(q1) R2.(q1)) (@Bweak _ R1.(q2) R2.(q2)).
  exact (fun alpha gamma ya yb => R2.(q3) alpha (◊ gamma) ya yb).
Defined.

Notation "⇑ A" := (@Lift _ _ A) (at level 10).

Definition Var (Gamma : Ctx) (R : Ty Gamma) : @REl (Gamma · R) (⇑ R).
Proof.
  exists (@AweakEl _ R.(q1)) (@BweakEl _ R.(q2)).
  exact (fun alpha gamma => gamma.(q3).(snd)). 
Defined.

Notation "#" := (@Var _ _) (at level 0).

Definition Weaken (Gamma : Ctx) (R S : Ty Gamma) (r : REl R) :
  @REl (Gamma · S) (⇑ R).
Proof.
  exists (Aweakterm r.(q1)) (Bweakterm r.(q2)).
  exact (fun alpha gamma => r.(q3) alpha (◊ gamma)).
Defined.

Notation "↑ M" := (Weaken M) (at level 10).

Definition Sub (Gamma : Ctx) (R : Ty Gamma) (S : Ty (Ctx_cons R)) (r : REl R) :
  Ty Gamma.
Proof.
  exists (ASub S.(q1) r.(q1)) (BSub S.(q2) r.(q2)). 
  destruct S as [Sa Sb Se] ; simpl.
  exact (fun alpha gamma =>
           Se alpha (ctx_cons (r ® gamma))).
Defined.

Notation "S {{ r }} " := (@Sub _ _ S r) (at level 20, left associativity).


(*Definition ctx_cons (Gamma : Ctx) (A : Ty Gamma) (alpha : X -> Y)
           (gamma : Ctx_El Gamma alpha) (a : REl A) :
  Ctx_El (Ctx_cons A) alpha.
Proof.
  unfold Ctx_El ; simpl.
  apply (@exist3 (ACtx_cons (q1 A) alpha) (BCtx_cons (q2 A))
                            (fun a b => @tsig (q3 Gamma alpha (fst a) (fst b))
                                              (fun gammae =>
                                                 q3 A alpha
                                                    {| q1 := fst a; q2 := fst b; q3 := gammae |}
                                                    (snd a) (snd b)))
                            ({| fst := q1 gamma; snd := q1 a alpha (q1 gamma) |})
                            ({| fst := q2 gamma; snd := q2 a (q2 gamma) |})
                            (@exist (Gamma.(q3) alpha (q1 gamma) (q2 gamma))
                                    (fun gammae =>
                                       q3 A alpha
                                          {| q1 := q1 gamma;
                                             q2 := q2 gamma;
                                             q3 := gammae |}
                                          (q1 a alpha (q1 gamma))
                                          (q2 a (q2 gamma)))
                                    gamma.(q3)
                                            (a.(q3) alpha gamma))).
Defined.*)

Definition TY (Gamma : Ctx) : Ty Gamma.
Proof.
  exists (@AType Gamma.(q1)) (@BType Gamma.(q2)).
  simpl ; intros alpha gamma A B.
  exact (A -> BEl B -> Type).
Defined.



         
Definition RPi (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A)) : Ty Gamma.
Proof.
  exists (APi B.(q1)) (BPi B.(q2)).
  intros alpha gamma PiA PiB.
  exact (forall a : Ty_inst A gamma,
            B.(q3) alpha (ctx_cons a)
                   (PiA a.(q1))
                   (PiB a.(q2) )).
Defined.


Notation "∏" := (@RPi).

Notation "A → B" := (@RPi _ A (⇑ B)) (at level 99, right associativity, B at level 200).

Definition RLam (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A)) (f : REl B)
  : REl (RPi B).
Proof.
  exists (ALam f.(q1)) (BLam f.(q2)).
  intros alpha gamma x.
  exact: f.(q3).
Defined.

Notation "'λ'" := RLam.


Definition RApp (Gamma : Ctx) (A : Ty Gamma)
           (B : Ty (Ctx_cons A)) (f : REl (RPi B)) (x : REl A) : REl (B {{ x }}).
Proof.
  exists (AApp2 f.(q1) x.(q1)) (BApp2 f.(q2) x.(q2)).
  exact (fun alpha gamma =>
           f.(q3) alpha gamma (Inst x  gamma)).
Defined.

Notation "t • u" := (@RApp _ _ _ t u) (at level 11, left associativity).


Definition REL (Gamma : Ctx) (A : [| TY Gamma |]r) : Ty Gamma.
Proof.
  unfold Ty ; simpl.
  exists (fun p γ => A.(q1) p γ) (fun gamma => A.(q2) gamma).
  exact (A.(q3)).
Defined.


Notation "[ A ]" := (REL A).

  
Definition RevApp (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A))
           (x : REl A) :
  @REl (Gamma · (∏ _ _ B)) (⇑  (B {{ x }})).
Proof.
  exists (ARevApp _) (BRevApp _) ; simpl.
  refine (fun alpha gamma => (¿ gamma).(q3) (x ® (◊ gamma))).
Defined.

Notation " B $ x " := (@RevApp _ _ B x) (at level 11).


Inductive RParabool (Gamma : Ctx) :
  forall (alpha : X -> Y) (g : Ctx_El Gamma alpha),
    (@Abool Gamma.(q1) alpha g.(q1)) -> (BEl (@Bbool' Gamma.(q2) g.(q2))) -> Type :=
| RParatrue : forall (alpha : X -> Y) (g : Ctx_El Gamma alpha),
    @RParabool _ _ g true (@Btrue X Y)
| RParafalse : forall (alpha : X -> Y) (g : Ctx_El Gamma alpha),
    @RParabool _ _ g false (@Bfalse X Y).


Definition Rbool (Gamma : Ctx) : Ty Gamma.
Proof.
  exists (@Abool Gamma.(q1)) (@Bbool' Gamma.(q2)).
  now apply RParabool.
Defined.

Definition Rtrue (Gamma : Ctx) : REl (@Rbool Gamma) :=
  {|
  q1 := @Atrue _ ;
  q2 := @Btrue' _ ;
  q3 := @RParatrue _ |}.

Definition Rfalse (Gamma : Ctx) : REl (@Rbool Gamma) :=
  {|
  q1 := @Afalse _ ;
  q2 := @Bfalse' _ ;
  q3 := @RParafalse _ |}.


Definition Rbool_stor (Gamma : Ctx) :
  [|∏ _ (∏ _ (Rbool Gamma) (TY _) ) (∏ _ (Rbool _) (TY _)) |]r.
Proof.
  exists (@Abool_stor Gamma.(q1)) (@Bbool_stor Gamma.(q2)).
  intros alpha gamma P b stora storb.
  induction b.(q3).
  - exact (P.(q3) (@Rtrue Gamma ® gamma) stora storb).
  - exact (P.(q3) (@Rfalse Gamma ® gamma) stora storb).
Defined.


Definition Rbool_rec (Gamma : Ctx) :
  [| ∏ _ (@TY Gamma)
       ((Var (TY _)) →
        (Var (TY _)) →
        (Rbool _) →
        (Var (TY _))) |]r.
Proof.
  exists (@Abool_rec _) (@Bbool_rec _).
  unfold Ty_inst ; simpl.
  intros alpha g P ptrue pfalse b.
  induction b.(q3).
  - exact ptrue.(q3).
  - exact pfalse.(q3).
Defined.



Definition Ty (Gamma : Ctx) := forall alpha : X -> Y, (Gamma alpha) -> Type.
Definition AType (Gamma : Ctx) : Ty Gamma :=
  fun alpha gamma => Type.

Definition AEl (Gamma : Ctx) (A : Ty Gamma) :=
  forall (alpha : X -> Y) (gamma : Gamma alpha), A alpha gamma. 

Definition APi (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A)) : Ty Gamma.
Proof.
  intros alpha gamma. 
  exact (forall a : A alpha gamma, B alpha (exist a)).
Defined.

Definition ALam (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A)) (f : AEl B)
  : AEl (APi B) := 
  fun (alpha : X -> Y) (gamma : Gamma alpha) (a : A alpha gamma) => f alpha (exist a).

Definition AApp (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A)) (f : AEl (APi  B))
  : AEl B :=
  fun (alpha : X -> Y) (gamma : Ctx_cons A alpha) => f alpha gamma.(fst) gamma.(snd).


Lemma AAppLam (Gamma : Ctx) (A : Ty Gamma) (B : Ty (Ctx_cons A)) (f : AEl B)
      (alpha : X -> Y) :
  (fun gamma => AApp (ALam f) gamma) = (fun gamma => f alpha gamma). 
Proof. reflexivity. Qed.


Definition BTYPE (Gamma : Ctx) : Ty Gamma :=
  fun (alpha : X -> Y) (gamma : Gamma alpha) => BranchingTYPE X Y.*)