https://gitlab.inria.fr/mbaillon/gardening-with-the-pythia
Raw File
Tip revision: 1c783fb2a09f78c7d1bd2f27008221724fe204d0 authored by Martin Baillon on 08 July 2021, 22:02:58 UTC
comments
Tip revision: 1c783fb
Translation.v
Set Primitive Projections.
Set Universe Polymorphism.
Require Import Dialogue.
Require Import Base.

Section AxiomTranslation.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Variables (X Y : Type).
Implicit Type (A B : Type).
(*In this section we present the Axiom translation,
which adds an oracle α : X -> Y in the context.
We use a Cwf-like presentation *)

(*In the axiom translation, the empty context is
translated as α : X -> Y. As such, there is no empty
context in the image of the translation, and all contexts
depend on α.*)
Definition ACtx := (X -> Y) -> Type.

(*A type is a function from contexts to Type*)
Definition ATy (Gamma : ACtx) : Type :=
  forall α : X -> Y, Gamma α -> Type.

(*Type is translated as the constant function
that always returns Type*)
Definition AType {Gamma : ACtx} : ATy Gamma :=
  fun α gamma => Type.

(*AEl is the axiom version of Tarsky's El function*)
Definition AEl (Gamma : ACtx) (A : ATy Gamma) :
  Type :=
  forall (α : X -> Y) (gamma : Gamma α), A α gamma. 

(*Empty context*)
Definition ACtx_nil : ACtx := fun α => unit.

Notation "()" := (ACtx_nil).

(*Context extension*)
Definition ACtx_cons (Gamma : ACtx) (A : ATy Gamma) :
  ACtx:=
  fun (α : X -> Y) => tsig (fun (gamma : Gamma α) => A α gamma).

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

Definition Actx_cons (Gamma : ACtx) (A : ATy Gamma) (α : X -> Y)
           (gamma : Gamma α) (a : A α gamma) : (ACtx_cons A) α.
Proof.
  exists gamma ; exact a.
Defined.

Notation "γ ·· x" := (@Actx_cons γ x) (at level 50, left associativity).

(*In what follows, we deal with the negative fragment
of type theory : Weakening, Pi-types, Substitution, etc*)


(*Lifting rule*)
Definition ALift
           (Gamma : ACtx) (A : ATy Gamma) (B : ATy Gamma) :
  ATy (ACtx_cons A) :=
  fun α gamma => B α gamma.(fst).

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

(*Weakening rule*)
Definition AWeaken {Γ : ACtx} {R S : ATy Γ} (r : AEl R) :
  @AEl (ACtx_cons S) (@ALift _ S R).
Proof.
  + refine (fun α γr => r α γr.(fst)).
Defined.

Notation "↑ M" := (@AWeaken _ _ _ M) (at level 10).

(*Variable rule*)
Definition AVar (Gamma : ACtx)
           (A : ATy Gamma) :
  AEl  (@ALift Gamma A A) :=
  fun (α : X -> Y) (gamma : ACtx_cons A α) => gamma.(snd).

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

(*Substitution*)
Definition ASub (Gamma : ACtx) (A : ATy Gamma)
           (B : ATy (ACtx_cons A)) (a : AEl A) : ATy Gamma :=
  fun α gamma => B α (exist (a α gamma)).

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

(*Pi-type*)
Definition APi (Gamma : ACtx) (A : ATy Gamma)
           (B : ATy (ACtx_cons A)) : ATy Gamma :=
  fun α gamma =>
    forall a : A α gamma, B α (exist a).

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

(*Introduction for Pi*)
Definition ALam (Gamma : ACtx) (A : ATy Gamma)
           (B : ATy (ACtx_cons A))(f : AEl B)
  : AEl (APi B) := 
  fun (α : X -> Y) (gamma : Gamma α) (a : A α gamma) => f α (exist a).

Notation "'λ'" := (@ALam).

(*Introduction of the non-dependent arrow*)
Definition ALamN {Γ : ACtx } {A : ATy Γ} {B : ATy Γ}
           (f : @AEl (Γ · A) (⇑ B)) : @AEl Γ (A → B) :=
  @ALam Γ A (⇑ B) f.

(*Elimination for Pi*)
Definition AApp {Γ : ACtx}
           {A : ATy Γ} {B : ATy (@ACtx_cons Γ A)}
           (f : @AEl Γ (APi B)) (x : @AEl Γ A) : @AEl Γ (ASub B x) :=
  fun α γr => f α γr (x α γr).

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


(*Elimination of the non-dependent arrow*)
Definition AAppN {Γ : ACtx } {A : ATy Γ} {B : ATy Γ}
           (f : @AEl Γ (A → B))(x : @AEl Γ A) : @AEl Γ B :=
  @AApp Γ A (⇑ B) f x.


Notation "t ◊ u" := (@AAppN _ _ _ t u) (at level 12, left associativity).



(*It is now time to define the translation
of various inductive types*)


(*The translation of booleans*)
Definition Abool {Gamma : ACtx} : ATy Gamma := fun α gamma => bool. 

Definition Atrue (Gamma : ACtx) : AEl (@Abool Gamma) :=
  fun α gamma => true.

Definition Afalse (Gamma : ACtx) : AEl (@Abool Gamma) :=
  fun α gamma => false.

(* The Axiom translation builds a model of full-CIC as soon as X->Y
is not empty, but the global translation will be a model of BTT.
Thus, we only define the Axiom translation for BTT*)


(*Non-dependent eliminator for booleans*)
Definition Abool_rec (Γ : ACtx) :
  @AEl Γ (∏ Γ AType ((@AVar _ AType) → (@AVar _ AType) → Abool → (@AVar _ AType))) :=
  fun α ga P ptrue pfalse b => match b with
          | true => ptrue
          | false => pfalse
         end.

(*Storage operator for booleans, in direct style*)
Definition Abool_stor {Γ : ACtx} :
  AEl (Abool → (Abool → AType) → AType) :=
  fun α ga b P => @Abool_rec Γ α ga ((bool -> Type) -> Type)
                             (fun k => k true)
                             (fun k => k false)
                             b P.


(*Restricted dependent-eliminator for booleans.*)
Definition Abool_rect (Γ : ACtx) :
  AEl (∏ Γ (Abool → AType)
            ((@AApp _ Abool AType # (@Atrue _)) →
                  ((@AApp _ Abool AType # (@Afalse _)) →
                   (∏ _ Abool (Abool_stor • # • (↑#)))))) :=
  fun α gamma P ptrue pfalse b =>
    match b with
    | true => ptrue
    | false => pfalse
    end.


(*The translation of natural numbers*)
Definition Anat {Γ : ACtx} : ATy Γ := fun α gamma => nat.

Definition A0 {Γ : ACtx} : AEl (@Anat Γ) := fun α gamma => 0.

Definition ASucc {Γ : ACtx} :
  AEl (∏ Γ (@Anat Γ) (@Anat (ACtx_cons (@Anat Γ)))) :=
    fun _ _ n => S n.


(*Non-dependent eliminator for natural numbers*)
Definition Anat_rec (Γ : ACtx) :
  @AEl Γ (∏ Γ AType
            (@AVar _ AType →
             (Anat → (@AVar _ AType) → (@AVar _ AType)) →
             Anat →
             (@AVar _ AType))).
Proof.
  refine (fun α gamma P p0 pS => _).
  refine (fix f n := match n with
                       | 0 => p0
                       | S k => pS k (f k)
                       end).
Defined.


(*Storage operator for natural numbers. In direct style it amounts to :
Definition Nat_stor (n : nat) (P : nat -> Type) : Type :=
  @Nat_rec ((nat -> Type) -> Type)
            (fun P => P 0)
            (fun n P k => k (S n))
             n P.*)
Definition Anat_stor{Γ : ACtx } :
  @AEl Γ (Anat → (Anat → AType) → AType).
Proof.
  pose (r := @AApp _ _ _ (@Anat_rec Γ) ((Anat → AType) → AType)).
  let T := constr:(@AEl Γ (((Anat → AType) → AType) → (Anat → ((Anat → AType) → AType) → ((Anat → AType) → AType)) → Anat → ((Anat → AType) → AType))) in
  unshelve refine (let r : T := r in _).
  unshelve refine (AApp (AApp r _) _).
  - refine (ALamN (@AAppN _ Anat _ _ _)).
    + now refine (@AVar _ _).
    + now refine (@A0 _).
  - refine (@ALamN _ _ _ _).
    refine (@ALamN (@ACtx_cons Γ Anat) (⇑ ((Anat → AType) → AType)) (⇑ ((Anat → AType) → AType)) _).
    refine (@ALamN (Γ · Anat · (⇑ ((Anat → AType) → AType)))
                   (⇑(⇑(Anat → AType))) (⇑ (⇑ AType)) _).
    refine (@AAppN _ Anat _ _ _).
    + now refine #.
    + now refine (@AAppN _ Anat _ (@ASucc _) (↑↑#)).
Defined.



(*Restricted dependent-eliminator for natural numbers.*)
Definition Anat_rect {Γ : ACtx} :
  @AEl Γ (∏ _ (Anat → AType)
              ((@AApp _ _ AType # A0) →
              (∏ _ Anat ((Anat_stor • # • (↑#)) →
                       (Anat_stor • (ASucc • #) • (↑#)))) →
              ∏ _ Anat (Anat_stor • # • (↑#)))).
Proof.
  unshelve refine (fun α γ P p0 pS => _).
  refine (fix g n := match n as n0 return
                                       (fix f (n : nat) : (nat -> Type) -> Type :=
                                          match n with
                                          | 0 => fun a0 : nat -> Type => a0 0
                                          | S k => fun a0 : nat -> Type => a0 (S k)
                                          end) n0 P
                                 with
                                 | 0 => p0
                                 | S k => pS k (g k)
                                 end).
Defined.

(*Our definitions "computes", that is : Anat_rect P p0 pS 0 reduces to p0
and Anat_rect P p0 pS (S k) reduces to pS k (Anat_rect P p0 pS k) *)
Goal forall (Γ : ACtx)
  (P : @AEl Γ (Anat → AType))
  (T0 := (P • (@A0 _)))
  (p0 : @AEl Γ T0)

  (TS := (∏ _ Anat ((@AApp (Γ · Anat) _ AType
                              (@AApp (Γ · Anat) _ _ Anat_stor #) (↑P)) →
                       (@AApp (Γ · Anat) _ AType
                              (@AApp (Γ · Anat) _ _ Anat_stor
                                     (@AApp (Γ · Anat) _ _ (@ASucc _) #)) (↑P)))))

  
  (pS : @AEl Γ TS)
  (TR := ∏ Γ Anat (Anat_stor • @AVar _ Anat • ↑ P))
  ,

  @AApp Γ _ _ (@AAppN Γ _ _ (@AAppN Γ T0 (TS → TR) ((@Anat_rect Γ) • P) p0) pS) (@A0 _)
  =
  p0.
Proof. reflexivity. Qed.

Goal forall (Γ : ACtx)
  (P : @AEl Γ (Anat → AType))
  (T0 := (P • (@A0 _)))
  (p0 : @AEl Γ T0)
  (TS := (∏ _ Anat ((@AApp (Γ · Anat) _ AType
                         (@AApp (Γ · Anat) _ _ Anat_stor #) (↑P)) →
                  (@AApp (Γ · Anat) _ AType
                         (@AApp (Γ · Anat) _ _ Anat_stor
                                (@AApp (Γ · Anat) _ _ (@ASucc _) #)) (↑P)))))
  (pS : @AEl Γ TS)
  (TR := ∏ Γ Anat (Anat_stor • @AVar _ Anat • ↑ P))
  (n : @AEl Γ Anat)
  ,
    forall (α : X -> Y) (γr : Γ α),
    
    (@AApp Γ _ _ (@AAppN Γ _ _ (@AAppN Γ T0 (TS → TR) ((@Anat_rect Γ) • P) p0) pS) (AApp (@ASucc _) n)) α γr
    =
    (@AAppN Γ (@AApp Γ (Anat → AType) _ (@AApp Γ _ _ Anat_stor n) P) (Anat_stor • ((@ASucc _) • n) • P) (AApp pS n) (@AApp Γ _ _ (@AAppN Γ _ _ (@AAppN Γ T0 (TS → TR) ((@Anat_rect Γ) • P) p0) pS) n)) α γr.
Proof. reflexivity. Qed.


(*Translation of equality*)
Inductive Eq {A : Type} (x : A) : A -> Type :=  Eq_refl : Eq x x.

Definition Aeq {Γ : ACtx} : AEl (∏ Γ AType (# → # → AType)) :=
  fun _ _ => @Eq.

Definition Arefl {Γ : ACtx} :
  AEl (∏ Γ AType
         (∏ _ #
            (Aeq • (↑#) ◊ # ◊ #))) :=
  fun _ _ => @Eq_refl.

(*Non-dependent eliminator for equality*)

Definition Aeq_rec (Γ : ACtx) :
  @AEl Γ (∏ Γ AType
            (∏ _ #
               (∏ (Γ · AType · (@AVar _ AType))
                  ((↑#) → AType)
                  (((@AVar (Γ · AType · (@AVar _ AType))
                          ((↑(@AVar _ AType)) → AType)) ◊ ↑#) →
                (∏ (Γ · AType · (@AVar _ AType) · ((↑#) → AType))
                   (↑↑#)
                   ((((Aeq • (↑↑↑(@AVar _ AType))) ◊ ↑↑#) ◊ #) →
                 ((↑(@AVar (Γ · AType · (@AVar _ AType))
                           ((↑(@AVar _ AType)) → AType))) ◊ #))))))) :=
  fun α γ A x P px y e =>
    match e as e0 in (Eq _ y0) return (P y0) with
    | Eq_refl _ => px
    end.

(*Storage operator for equality, in direct style*)
  
Definition Aeq_stor {Γ : ACtx} :
  @AEl Γ (∏ Γ AType
            (∏ _ #
               (∏ _ (↑#)
                  ((((Aeq • (↑↑(@AVar _ AType))) ◊ ↑#) ◊ #) →
                   (∏ _ (↑↑#)
                      ((((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #) →
                       AType)) →
                   AType)))) :=
  fun α γ A x y e P =>
    @Aeq_rec Γ α γ A x (fun z => ((Eq x z -> Type) -> Type))
             (fun k => k (Eq_refl x)) y e (P y).


(*Restricted dependent-eliminator for equality.
Unfortunately, due to unification problems, Coq
crashes before it can even compute the type of
Aeq_rect.
That is why we leave this in comment mode.



Definition Aeq_rect (Γ : ACtx) :
  @AEl Γ (∏ Γ AType
            (∏ _ #
               (∏ _ (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) →
                           AType))
                  (((@AApp (Γ · AType · (@AVar _ AType) · (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType)))
                           (↑↑#) ((((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #) → AType) # (↑#)) ◊
                                                                                                (@AApp (Γ · AType · (@AVar _ AType) · (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType))) (↑ (↑ #)) (Aeq • ↑ (↑ (↑ #)) ◊ # ◊ #) (Arefl • (↑↑#)) (↑#))) →
                   ∏ (Γ · AType · (@AVar _ AType) · (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType)))
                     (↑↑#)
                     (∏ _ (((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #)
                        ((@AApp _ (↑↑↑↑(@AVar _ AType)) _
                                (@AApp (Γ · AType · (@AVar _ AType) ·
                                          (∏ _ (↑#) ((((@AApp _ AType ((# → # → AType)) Aeq (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType)) ·
                                          (↑↑#) ·
                                          (((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #))
                                       (↑↑↑↑(@AVar _ AType)) _
                                       (@AApp _ AType _
                                              Aeq_stor (↑↑↑↑(@AVar _ AType)))
                                       (↑↑↑#))
                                (↑#))
                           ◊ # ◊ (↑↑#))))))).
 *)


(*Translation of lists*)

Inductive list (A : Type) : Type :=
  nil : list A | cons : A -> list A -> list A.
Arguments nil {A}.
Definition Alist {Γ : ACtx} : @AEl Γ (AType → AType) :=
  fun α gamma a => list a.

Definition Anil {Γ : ACtx} :
  AEl (∏ Γ AType (Alist • (@AVar _ AType))) := fun α ga A => @nil A.


Definition Acons {Γ : ACtx} :
  AEl (∏ Γ AType
         ((@AVar _ AType) → (Alist • (@AVar _ AType)) → (Alist • (@AVar _ AType)))) :=
  fun α gamma A a la => cons a la.


(*Non-dependent eliminator for lists*)
Definition Alist_rec (Γ : ACtx) :
  @AEl Γ (∏ Γ AType
            (∏ _ AType
               (# →
                (↑ # → Alist • ↑ # → # → #) →
                Alist • ↑ # →
                #))).
Proof.
  unshelve refine (fun alpha gamma A P pnil pcons => _). 
  refine (fix f l {struct l} := match l with
                     | nil => pnil
                     | cons x q => pcons x q (f q)
                     end).
Defined.

(*Storage operator for lists, in direct style*)
Definition Alist_stor{Γ : ACtx } :
  AEl (∏ Γ AType (Alist • # → (Alist • # → AType) → AType)) :=
  fun (α : X -> Y) (_ : Γ α) (A : Type) =>
       fix f (l : list A) : (list A -> Type) -> Type :=
         match l with
         | nil => fun a0 : list A -> Type => a0 nil
         | cons x q =>
             fun P : list A -> Type =>
             f q (fun q' : list A => P (cons x q'))
         end.


(*Restricted dependent-eliminator for lists.
Unification problems also appear here, albeit less
serious ones, which is why our definition type-checks,
in a couple of minutes time.*)
Definition Alist_rect {Γ : ACtx} :
  @AEl Γ (∏ Γ AType
            (∏ _ ((Alist • (@AVar _ AType)) → AType)
               ((@AAppN _ _ AType # (Anil • (↑(@AVar _ AType)))) →
                 (∏ _ (↑(@AVar _ AType))
                    (∏ (Γ · AType · ((Alist • (@AVar _ AType)) → AType) · (↑(@AVar _ AType)))
                       (Alist • (↑↑(@AVar _ AType)))
                       ((((Alist_stor • (↑↑↑(@AVar _ AType)))
                            ◊ (@AVar _ ((Alist • (↑↑(@AVar _ AType)))))
                            ◊ (↑↑(@AVar _ ((Alist • (@AVar _ AType)) → AType))))) →
                        (((Alist_stor • (↑↑↑(@AVar _ AType)))
                            ◊ ((Acons • (↑↑↑(@AVar _ AType))) ◊ (↑#) ◊ #)
                            ◊ (↑↑(@AVar _ ((Alist • (@AVar _ AType)) → AType)))))))) →
                ∏ (Γ · AType · ((Alist • (@AVar _ AType)) → AType)) (Alist • ↑#)
                  ((Alist_stor • (↑↑(@AVar _ AType))) ◊ # ◊ (↑#))))) :=
  fun alpha gamma A P pnil pcons =>
    fix f l := match l as l0 return
                     (fix g (l : list A) : (list A -> Type) -> Type :=
                        match l with
                        | nil => fun a0 : list A -> Type => a0 nil
                        | cons x q =>
                          fun P : list A -> Type =>
                            g q (fun q' : list A => P (cons x q'))
                        end) l0 P
               with
               | nil => pnil
               | cons x q => pcons x q (f q)
               end.


End AxiomTranslation.


Section BranchingTranslation.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Variables (X Y : Type).


(*In this section we present the Branching translation,
which interprets all types as algebras of the Dialogue monad.
Again, we use a Cwf-like presentation *)

(*Let us first formalize what is an algebra of the Dialogue monad.*)
Definition BranchingTYPE := {A : Type & (Y -> A) -> X -> A}.

(*In the Branching translation, contexts are translated pointwise.
As such, they are simply types.*)
Definition BCtx := Type.

(*A type is a function from contexts to BranchingType*)
Definition BTy (Gamma : BCtx) := Gamma -> BranchingTYPE.

(*Type is translated as the constant function that always return
BranchingTYPE. The proof of algebraicity is a dummy function.*)
Definition Bunit : BranchingTYPE :=
  @exist Type (fun A =>  (Y -> A) -> X -> A) unit (fun _ _ => tt).

Definition BType {Gamma : BCtx} : BTy Gamma :=
  fun _ => @exist Type (fun A =>  (Y -> A) -> X -> A)
                  BranchingTYPE (fun _ _ => Bunit).


(*BEl is the branching version of Tarsky's El function*)
Definition BEl {Gamma : BCtx} (A : BTy Gamma) : Type :=
  forall (gamma : Gamma), (A gamma).(fst). 

(*Empty context*)
Definition BCtx_nil : BCtx := unit.

Notation "()" := (BCtx_nil).

(*Context extension*)
Definition BCtx_cons (Gamma : BCtx) (A : BTy Gamma) :=
  tsig (fun (gamma : Gamma) => (A gamma).(fst)).

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


Definition Bctx_cons (Gamma : BCtx) (B : BTy Gamma)
           (gamma : Gamma) (b : (B gamma).(fst)) : Gamma · B.
Proof.
  exists gamma ; exact b.
Defined.

Notation "γ ·· x" := (@Actx_cons γ x) (at level 50, left associativity).


(*In what follows, we deal with the negative fragment
of type theory : Weakening, Pi-types, Substitution, etc*)

(*Lifting rule*)
Definition BLift {Gamma : BCtx} {A : BTy Gamma} (B : BTy Gamma) : BTy (Gamma · A) :=
  fun gamma => B gamma.(fst).

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

(*Weakening rule*)
Definition BWeaken {Γ : BCtx} {R S : BTy Γ} (r : BEl R) :
  @BEl (Γ · S) (⇑ R).
Proof.
  + refine (fun γr => r γr.(fst)).
Defined.

Notation "↑ M" := (@BWeaken _ _ _ M) (at level 10).

(*Variable rule*)
Definition BVar {Gamma : BCtx}
           (A : BTy Gamma) :
  BEl (@BLift Gamma A A) :=
  fun (gamma : (Gamma · A)) => gamma.(snd).

Notation "#" := (@BVar _ _) (at level 0).
 
(*Substitution*)
Definition BSub {Gamma : BCtx} (A : BTy Gamma) (B : BTy (Gamma · A)) (a : BEl A) : BTy Gamma :=
  fun gamma => B ({|fst := gamma ; snd := a gamma |}).

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


(*Pi-type*)
Definition BPi {Gamma : BCtx} {A : BTy Gamma} (B : BTy (Gamma · A)) : BTy Gamma.
Proof.
  unshelve refine (fun gamma => exist _). 
  - exact (forall a : (A gamma).(fst),
             (B {| fst := gamma; snd := a|}).(fst)).
  - exact (fun f x a => (B {| fst := gamma; snd := a |}).(snd) (fun y => f y a) x).
Defined.

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

(*Introduction for Pi*)
Definition BLam {Gamma : BCtx} (A : BTy Gamma) (B : BTy (Gamma · A)) (f : BEl B)
  : BEl (BPi B) := 
  fun (gamma : Gamma) (a : (A gamma).(fst)) => f {| fst := gamma; snd := a |}.

Notation "'λ'" := (@ALam).

(*Introduction of the non-dependent arrow*)
Definition BLamN {Γ : BCtx } {A : BTy Γ} {B : BTy Γ}
           (f : @BEl (Γ · A) (⇑ B)) : @BEl Γ (A → B) :=
  @BLam Γ A (⇑ B) f.

(*Elimination for Pi*)

Definition BApp {Γ : BCtx} {A : BTy Γ} {B : BTy (Γ · A)}
           (f : BEl (∏ Γ A B)) (x : BEl A) : @BEl _ (B {{ x }}) :=
  fun gamma => f gamma (x gamma).

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

(*Elimination of the non-dependent arrow*)
Definition BAppN {Γ : BCtx } {A : BTy Γ} {B : BTy Γ}
           (f : @BEl Γ (A → B)) (x : @BEl Γ A) : @BEl Γ B :=
  @BApp Γ A (⇑ B) f x.


Notation "t ◊ u" := (@BAppN _ _ _ t u) (at level 12, left associativity).

(*Internal Tarsky's El function*)
Definition BEL {Γ : BCtx } (A : @BEl Γ BType) : BTy Γ := A.

Notation "[ A ]" := (@BEL _ A).


(*It is now time to define the translation
of various inductive types*)


(*The translation of booleans*)
Inductive BranchingBool :=
| Btrue_aux : BranchingBool
| Bfalse_aux : BranchingBool
| Bêtabool : (Y -> BranchingBool) -> X -> BranchingBool.


Definition Bbool {Gamma : BCtx} : BTy Gamma :=
  fun gamma => {| fst := BranchingBool; snd := Bêtabool |}.

Definition Btrue {Gamma : BCtx} : BEl (@Bbool Gamma) := (fun _ => Btrue_aux).

Definition Bfalse {Gamma : BCtx} : BEl (@Bbool Gamma) := (fun _ => Bfalse_aux ).


(*Non-dependent eliminator for booleans*)
Definition Bbool_rec {Γ : BCtx} :
  @BEl Γ (∏ Γ BType ((@BVar _ BType) → (@BVar _ BType) → Bbool → (@BVar _ BType))).
Proof.
  unshelve refine (fun ga P ptrue pfalse => _).
  now refine (fix f b := match b with
                         | Btrue_aux  => ptrue
                         | Bfalse_aux  => pfalse
                         | Bêtabool g x => P.(snd) (fun y => f (g y)) x
                         end).
Defined.

(*Storage operator for booleans*)
Definition Bbool_stor {Gamma : BCtx} :
  @BEl Gamma (Bbool → (Bbool → BType) → BType).
Proof.
  exact (fun ga b P => @Bbool_rec Gamma ga
                                  (@BPi Gamma (@BPi Gamma (@Bbool Gamma) (@BType _))
                                        (@BType _) ga)
                                  (fun k => k Btrue_aux)
                                  (fun k => k Bfalse_aux) b P).
Defined.

(*Restricted dependent-eliminator for booleans.*)
Definition Bbool_rect (Γ : BCtx) :
  @BEl Γ (∏ _ (Bbool → BType) (
    (@BApp (Γ · (Bbool → BType)) Bbool BType # Btrue) →
    (@BApp (Γ · (Bbool → BType)) Bbool BType # Bfalse) →
    ∏ _ Bbool (@BApp _  _ BType
                      (@BApp (Γ · (Bbool → BType) · Bbool) _ _ Bbool_stor #) (↑#)))) :=
  fun ga P ptrue pfalse b =>
    match b with
    | Btrue_aux => ptrue
    | Bfalse_aux => pfalse
    | Bêtabool g x => tt
    end.



(*The translation of natural numbers*)

Definition Bnat {Gamma : BCtx} : BTy Gamma :=
  fun gamma => {| fst := BranchingNat X Y ; snd := @Bêtanat X Y |}.

Definition Bzero {Gamma : BCtx} : BEl (@Bnat Gamma) := fun gamma => @B0 X Y. 

Definition BSucc {Gamma : BCtx} :
  @BEl Gamma (Bnat → Bnat) :=
  fun gamma => (@BS X Y).

(*Non-dependent eliminator for natural numbers*)
Definition Bnat_rec (Γ : BCtx) :
  BEl (∏ Γ BType ([#] →
                  (Bnat → [#] → [#]) →
                  Bnat →
                  [#])).
Proof.
  - unshelve refine (fun gamma P p0 pS => _).
    exact (fix f n := match n with
                       | B0 _ _ => p0
                       | BS k => pS k (f k)
                       | Bêtanat g x => P.(snd) (fun y => f (g y)) x
                       end).
Defined.


(*Storage operator for natural numbers*)
Definition Bnat_stor {Γ : BCtx} :
  @BEl Γ (Bnat → (Bnat → BType) → BType).
Proof.
  pose (r := BApp (@Bnat_rec Γ) ((Bnat → BType) → BType)).
  let T := constr:(@BEl Γ (((Bnat → BType) → BType) → (Bnat → ((Bnat → BType) → BType) → ((Bnat → BType) → BType)) → Bnat → ((Bnat → BType) → BType))) in
  unshelve refine (let r : T := r in _).
  unshelve refine (BAppN (BAppN r _) _).
  - refine (BLamN (@BAppN _ Bnat _ _ _)).
    + now refine #.
    + now refine Bzero.
  - refine (@BLamN _ _ _ _).
    refine (@BLamN _ (⇑ ((Bnat → BType) → BType)) (⇑ ((Bnat → BType) → BType)) _).
    refine (@BLamN _ (⇑(⇑(Bnat → BType))) (⇑ (⇑ BType)) _).
    refine (@BAppN _ Bnat _ _ _).
    + now refine #.
    + now refine (@BAppN _ Bnat _ BSucc (↑↑#)).
Defined.


(*Restricted dependent-eliminator for natural numbers*)
Definition Bnat_rect {Γ : BCtx} :
  BEl (∏ Γ (Bnat → BType) (
           (@BApp (Γ · (Bnat → BType)) Bnat BType # Bzero) →
           (∏ _ Bnat ((Bnat_stor • # • (↑#)) →
                       (Bnat_stor • (BSucc • #) • (↑#)))) →
              ∏ _ Bnat (Bnat_stor • # • (↑#)))).
Proof.
    unshelve refine (fun γ P p0 pS => _).
    exact (fix g n :=
              match n with
              | B0 _ _ => p0
              | BS k => pS k (g k)
              | Bêtanat _ _ => tt
              end).
Defined.


(*The translation of equality*)

Inductive BranchingEq (A : BranchingTYPE) (a : A.(fst)) : A.(fst) -> Type :=
| Beq_refl : BranchingEq a a
| Bêtaeq : forall (b : A.(fst)), (Y -> BranchingEq a b) -> X -> BranchingEq a b.
 
Definition Beq {Gamma : BCtx}: BEl (∏ Gamma BType ([#] → [#] → BType)).
Proof.
  unshelve refine (fun gamma A x y => exist _).
  - exact (@BranchingEq A x y).
  - exact (@Bêtaeq A x y).
Defined.

Definition Brefl {Γ : BCtx} :
  BEl (∏ Γ BType
         (∏ _ [#]
            [Beq • (↑#) ◊ # ◊ #])) :=
  fun _  => @Beq_refl.

(*Non-dependent eliminator for equality*)

Definition Beq_rec (Γ : BCtx) :
  @BEl Γ (∏ Γ BType
            (∏ _ [#]
               (∏ (Γ · BType · (@BVar _ BType))
                  ([↑#] → BType)
                  ([(@BVar (Γ · BType · (@BVar _ BType))
                          ((↑(@BVar _ BType)) → BType)) ◊ ↑#] →
                (∏ (Γ · BType · (@BVar _ BType) · ([↑#] → BType))
                   (↑↑#)
                   ([((Beq • (↑↑↑(@BVar _ BType))) ◊ ↑↑#) ◊ #] →
                 [(↑(@BVar (Γ · BType · (@BVar _ BType))
                           ((↑(@BVar _ BType)) → BType))) ◊ #])))))):=
  fun γ B x P px =>
    fix g y e :=
    match e as e0 in (BranchingEq _ y0) return (P y0).(fst) with
    | Beq_refl _ => px
    | @Bêtaeq _ _ b f x => (P b).(snd) (fun z => g b (f z)) x
    end.

(*Storage operator for equality, in direct style*)
  
Definition Beq_stor {Γ : BCtx} :
  @BEl Γ (∏ Γ BType
            (∏ _ [#]
               (∏ _ [↑#]
                  ([((Beq • (↑↑(@BVar _ BType))) ◊ ↑#) ◊ #] →
                   (∏ _ [↑↑#]
                      ([((Beq • (↑↑↑(@BVar _ BType))) ◊ (↑↑#)) ◊ #] →
                       BType)) →
                   BType)))) :=
  fun γ B x y e P =>
    match e in (BranchingEq _ b)
          return ((BranchingEq x b -> BranchingTYPE) -> BranchingTYPE)
    with
    | Beq_refl _ => fun k : BranchingEq x x -> BranchingTYPE => k (Beq_refl x)
    | @Bêtaeq _ _ _ _ _ => fun _ => Bunit
    end (P y).

(*As for the axiom translation, unification problems forbid us
from writing the restricted dependent eliminator*)


(*The translation of lists*)

Inductive BranchingList {A : BranchingTYPE} : Type :=
| Bnil_aux : BranchingList
| Bcons_aux : A.(fst)  -> BranchingList -> BranchingList
| Bêtalist : (Y -> BranchingList) -> X -> BranchingList.


Definition Blist {Gamma : BCtx} : @BEl Gamma (BType → BType) :=
  fun _ A => {| fst := @BranchingList A ; snd := @Bêtalist A |}.



Definition Bnil {Γ : BCtx} : BEl (∏ Γ BType (Blist • #)) :=
  fun _ B => @Bnil_aux B.


Definition Bcons {Γ : BCtx} :
  BEl (∏ Γ BType ([#] → (Blist • #) → (Blist • #))) :=
  fun gamma A x l => Bcons_aux x l.


(*Non-dependent eliminator for lists*)
Definition Blist_rec (Γ : BCtx) :
  @BEl Γ (∏ Γ BType
            (∏ _ BType
               ([#] →
                ([↑#] → Blist • ↑ # → [#] → [#]) →
                Blist • ↑ # →
                [#]))).
Proof.
  unshelve refine (fun gamma B P pnil pcons => _). 
  refine (fix f l {struct l} := match l with
                     | Bnil_aux => pnil
                     | Bcons_aux x q => pcons x q (f q)
                     | Bêtalist g x => P.(snd) (fun y => f (g y)) x
                     end).
Defined.


(*Storage operator for lists*)
Definition Blist_stor{Γ : BCtx } :
  BEl (∏ Γ BType (Blist • # → (Blist • # → BType) → BType)) :=
  fun (_ : Γ) B =>
       fix f (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
         match l with
         | Bnil_aux => fun P : @BranchingList B -> BranchingTYPE => P (Bnil_aux)
         | Bcons_aux x q =>
             fun P : @BranchingList B -> BranchingTYPE =>
               f q (fun l' : @BranchingList B => P (Bcons_aux x l'))
         | Bêtalist g x => fun P : @BranchingList B -> BranchingTYPE => Bunit
         end.



(*Restricted dependent-eliminator for lists.*)
Definition Blist_rect {Γ : BCtx} :
  @BEl Γ (∏ Γ BType
            (∏ _ ((Blist • #) → BType)
               ((@BAppN _ _ BType # (Bnil • (↑#))) →
                 (∏ _ [↑(@BVar _ BType)]
                    (∏ (Γ · BType · ((Blist • #) → BType) · (↑#))
                       (Blist • (↑↑(@BVar _ BType)))
                       (([(Blist_stor • (↑↑↑(@BVar _ BType)))
                            ◊ (@BVar _ ((Blist • (↑↑#))))
                            ◊ (↑↑(@BVar _ ((Blist • #) → BType)))]) →
                        ([(Blist_stor • (↑↑↑(@BVar _ BType)))
                            ◊ ((Bcons • (↑↑↑(@BVar _ BType))) ◊ (↑#) ◊ #)
                            ◊ (↑↑(@BVar _ ((Blist • #) → BType)))])))) →
                ∏ (Γ · BType · ((Blist • #) → BType)) (Blist • ↑#)
                  [(Blist_stor • (↑↑(@BVar _ BType))) ◊ # ◊ (↑#)]))) :=
  fun _ B P pnil pcons =>
    fix f l := match l as l0 return
                     ((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
                         match l with
                         | Bnil_aux => fun P => P (Bnil_aux)
                         | Bcons_aux x q =>
                           fun P =>
                             g q (fun l' => P (Bcons_aux x l'))
                         | Bêtalist g x => fun P => Bunit
                         end) l0 P).(fst)
               with
               | Bnil_aux => pnil
               | Bcons_aux x q => pcons x q (f q)
               | Bêtalist _ _ => tt
               end.



  
End BranchingTranslation.



Section Parametricity.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Variables (X Y : Type).
Definition ℙ := X -> Y.
Notation "'ACtx'" := (ACtx X Y).
Notation "'ACtx_nil'" := (@ACtx_nil X Y).
Notation "'BTy'" := (BTy X Y).


(*In this section we present the Algebraic Binary
Parametricity translation, which binds together
the two previous ones.
Again, we use a Cwf-like presentation *)

(*An algebraic binary parametric type is made of a binary predicate
 Te, together with the proof that it is algebraic in respect to the
Branching translation*)
Set Printing Universes.

Definition ETy_aux (α : X -> Y) (A : Type) (B : BranchingTYPE X Y) :=
  {Te : A -> fst B -> Type &
                      forall (a : A) (f : Y -> fst B) (x : X),
                        Te a (f (α x)) -> Te a (snd B f x)}.

(*Contexts are relations on contexts from the Axiom
translation and from the Branching translation.
As such, they start by α : ℙ.*)
Definition ECtx (Γa : ACtx) (Γb : BCtx) :=
  forall (α : ℙ),  Γa α -> Γb -> Type.


(*ETy is simply ETy_aux depending on contexts*)
Definition ETy (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (A : ATy Γa) (B : BTy Γb) :=
  forall (α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb),
    ETy_aux α (A α γa) (B γb).


Definition EElt_aux {α : X -> Y} (A : Type) (B : BranchingTYPE X Y)
           (R : ETy_aux α A B) (a : A) (b : B.(fst)) :=
  R.(fst) a b.

(*EElt is the parametric version of Tarsky's El function*)
Definition EElt (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (ra : AEl Ra) (rb : BEl Rb) :=
  forall (α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb),
    EElt_aux (Re α γa γb γe) (ra α γa) (rb γb).

(*As for the Branching translation, the translation of Type
is the constant function that always returns ETy_aux, and
we ensure algebraicity through a dummy function.*)
Definition Ue {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  ETy Γe (@AType _ _ _) (@BType _ _ _).
Proof.
  unshelve refine (fun α γa γb γe => exist _).
  + refine (fun A B => @tsig (A -> B.(fst) -> Type) _).
    exact (fun Te => forall (a : A) (f : Y -> B.(fst)) (x : X) (fe : Te a (f (α x))),
                Te a ((B.(snd) f x))).

  + intros A f x fe.
    unshelve refine (exist _).
    * exact (fun _ _ => unit).
    * exact (fun _ _ _ _ => tt).
Defined.

(*Empty context*)

Definition ECtx_nil : ECtx ACtx_nil (BCtx_nil) :=
  fun _ _ _ => unit.


Definition Ectx_nil {α : ℙ} : @ECtx_nil α tt tt := tt.


Notation "()" := Ectx_nil.



(*Context extension*)

Definition ECtx_cons (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb) :
  ECtx (ACtx_cons Ra) (BCtx_cons Rb).
Proof.
  unshelve refine (fun α γa γb => _).
  apply (@tsig (Γe α γa.(fst) γb.(fst))).
  intro γe.
  exact ((Re α _ _ γe).(fst) γa.(snd) γb.(snd)).
Defined.


Notation "Γe · Re" := (@ECtx_cons _ _ Γe _ _ Re) (at level 50, left associativity).

Definition ETy_inst (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb)
           (ra : Ra α γa) (rb : (Rb γb).(fst)) :=
  (Re α γa γb γe).(fst) ra rb.


Definition Ectx_cons (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb)
           (ra : Ra α γa) (rb : (Rb γb).(fst)) (re : ETy_inst Re γe ra rb) :
  (Γe · Re) (Actx_cons ra) (Bctx_cons rb) :=
  {| fst := γe; snd := re |}.


Notation "γe ·· xe" := (@Ectx_cons _ _ _ _ _ _ _ _ _ γe _ _ xe) (at level 50, left associativity).


(*In what follows, we deal with the negative fragment
of type theory : Weakening, Pi-types, Substitution, etc*)

(*Lifting rule*)

Definition ELift (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
  : ETy (Γe · Re) (@ALift X Y _ Ra Sa) (@BLift X Y _ Rb Sb) :=
  fun α γa γb γe => Se α γa.(fst) γb.(fst) γe.(fst).


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


(*Weakening rule*)
Definition EWeaken (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
           (ra : AEl Ra) (rb : BEl Rb) (re : EElt Re ra rb) :
  @EElt _ _ (Γe · Se) _ _ (⇑ Re) (AWeaken ra) (BWeaken rb) :=
  fun α γa γb γe => re α _ _ γe.(fst).

Notation "↑ M" := (@EWeaken _ _ _ _ _ _ _ _ _ _ _ M) (at level 10).


(*Variable rule*)

Definition EVar (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb) :
  @EElt _ _ (Γe · Re) _ _ (ELift Re) (@AVar X Y _ Ra) (@BVar X Y _ Rb) :=
  fun α γa γb γe => γe.(snd).

Arguments EVar {Γa} {Γb} {Γe} {Ra} {Rb} _.

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


(*Substitution*)

Definition ESub (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy (ACtx_cons Ra)) (Sb : BTy (BCtx_cons Rb))
           (Se : ETy (Γe · Re) Sa Sb)
           (ra : AEl Ra) (rb : BEl Rb) (re : EElt Re ra rb) :
  ETy Γe (ASub Sa ra) (BSub Sb rb) :=
  fun α γa γb γe => Se _ _ _ (γe ·· (re α γa γb γe)).


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


(*Pi-type*)

Definition EPi {Γa : ACtx} {Γb : BCtx} (Γe : ECtx Γa Γb)
           {Ra : ATy Γa} {Rb : BTy Γb} (Re : ETy Γe Ra Rb)
           {Sa : ATy (ACtx_cons Ra)} {Sb : BTy (BCtx_cons Rb)}
           (Se : ETy (Γe · Re) Sa Sb) :
  ETy Γe (APi Sa) (BPi Sb).
Proof.
  unshelve refine (fun α γa γb γe => exist _).
  + exact (fun fa fb =>
             forall (ra : Ra α γa) (rb : (Rb γb).(fst))
                    (re : ETy_inst Re γe ra rb),
               (Se α _ _ (γe ·· re)).(fst) (fa ra) (fb rb)).
  + unshelve refine (fun _ _ _ fe ra rb re =>
                       (Se α _ _ (γe ·· re)).(snd) _ _ _ _).
    exact (fe ra rb re).
Defined.

Notation "∏ A B" := (@EPi _ _ _ _ _ A _ _ B) (at level 100).

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

(*Introduction for Pi*)
Definition ELam (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy (ACtx_cons Ra)) (Sb : BTy (BCtx_cons Rb))
           (Se : ETy (Γe · Re) Sa Sb)
           (fa : AEl Sa) (fb : BEl Sb) (fe : EElt Se fa fb) :
  EElt (EPi Se) (ALam fa) (BLam fb) :=
  fun _ _ _ γe _ _ re => fe _ _ _ (γe ·· re).


Notation "'λ'" := ELam.


(*Introduction of the non-dependent arrow*)


Definition ELamN (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
           fa fb (fe : @EElt _ _ (Γe · Re) _ _ (⇑ Se) fa fb) :
  EElt (Re → Se) (ALamN fa) (BLamN fb) :=
  @ELam _ _ Γe _ _ Re _ _ (⇑ Se) _ _ fe.


(*Elimination for Pi*)

Definition EApp (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy (ACtx_cons Ra)) (Sb : BTy (BCtx_cons Rb))
           (Se : ETy (Γe · Re) Sa Sb)
           (fa : AEl (APi Sa)) (fb : BEl (BPi Sb))
           (fe : EElt (EPi Se) fa fb)
           (ra : AEl Ra) (rb : BEl Rb) (re : EElt Re ra rb) :
  EElt (Se {{re}}) (AApp fa ra) (BApp fb rb) :=
  fun α γa γb γe => fe _ _ _ _ _ _ (re α γa γb γe).

Notation "t • u" := (EApp t u) (at level 12, left associativity).


(*Elimination of the non-dependent arrow*)

Definition EAppN (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
           (Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
           fa fb (fe : EElt (Re → Se) fa fb)
           ra rb (re : EElt Re ra rb) : EElt Se (AAppN fa ra) (BAppN fb rb) :=
  @EApp _ _ Γe _ _ Re _ _ (⇑ Se) _ _ fe _ _ re.

Notation "t ◊ u" := (@EAppN _ _ _ _ _ _ _ _ _ _ _ t _ _ u) (at level 12, left associativity).


(*Internal Tarsky's El function*)

Definition EREL (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
           (Ra : AEl (@AType X Y Γa)) (Rb : BEl (@BType X Y Γb))
           (Re : EElt (@Ue _ _ Γe) Ra Rb) : ETy Γe Ra Rb :=
  Re.

Notation "[ A ]" := (@EREL _ _ _ _ _ A).

(*The translation of booleans*)
Inductive EParabool (α : X -> Y) :
  bool -> (BranchingBool X Y) -> Type :=
| EParatrue : EParabool α true (@Btrue_aux X Y)
| EParafalse : EParabool α false (@Bfalse_aux X Y)
| EParabêtabool : forall  (bo : bool) (f : (Y ->  BranchingBool X Y)) (x : X)
                        (rel : EParabool α bo (f (α x)) ),
    EParabool α bo (Bêtabool f x).


Definition Ebool {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  ETy Γe (@Abool X Y Γa) (@Bbool X Y Γb) :=
  (fun (α : ℙ) _ _ _ => {| fst := EParabool α; snd := @EParabêtabool α |}).


Definition Etrue {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (@Ebool _ _ Γe) (@Atrue X Y Γa) (@Btrue X Y Γb) :=
  fun α _ _ _ => @EParatrue α.


Definition Efalse {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (@Ebool _ _ Γe) (@Afalse X Y Γa) (@Bfalse X Y Γb) :=
  fun α _ _ _ => @EParafalse α.

(*Non-dependent eliminator for booleans*)

Definition Ebool_rec (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb) :
  @EElt _ _ Γe _ _ (@EPi _ _ _ _ _ Ue _ _ ([EVar Ue] → [EVar Ue] → Ebool → [EVar Ue]))
        (@Abool_rec X Y Γa) (@Bbool_rec X Y Γb).
Proof.
  unshelve refine (fun α γa γb γe Pa Pb Pe pta ptb pte pfa pfb pfe => _).
  exact (fix f _ _ b := match b with
                                  | EParatrue _ => pte
                                  | EParafalse _ => pfe
                                  | EParabêtabool rel =>
                                    Pe.(snd) _ _  _ (f _ _ rel)
                              end).
Defined.

(*Storage operator for booleans*)

Definition Ebool_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  @EElt _ _ Γe _ _ (Ebool → (Ebool → Ue) → Ue) (@Abool_stor X Y Γa) (@Bbool_stor X Y Γb).
Proof.
  pose (r := EApp (@Ebool_rec _ _ Γe) ((Ebool → Ue) → Ue)).
  let T := constr:(@EElt _ _ Γe _ _ (((Ebool → Ue) → Ue) → ((Ebool → Ue) → Ue) → Ebool → ((Ebool → Ue) → Ue)) (AApp (@Abool_rec _ _ Γa) _) (BApp (@Bbool_rec _ _ Γb) _)) in
  unshelve refine (let r : T := r in _).
  unshelve refine (EAppN (EAppN r _) _).
  + refine (ELamN (@EAppN _ _ _ _ _ Ebool _ _ Ue (@AVar X Y _ _) (@BVar X Y _ _)  # _ _ Etrue)).
  + refine (ELamN (@EAppN _ _ _ _ _ Ebool _ _ Ue (@AVar X Y _ _) (@BVar X Y _ _)  # _ _ Efalse)).
Defined.

(*Restricted dependent eliminator for booleans*)

Definition Ebool_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (EPi (Γe := Γe) (Re := (Ebool → Ue)) (
               [@EApp _ _ (Γe · (Ebool → Ue)) _ _ Ebool _ _ Ue _ _ # _ _ Etrue] →
               [@EApp _ _ (Γe · (Ebool → Ue)) _ _ Ebool _ _ Ue _ _ # _ _ Efalse] →
               (@EPi _ _ _ _ _ Ebool _ _ [(Ebool_stor • #) • (↑#)])))
       (@Abool_rect X Y Γa) (@Bbool_rect _ _ Γb) :=
  fun α γa γb γe Pa Pb Pe pta ptb pte pfa pfb pfe ba bb be =>
    match be as be0 in EParabool _ ba0 bb0
    with
    | EParatrue _ => pte
    | EParafalse _ => pfe
    | EParabêtabool rel => tt
    end.


(*The translation of natural numbers*)

Inductive EParanat (α : X -> Y) : nat -> BranchingNat X Y -> Type :=
| EP0 : EParanat α 0 (@B0 X Y)
| EPS : forall (no : nat) (nt :  BranchingNat X Y)
                     (ne : EParanat α no nt),
    EParanat α (S no) (BS nt)
| EPbêta : forall  (no : nat) (f : (Y ->  BranchingNat X Y)) (x : X)
                        (rel : EParanat α no (f (α x)) ),
    EParanat α no (Bêtanat f x).


Definition Enat {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
  ETy Γe (@Anat X Y Γa) (@Bnat X Y Γb).
Proof.
  unshelve refine (fun α γa γb γe => exist _).
  - exact (EParanat α).
  - exact (@EPbêta α).
Defined.


Definition E0 {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (@Enat _ _ Γe) (@A0 X Y Γa) (@Bzero X Y Γb) :=
  fun α _ _ _ => EP0 α.

Definition ES {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  @EElt _ _ Γe _ _ (Enat → Enat) (@ASucc X Y Γa) (@BSucc X Y Γb) :=
  fun α _ _ _ _ _ ne => EPS ne.


(*Non-dependent eliminator for natural numbers*)

Definition Enat_rec (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb): 
  @EElt _ _ Γe _ _ (EPi (Re:= Ue) ([EVar Ue] → (Enat → [EVar Ue] → [EVar Ue]) → Enat → [EVar Ue]))
        (@Anat_rec X Y Γa) (@Bnat_rec X Y Γb).
Proof.
  cbv.
  unshelve refine (fun α γa γb γe Pa Pb Pe p0a p0b p0e pSa pSb pSe => _).
  refine (fix g na nb ne :=
            match ne as n in EParanat _ mo mt return
                  fst Pe
                      ((fix f (n : nat) : Pa :=
                          match n with
                          | 0 => p0a
                          | S k => pSa k (f k)
                          end) mo)
                      ((fix f (n : BranchingNat X Y) : fst Pb :=
                          match n with
                          | B0 _ _ => p0b
                          | BS k => pSb k (f k)
                          | Bêtanat g x => snd Pb (fun y : Y => f (g y)) x
                          end) mt)                                     
            with
            | EP0 _ => p0e
            | @EPS _ ka kb ke => pSe _ _ ke _ _ (g ka kb ke)
            | @EPbêta _ ka f x rel => Pe.(snd) _ _ _ (g ka (f (α x)) rel) 
            end).
Defined.


(*Storage operator for natural numbers*)

Definition Enat_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
  @EElt  _ _ Γe _ _ (Enat → (Enat → Ue) → Ue) (@Anat_stor X Y Γa) (@Bnat_stor X Y Γb).
Proof.
  pose (r := EApp (@Enat_rec _ _ Γe) ((Enat → Ue) → Ue)).
  let T := constr:(EElt (Γe := Γe) (((Enat → Ue) → Ue) → (Enat → ((Enat → Ue) → Ue) → ((Enat → Ue) → Ue)) → Enat → ((Enat → Ue) → Ue)) (AApp (@Anat_rec _ _ Γa) _) (BApp (@Bnat_rec _ _ Γb) _)) in
  unshelve refine (let r : T := r in _).
  unshelve refine (EAppN (EAppN r _) _).
  - refine (ELamN (EAppN (Re := Enat) (Se := Ue) _ _)).
    + now refine #.
    + now refine E0.
  - refine (@ELamN _ _ _ _ _ _ _ _ _ _ _ _).
    refine (ELamN (Γe:= Γe · Enat) (Re:= (⇑((Enat → Ue) → Ue))) (Se:= (⇑ ((Enat → Ue) → Ue))) _).
    refine (ELamN (Γe:= (Γe · Enat · (⇑ ((Enat → Ue) → Ue))))
                  (Re:= (⇑(⇑(Enat → Ue)))) (Se:= (⇑ (⇑ Ue))) _).
    refine (EAppN (Re:= Enat) _ _).
    + now refine #.
    + now refine (EAppN (Re:= Enat) ES (↑↑(EVar Enat))).
Defined.


(*Restricted dependent eliminator for natural numbers*)

Definition Enat_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
  EElt (EPi (Γe:= Γe) (Re:= Enat → Ue)
            ([EApp (Γe := (Γe · (Enat → Ue))) (Re:= Enat) (Se:= Ue) # E0] →
             [EPi (Re:= Enat) ([EApp (Γe:= Γe · (Enat → Ue) · Enat) (Se:= Ue)
                                     (EApp (Γe:= Γe · (Enat → Ue) · Enat) Enat_stor #) (↑#)] →
                               [EApp (Γe:= Γe · (Enat → Ue) · Enat) (Se:= Ue)
                                     (EApp (Γe:= Γe · (Enat → Ue) · Enat) Enat_stor
                                           (EApp (Γe:= Γe · (Enat → Ue) · Enat) ES #)) (↑#)])] →
             EPi (Re:= Enat) [EApp (Γe:= Γe · (Enat → Ue) · Enat) (Se:= Ue)
                                   (EApp (Γe:= Γe · (Enat → Ue) · Enat) Enat_stor #) (↑#)]))
       (@Anat_rect X Y Γa) (@Bnat_rect X Y Γb).
Proof.
  unshelve refine (fun α γa γb γe Pa Pb Pe p0a p0b p0e pSa pSb pSe => _).
  now refine (fix g na nb ne :=
            match ne as n in EParanat _ mo mt
            with
            | EP0 _ => p0e
            | @EPS _ ka kb ke => pSe _ _ ke _ _ (g ka kb ke)
            | @EPbêta _ ka f x rel => tt 
            end).
Defined.


(*The two following propositions are Propositions 19 and 20 in our paper *)
Proposition Specification_unicity {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  forall (na : AEl (@Anat X Y Γa)) (nb : BEl (@Bnat X Y Γb)) (α : X -> Y)
         (γa : Γa α) (γb : Γb) (γe : Γe α γa γb),
    EParanat α (na α γa) (nb γb) -> na α γa = BNdialogue (nb γb) α.
Proof.
  intros na nb α γa γb γe ne.
  induction ne ; trivial ; now apply eq_S.
Defined.  

Proposition Generic_Parametricity :
  forall (α : X -> Y) (nb : BranchingNat X Y),
    EParanat α (BNdialogue nb α) nb.
Proof.
  now refine (fix g α nb :=
            match nb as n return
                  EParanat _ (BNdialogue n α) n
            with
            | B0 _ _ => EP0 α
            | BS kb => EPS (g α kb)
            | Bêtanat f x => EPbêta (g α (f (α x)))
            end).
Defined.


(*The translation of equality*)

Inductive EParaeq {α : X -> Y} (A : Type) (B : BranchingTYPE X Y) (E : ETy_aux α A B)
          (ta : A) (tb : B.(fst)) (te : EElt_aux E ta tb) :
  forall (ua : A) (ub : B.(fst)) (ue : EElt_aux E ua ub),
  (Eq ta ua) -> (BranchingEq tb ub) -> Type :=
| EParaeq_refl : EParaeq te te (Eq_refl ta) (Beq_refl tb)
| EParabêtaeq : forall (ua : A) (ub : B.(fst)) (ue : EElt_aux E ua ub)
                       (e : Eq ta ua)
                       (f : Y -> BranchingEq tb ub) (x : X)
                       (rel : EParaeq te ue e (f (α x))),
    EParaeq te ue e (Bêtaeq f x).


Definition Eeq {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe := Γe) (EPi (Γe := Γe) (Re:= Ue) ((EVar Ue) → (EVar Ue) → Ue))
       (@Aeq X Y Γa) (@Beq X Y Γb).
Proof.
  unshelve refine (fun α γa γb γe Ra Rb Re ta tb te ua ub ue => exist _). 
  - exact (EParaeq te ue).
  - exact (EParabêtaeq (te:= te) (ue:= ue)).
Defined.

Definition Eeq_refl {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (EPi (Γe := Γe) (Re:= Ue)
            (EPi (Γe := Γe · Ue) (Re:= [EVar Ue])
                 [(EApp (Γe := Γe · Ue · [EVar Ue])
                        (Re := Ue)
                        (Se:= (EVar Ue) → (EVar Ue) → Ue) Eeq (↑#)) ◊ # ◊ #]))
       (@Arefl _ _ Γa) (@Brefl _ _ Γb) :=
  fun α γa γb γe Ra Rb Re ra rb re => EParaeq_refl re. 


(*Non-dependent eliminator for equality*)

Definition Eeq_rec {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe:= Γe) (EPi (Γe:= Γe) (Re:= Ue)
            (EPi (Re:= [EVar Ue])
               (EPi (Γe:= Γe · Ue · (EVar Ue))
                  (Re:= [↑(EVar Ue)] → Ue)
                  ([(EVar (Γe:= Γe · Ue · (EVar Ue))
                          ([↑(EVar Ue)] → Ue)) ◊ ↑#] →
                (EPi (Γe:= Γe · Ue · (EVar Ue) · ([↑(EVar Ue)] → Ue))
                   (Re:= [↑↑#])
                   ([((Eeq • (↑↑↑(EVar Ue))) ◊ ↑↑#) ◊ #] →
                 [(↑(EVar (Γe:= Γe · Ue · (EVar Ue))
                          ((↑(EVar Ue)) → Ue))) ◊ #]))))))
       (@Aeq_rec _ _ Γa) (@Beq_rec _ _ Γb) :=
  fun α γa γb γe Ra Rb Re xa xb xe Pa Pb Pe pa pb pe =>
    fix g ya yb ye eqa eqb eqe :=
             match eqe in (@EParaeq _ _ _ _ _ _ _ ya0 yb0 ye0 eqa0 eqb0)
                   return (Pe ya0 yb0 ye0).(fst)
                                             (match eqa0 in (Eq _ ya0)
                                                    return (Pa ya0)
                                              with
                                              | Eq_refl _ => pa
                                              end)
                                             ((fix g y e :=
                                                 match e in (BranchingEq _ yb0)
                                                       return (fst (Pb yb0))
                                                 with
                                                 | Beq_refl _ => pb
                                                 | @Bêtaeq _ _ _ _ b f x => snd (Pb b) (fun z : Y => g b (f z)) x
        end) yb0 eqb0)
             with
            | EParaeq_refl _ => pe
            | @EParabêtaeq _ _ _ _ _ _ _ za zb ze eqza f x rel =>
              (Pe za zb ze).(snd) _ _ x (g za zb ze eqza (f (α x)) rel)
             end.

(*Storage operator for equality, in direct style*)
  
Definition Eeq_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe:= Γe)
       (EPi (Γe:= Γe) (Re:= Ue)
            (EPi (Re:= [EVar Ue])
               (EPi (Re:= [↑(EVar Ue)])
                    ([((Eeq • (↑↑(EVar Ue))) ◊ ↑#) ◊ #] →
                     (EPi (Γe:= Γe · Ue · [EVar Ue] · [↑(EVar Ue)])
                          (Re:= [↑↑(EVar Ue)])
                      ([((Eeq • (↑↑↑(EVar Ue))) ◊ (↑↑#)) ◊ #] →
                       Ue)) →
                     Ue))))
       (@Aeq_stor _ _ Γa) (@Beq_stor _ _ Γb).
Proof.
  cbv.
  refine (fun α γa γb γe Ra Rb Re xa xb xe ya yb ye eqa eqb eqe =>
            match eqe in (@EParaeq _ _ _ _ _ _ _ ya0 yb0 ye0 eqa0 eqb0)
            with
            | EParaeq_refl _ =>
              fun Pa Pb Pe => Pe xa xb xe (Eq_refl xa) (Beq_refl xb) (EParaeq_refl xe)
            | @EParabêtaeq _ _ _ _ _ _ _ za zb ze eqza f x rel =>
              fun Pa Pb Pe => {|fst := fun _ _ => unit ;
                                snd := fun _ _ _ _ => tt |}
            end).
Defined.


(*As for the two previous translations, unification problems forbid us
from writing Eeq_rect*)


(*The translation of lists*)

Arguments nil {A}.
Notation "x :: l" := (cons x l).


Inductive EParalist {α : X -> Y} (A : Type) (B : BranchingTYPE X Y) (E : ETy_aux α A B)
  : list A -> (@BranchingList X Y B) -> Type :=
| EParanil : EParalist E nil (@Bnil_aux X Y _)
| EParacons : forall (la : list A) (lb :  @BranchingList X Y B)
                     (le : EParalist E la lb)
                     (a : A) (b : B.(fst))
                     (e : EElt_aux E a b),
    EParalist E (a :: la) (Bcons_aux b lb)
| EParabêtalist : forall (la : list A)
                         (f : Y -> (@BranchingList X Y B))
                         (x : X)
                         (rel : EParalist E la (f (α x))),
    EParalist E la (Bêtalist f x).


Definition Elist {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe := Γe) (Ue → Ue) (@Alist _ _ Γa) (@Blist _ _ Γb).
Proof.
  unshelve refine (fun alpha γa γb γe Ra Rb Re => exist _).    
    + exact (EParalist Re).
    + exact (EParabêtalist (E := Re)).
Defined.


Definition Enil {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe := Γe) (EPi (Re := Ue) (Elist • (EVar Ue))) (@Anil _ _ _) (@Bnil _ _ _) :=
  fun α γa γb γe Ra Rb Re => EParanil _.


Definition Econs {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe := Γe) (EPi (Re := Ue) ((EVar Ue) → [EApp Elist (EVar Ue)] → [EApp Elist (EVar Ue)]))
       (@Acons _ _ _) (@Bcons _ _ _) :=
  fun α γa γb γe Ra Rb Re ra rb re la lb le => EParacons le re.


(*Non-dependent eliminator for lists*)

Definition Elist_rec {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
  EElt (Γe := Γe) (EPi (Re := Ue)
            (EPi (Re := Ue)
               ([EVar Ue] →
                ([↑(EVar Ue)] → Elist • ↑ (EVar Ue) → [EVar Ue] → [EVar Ue]) →
                Elist • ↑ (EVar Ue) →
                [EVar Ue]))) (@Alist_rec _ _ _) (@Blist_rec _ _ _)
  :=
  fun α γa γb γe Ra Rb Re Pa Pb Pe pnila pnilb pnile pconsa pconsb pconse =>
    fix f la lb le {struct le} :=
    match le as le0 in EParalist _ la0 lb0
          return
          fst Pe
              ((fix f (l : list Ra) : Pa :=
                  match l with
                  | nil => pnila
                  | (x :: q) => pconsa x q (f q)
                  end) la0)
              ((fix f (l : BranchingList (Y:=Y)) : fst Pb :=
                  match l with
                  | @Bnil_aux _ _ => pnilb
                  | Bcons_aux x q => pconsb x q (f q)
                  | Bêtalist g x => snd Pb (fun y : Y => f (g y)) x
                  end) lb0)
    with
    | @EParanil _ _ _ _ => pnile
    | @EParacons _ _ _ _ qa qb qe ra rb re =>
      pconse ra rb re qa qb qe _ _  ((f qa qb qe)) 
    | @EParabêtalist _ _ _ _ qa g x rel => Pe.(snd) _ _ _ (f qa (g (α x)) rel)
    end.


(*Storage operator for lists, in direct style*)

Definition Elist_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe := Γe) (EPi (Re := Ue) (Elist • (EVar Ue) → (Elist • (EVar Ue) → Ue) → Ue))
       (@Alist_stor _ _ _) (@Blist_stor _ _ _).
Proof.
  unshelve refine (fun α γa γb γe Ra Rb Re  => _).
  unshelve refine (fix f la lb le :=
                     match le as le0 in EParalist _ la0 lb0
                     with
                     | EParanil _ => fun _ _ Pe => (Pe nil (@Bnil_aux X Y _) (EParanil _))
                     | @EParacons _ _ _ _ qa qb qe ra rb re =>
                       fun Pa Pb Pe => f qa qb qe _ _ (fun la lb le => Pe _ _ (EParacons le re))
                     | @EParabêtalist _ _ _ _ qa g x rel =>
                       fun Pa Pb Pe => ((ELift Ue _ ).(snd) _ _ x _)
                     end).
  - exact (fun y => @Blist_stor X Y _ _ _ (g y) Pb).
  - exact (f _ _ rel Pa Pb Pe).
Defined.


(*Restricted dependent eliminator for lists*)

Definition Elist_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe:= Γe) (EPi (Re:= Ue)
                      (EPi (Re:= (Elist • (EVar Ue)) → Ue)
                      ((EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue))
                              (Re:= ⇑(Elist • ((EVar Ue)))) (Se:= Ue) # (Enil • (↑(EVar Ue)))) →
                       (EPi (Re:= [↑(EVar Ue)])
                            (EPi (Re:= Elist • (↑↑(EVar Ue)))
                                 (([(EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (↑#) · (Elist • (↑↑(EVar Ue))))
                                           (Re:= (Elist • (↑ ↑ ↑(EVar Ue))))
                                           (Se:= ((Elist • (↑ ↑ ↑(EVar Ue))) → Ue) → Ue)
                                           (Elist_stor • (↑↑↑(EVar Ue)))
                                           (EVar ((Elist • (↑↑(EVar Ue))))))
                                      ◊ (↑↑(EVar ((Elist • (EVar Ue)) → Ue)))]) →
                                  ([(EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (↑#) · (Elist • (↑↑(EVar Ue))))
                                  (Re:= (Elist • (↑ ↑ ↑(EVar Ue))))
                                  (Se:= ((Elist • (↑ ↑ ↑(EVar Ue))) → Ue) → Ue)
                                  (Elist_stor • (↑↑↑(EVar Ue)))
                                  ((EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (↑#) · (Elist • (↑↑(EVar Ue))))
                                          (Re:= ↑ ↑ ↑(EVar Ue))
                                          (Se:= (Elist • (↑ ↑ ↑ (EVar Ue))) → (Elist • (↑ ↑ ↑ (EVar Ue))))
                                          (Econs • (↑↑↑(EVar Ue))) (↑#)) ◊ #))
                                      ◊ (↑↑(EVar ((Elist • (EVar Ue)) → Ue)))])))) →
                       EPi (Re:= Elist • ↑(EVar Ue))
                           [(EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (Elist • ↑(EVar Ue)))
                                   (Re:= (Elist • (↑ ↑ (EVar Ue))))
                                   (Se:= ((Elist • (↑ ↑(EVar Ue))) → Ue) → Ue) 
                                   (Elist_stor • (↑↑(EVar Ue))) #) ◊ (↑#)])))
       (@Alist_rect X Y Γa) (@Blist_rect X Y Γb).
Proof.
  vm_compute.intros α γa γb γe Ra Rb Re.




(*Restricted dependent-eliminator for lists.*)
Definition Elist_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
  EElt (Γe := Γe) (EPi (Re := Ue)
            (EPi  (Re := ((Elist • #) → Ue))
               ((EAppN (Se := Ue) # (Enil • (↑#))) →
                 (EPi  (Re := [↑(EVar Ue)])
                    (EPi (Γe := (Γe · Ue · ((Elist • #) → Ue) · (↑#)))
                       (Re :=  (Elist • (↑↑(EVar Ue))))
                       (([(EAppN 
                                 (@EApp _ _ _ _ _ Ue _ _
                                        (Elist • (EVar Ue) → (Elist • (EVar Ue) → Ue) → Ue)
                                        (@Alist_stor X Y _) (@Blist_stor _ _ _) 
                                   Elist_stor _ _ (↑↑↑(EVar Ue)))
                                 (EVar ((Elist • (↑↑(EVar Ue))))))
                            ◊ (↑↑(EVar ((Elist • #) → Ue)))]) →
                        ([(Elist_stor • (↑↑↑(EVar Ue)))
                            ◊ ((Econs • (↑↑↑(EVar Ue))) ◊ (↑#) ◊ #)
                            ◊ (↑↑(@EVar _ ((Elist • #) → Ue)))])))) →
                EPi (Γe := Γe · Ue · ((Elist • #) → Ue)) (Re := (Elist • ↑#))
                    [(Elist_stor • (↑↑(EVar Ue))) ◊ # ◊ (↑#)])))
       (@Alist_rect X Y Γa) (@Blist_rect X Y Γb).
Proof.
  unshelve refine (fun gamma B P pnil pcons => _).
  refine (fix f l := match l as l0 return
                           ((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
                              match l with
                              | Bnil_aux => fun P => P (Bnil_aux)
                              | Bcons_aux x q =>
                                fun P =>
                                  g q (fun l' => P (Bcons_aux x l'))
                              | Bêtalist g x => fun P => Bunit
                              end) l0 P).(fst)
                     with
                     | Bnil_aux => pnil
                     | Bcons_aux x q => pcons x q (f q)
                     | Bêtalist _ _ => tt
                     end).*)




End Parametricity.


Section AvareXY.

Unset Implicit Arguments.
Variables X Y : Type.
Notation "'ℙ'" := (X -> Y).
Notation "'ACtx'" := (ACtx X Y).
Notation "'BTy'" := (BTy X Y).

Definition Ctx :=
  triple (fun (A : ACtx) (B : BCtx) =>
            forall (α : ℙ),  A α -> B -> Type).

Definition Ctx_El (Γ : Ctx) (α : ℙ) :=
    triple (fun (a : Γ.(q1) α) (b : Γ.(q2)) =>
              Γ.(q3) α a b).

Notation " Γ ‡ α " := (Ctx_El Γ α) (at level 11).


Definition Ty (Γ : Ctx) : Type :=
    triple (fun (A :  ATy Γ.(q1)) (B : BTy Γ.(q2)) =>
              forall (α : ℙ) (γ : Ctx_El Γ α),
                tsig (fun (Te : A α (γ.(q1)) -> (B γ.(q2)).(fst) -> Type) =>
                        forall (a : A α (γ.(q1)))
                               (f : Y -> (B γ.(q2)).(fst))
                               (x : X) (fe : Te a (f (α x))), Te a ((B γ.(q2)).(snd) f x))).

Definition RElt (Γ : Ctx) (R : Ty Γ) : Type :=
    triple (fun (a : AEl R.(q1)) (b : BEl R.(q2)) =>
              forall (α : ℙ) (γ : Ctx_El Γ α),
                (R.(q3) α γ).(fst) (a α γ.(q1)) (b γ.(q2))).



Definition Ty_inst {Γ : Ctx} {α : ℙ} (R : Ty Γ)  (γ : Ctx_El Γ α) : Type
  :=
    triple (fun (a : R.(q1) α γ.(q1)) (b : (R.(q2) γ.(q2)).(fst)) =>
            (R.(q3) α γ).(fst) a b).


Definition Inst {Γ : Ctx} {R : Ty Γ} {α : ℙ} (r : RElt _ R)
            (γ : Ctx_El Γ α) : Ty_inst R γ.
Proof.
  exists (r.(q1) α γ.(q1)) (r.(q2) γ.(q2)).
  exact (r.(q3) α γ).
Defined.  


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



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


Definition ctx_nil {α : ℙ} : Ctx_nil ‡ α.
Proof.
  exists tt tt.
  exact: tt.
Defined.

Notation "()" := ctx_nil.

Definition Ctx_cons (Γ : Ctx) (R : Ty Γ) : Ctx.
Proof.
  exists (ACtx_cons R.(q1)) (BCtx_cons R.(q2)).
  intros α Acons Bcons.
  apply (@tsig (Γ.(q3) α Acons.(fst) Bcons.(fst))).
  intro γe.
  exact ((R.(q3) α (exist3 γe)).(fst) Acons.(snd) Bcons.(snd)).
Defined.


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



Definition ctx_cons {Γ : Ctx} {R : Ty Γ} {α : ℙ}
           (γ : Γ ‡ α) (x : Ty_inst R γ) :
  (Γ · R) ‡ α.
Proof.
  destruct x as [xa xb xe].
  exists (Actx_cons xa) (Bctx_cons xb).
  exists γ.(q3).
  exact xe.
Defined.

Notation "γ ·· x" := (ctx_cons γ x) (at level 50, left associativity).


Definition Ctx_tl {Γ : Ctx} {R : Ty Γ} {α : ℙ}
           (γ : Ctx_El (Γ · R) α) : Ctx_El Γ α.
Proof.
  exists γ.(q1).(fst) γ.(q2).(fst).
  exact (γ.(q3).(fst)).
Defined.


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


Definition Lift {Γ : Ctx} {R1 : Ty Γ}  (R2 : Ty Γ) : Ty (Γ · R1).
Proof.
  unshelve refine (exist3 _).
  + refine (fun α γr => R2.(q1) α γr.(fst)).
  + refine (fun γd => R2.(q2) γd.(fst)).
  + unshelve refine (fun α γ => _).
    exact (R2.(q3) α (¿ γ)).
Defined.

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


Definition Var {Γ : Ctx} (R : Ty Γ) : RElt (Γ · R) (⇑ R).
Proof.
  unshelve refine (exist3 _).
  + refine (fun α γr => γr.(snd)).
  + refine (fun γd => γd.(snd)).
  + exact (fun α γ => γ.(q3).(snd)). 
Defined.

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


Definition Weaken {Γ : Ctx} {R S : Ty Γ} (r : RElt Γ R) :
  RElt (Γ · S) (⇑ R).
Proof.
  unshelve refine (exist3 _).
  + refine (fun α γr => r.(q1) α γr.(fst)).
  + refine (fun γd => r.(q2) γd.(fst)).
  + exact (fun α γ => r.(q3) α (¿ γ)).
Defined.

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

Definition Sub {Γ : Ctx} {R : Ty Γ} (S : Ty (Γ · R)) (r : RElt Γ R) :
  Ty Γ.
Proof.
  unshelve refine (exist3 _).
  + refine (fun α γr => S.(q1) α (@exist _ _ γr (r.(q1) α γr))).
  + refine (fun γd => S.(q2) (@exist _ _ γd (r.(q2) γd))).
  + exact (fun α γ =>
           S.(q3) α (γ ·· (r ® γ))).
Defined.


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

         
Definition RPi {Γ : Ctx} (A : Ty Γ) (B : Ty (Γ ·  A)) : Ty Γ.
Proof.
  unshelve refine (exist3 _).
  - refine (fun α γr => forall (x : A.(q1) α γr), B.(q1) α (@exist _ _ γr x)).
  - intro γd.
    unshelve refine (exist _) ; simpl.
    + refine (forall (x : (A.(q2) γd).(fst)), (B.(q2) (@exist _ _ γd x)).(fst)).
    + refine (fun f x a => (B.(q2) (@exist _ _ γd a)).(snd) (fun y => f y a) x).
  - simpl ; unshelve refine (fun α γ => _).
    unshelve refine (exist _).
    have aux : 
    + exact  (fun fr fd => forall a : Ty_inst A γ,
            (B.(q3) α (γ ·· a)).(fst)
                                  (fr a.(q1))
                                  (fd a.(q2))).
(*    + exact (fun fr fd => forall a : RElt Γ A,
                 (B.(q3) α (γ ·· (a ® γ))).(fst)
                                             (fr (a ® γ).(q1))
                                             (fd (a ® γ).(q2))).*)
                                             
    + unshelve refine (fun _ _ _ fe a => (B.(q3) α (γ ·· a)).(snd) _ _ _ _).
      exact (fe a). 
Defined.


Notation "∏" := (RPi).

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


Definition RLam {Γ : Ctx} {A : Ty Γ} (B : Ty (Γ · A)) (f : RElt (Γ · A) B)
  : RElt Γ (RPi A B).
Proof.
  unshelve refine (exist3 _).
  + refine (fun α γr xr => f.(q1) α (@exist _ _ γr xr)).
  + refine (fun γd xd => f.(q2) (@exist _ _ γd xd)).
  + exact (fun α γ x => f.(q3) α (γ ·· x)).
Defined.


Notation "'λ'" := RLam.

Definition RLamN {Γ : Ctx} {A : Ty Γ} {B : Ty Γ} (f : RElt (Γ · A) (⇑ B)) : RElt Γ (A → B) :=
  @RLam Γ A (⇑ B) f.

Definition RApp {Γ : Ctx} {A : Ty Γ} {B : Ty (Γ · A)}
           (f : RElt Γ (RPi A B)) (x : RElt Γ A) : RElt Γ (B {{ x }}).
Proof.
  unshelve refine (exist3 _).
  + refine (fun α γr => f.(q1) α γr (x.(q1) α γr)).
  + refine (fun γd => f.(q2) γd (x.(q2) γd)).
  + exact (fun α γ =>
           f.(q3) α γ (x ® γ)).
Defined.

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

Definition RAppN {Γ : Ctx} {A : Ty Γ} {B : Ty Γ} (f : RElt Γ (A → B))(x : RElt Γ A) : RElt Γ B :=
  @RApp Γ A (⇑ B) f x.

Notation "t ◊ u" := (@RAppN _ _ _ t u) (at level 12, left associativity).


Definition U {Γ : Ctx} : Ty Γ.
Proof.
  unshelve refine (exist3 _).
  - refine (fun α γr => Type).
  - unshelve refine (fun γd => exist _).
    + refine (BranchingTYPE X Y).
    + refine (fun _ _ => Bunit X Y).
  - unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
    + unshelve refine (fun A B => @tsig (A -> B.(fst) -> Type) _).
      * exact (fun Te => forall (a : A) (f : Y -> B.(fst)) (x : X) (fe : Te a (f (α x))),
                Te a ((B.(snd) f x))).
    + intros A f x fe.
      unshelve refine (exist _).
      * exact (fun _ _ => unit).
      * simpl.
        exact (fun _ _ _ _ => tt).
Defined.


Definition REL {Γ : Ctx} (A : RElt Γ U) : Ty Γ.
Proof.
  exists (fun p γ => A.(q1) p γ) (fun γ => A.(q2) γ).
  unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
  - exact (A.(q3) α γ).(fst).
  - exact (A.(q3) α γ).(snd).
Defined.

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

Definition RElt_inst {Γ : Ctx} {α : ℙ} {γ : Γ ‡ α}
           (R : Ty_inst U γ) : Type :=
    triple (fun (a : R.(q1)) (b : R.(q2).(fst)) =>
                R.(q3).(fst) a b).


Definition RProp {Γ : Ctx} : Ty Γ.
Proof.
  unshelve refine (exist3 _).
  - refine (fun α γr => Prop).
  - intro γd.
    unshelve refine (exist _).
    + refine ({P : Prop & (Y -> P) -> X -> P}).
    + refine (fun _ _ => _).
      refine (@exist _ _ True _).
      refine (fun _ _ => I).
  - unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
    + exact (fun A B => tsig (fun (Te : A -> B.(fst) -> Type) =>
              forall (a : A) (f : Y -> B.(fst) ) (x : X) (fe : Te a (f (α x))),
                Te a ((B.(snd) f x)))).
    + simpl ; intros.
      unshelve refine (exist _).
      * exact (fun _ _ => True).
      * simpl.
        exact (fun _ _ _ _ => I).
Defined.



Definition REL_Prop {Γ : Ctx} (A : RElt Γ RProp) : Ty Γ.
Proof.
  unshelve refine (exist3 _).
  - unshelve refine (fun α γ => _).
    exact (A.(q1) α γ).
  - refine (fun γ => _).
    refine (exist _).
    apply (A.(q2) γ).(snd).
  - unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
    + exact (A.(q3) α γ).(fst).
    + exact (A.(q3) α γ).(snd).
Defined.


Inductive RParabool (α : X -> Y) :
  bool -> (BranchingBool X Y) -> Type :=
| RParatrue : RParabool α true (@Btrue_aux X Y)
| RParafalse : RParabool α false (@Bfalse_aux X Y)
| RParabêtabool : forall  (bo : bool) (f : (Y ->  BranchingBool X Y)) (x : X)
                        (rel : RParabool α bo (f (α x)) ),
    RParabool α bo (Bêtabool f x).

Definition Rbool {Γ : Ctx} : Ty Γ.
Proof.
  exists (@Abool X Y Γ.(q1)) (@Bbool X Y Γ.(q2)).
  exact (fun (α : ℙ) (γ : Γ ‡ α) => {| fst := RParabool α; snd := RParabêtabool α |}).
Defined.


Definition Rtrue {Γ : Ctx} : RElt Γ Rbool.
Proof.
  exists (@Atrue X Y Γ.(q1)) (@Btrue X Y Γ.(q2)).
  exact (fun α _ => RParatrue α).
Defined.


Definition Rfalse {Γ : Ctx} : RElt Γ Rbool.
Proof.
  exists (@Afalse X Y Γ.(q1)) (@Bfalse X Y Γ.(q2)).
  exact (fun α _ => RParafalse α).
Defined.

  
Definition Rbool_rec (Γ : Ctx) :
   RElt Γ (∏ U ([Var U] → [Var U] → Rbool → [Var U])).
Proof.
  exists (@Abool_rec X Y Γ.(q1)) (@Bbool_rec X Y Γ.(q2)).
  simpl ; intros α g P ptrue pfalse b.
  destruct b as [bo bb be].
  revert be ; revert  bb ; revert bo ; simpl.
  unshelve refine (fix f _ _ b := match b with
                              | RParatrue _ => _
                              | RParafalse _ => _
                              | RParabêtabool _ _ _ _ rel =>
                                P.(q3).(snd) _ _  _ (f _ _ rel)
                              end).
  - exact ptrue.(q3).
  - exact pfalse.(q3).
Defined.



Definition Rbool_stor {Γ : Ctx} :
  RElt Γ (Rbool → (Rbool → U) → U).
Proof.
  pose (r := RApp (Rbool_rec Γ) ((Rbool → U) → U)).
  let T := constr:(RElt Γ (((Rbool → U) → U) → ((Rbool → U) → U) → Rbool → ((Rbool → U) → U))) in
  unshelve refine (let r : T := r in _).
  unshelve refine (RAppN (RAppN r _) _).
  + refine (RLamN (@RAppN _ Rbool _ _ _)).
    - refine #.
    - refine Rtrue.
  + refine (RLamN (@RAppN _ Rbool _ _ _)).
    - refine #.
    - refine Rfalse.
Defined.

Definition Rbool_rect {Γ : Ctx} :
  RElt Γ (∏ (Rbool → U) (
    [@RApp (Γ · (Rbool → U)) Rbool U (Var (Rbool → U)) Rtrue] →
    [@RApp (Γ · (Rbool → U)) Rbool U # Rfalse] →
    ∏ Rbool [@RApp _  _ U
                   (@RApp (Γ · (Rbool → U) · Rbool) _ _ Rbool_stor #) (↑#)])).
Proof.
  unshelve refine (exist3 _).
  - refine (fun α γ P ptrue pfalse b =>
    match b with
    | true => ptrue
    | false => pfalse
    end).
  - unshelve refine (fun g P ptrue pfalse bb =>
              match bb with
              | Btrue_aux _ _ => ptrue
              | Bfalse_aux _ _ => pfalse
              | Bêtabool _ _ => tt
              end).
  - intros α γ P ptrue pfalse b.
    destruct b as [bo bb be].
    revert be ; revert  bb ; revert bo.
    unshelve refine (fun  _ _ b => match b with
                                   | RParatrue _ => _
                                   | RParafalse _ => _
                                   | RParabêtabool _ _ _ _ _ => tt
                              end).
    + now apply ptrue.
    + now apply pfalse.
Defined.


Inductive RParanat (α : X -> Y) : nat -> BranchingNat X Y -> Type :=
| RP0 : RParanat α 0 (B0 X Y)
| RPS : forall (no : nat) (nt :  BranchingNat X Y)
                     (ne : RParanat α no nt),
    RParanat α (S no) (BS nt)
| RPbêta : forall  (no : nat) (f : (Y ->  BranchingNat X Y)) (x : X)
                        (rel : RParanat α no (f (α x)) ),
    RParanat α no (Bêtanat f x).


Definition Rnat {Γ : Ctx} : Ty Γ.
Proof.
  unshelve refine (exist3 _).
  - refine (fun (α : X -> Y) (γ : Γ.(q1) α) => nat ).
  - refine (Bnat X Y).
  - exact (fun α γ => exist (RPbêta α)).
Defined.

Definition R0 {Γ : Ctx} : RElt Γ Rnat.
Proof.
  exists (fun _ _ => 0) (fun _ => B0 X Y).
  now refine (fun α _ => RP0 α).
Defined.

Definition RS {Γ : Ctx} : RElt Γ (Rnat → Rnat).
Proof.
  exists (fun _ _ => S) (fun _ => @BS X Y).
  now refine (fun α _ n => RPS α n.(q1) n.(q2) n.(q3)).
Defined.


Lemma RParanat_equal {Γ : Ctx} (n : RElt Γ Rnat)
      (α : X -> Y) (γ : Γ ‡ α)  :
    BNdialogue (n ® γ).(q2) α = (n ® γ).(q1).
Proof.
  destruct n as [nt no ne] ; simpl.
  elim: (ne α γ) =>
  [ | β mt mo me | β f x mo rel] ; trivial ; simpl.
  exact: eq_S.
Qed.



Definition Rnat_rec (Γ : Ctx) :
   RElt Γ (∏ U ([Var U] → (Rnat → [Var U] → [Var U]) → Rnat → [Var U])).
Proof.
  unshelve refine (exist3 _).
  - simpl ; unshelve refine (fun α gamma P p0 pS => _).
    refine (fix f n := match n with
                       | 0 => p0
                       | S k => pS k (f k)
                       end).
  - simpl ; unshelve refine (fun gamma P p0 pS => _).
    refine (fix f n := match n with
                       | B0 _ _ => p0
                       | BS k => pS k (f k)
                       | Bêtanat g x => P.(snd) (fun y => f (g y)) x
                       end).
  - simpl.
    unshelve refine (fun α gamma P p0 pS n => _).
    cbv in P.
    unshelve refine (let fix g no nt ne :=
                         match ne as n in RParanat _ mo mt return
                                  fst (q3 P)
                                      ((fix f (n : nat) : q1 P :=
                                          match n with
                                          | 0 => q1 p0
                                          | S k => q1 pS k (f k)
                                          end) mo)
                                      ((fix f n : (q2 P).(fst) :=
                                          match n with
                                          | B0 _ _ => q2 p0
                                          | BS k => q2 pS k (f k)
                                          | Bêtanat g x => ((P.(q2)).(snd) (fun y => f (g y)) x)
                                          end) mt)                                     
                         with
                         | RP0 _ => p0.(q3)
                         | RPS _ ko kt ke => pS.(q3) (exist3 ke) (exist3 (g ko kt ke))
                         | RPbêta _ ko f x rel => P.(q3).(snd) _ _ _ (g ko (f (α x)) rel)
                         end
      in g n.(q1) n.(q2) n.(q3)).
Defined.      


Definition Rnat_stor {Γ : Ctx} :
  RElt Γ (Rnat → (Rnat → U) → U).
Proof.
  pose (r := RApp (Rnat_rec Γ) ((Rnat → U) → U)).
  let T := constr:(RElt Γ (((Rnat → U) → U) → (Rnat → ((Rnat → U) → U) → ((Rnat → U) → U)) → Rnat → ((Rnat → U) → U))) in
  unshelve refine (let r : T := r in _).
  unshelve refine (RAppN (RAppN r _) _).
  - refine (RLamN (@RAppN _ Rnat _ _ _)).
    + now refine #.
    + now refine R0.
  - refine (@RLamN _ _ _ _).
    refine (@RLamN (@Ctx_cons Γ Rnat) (⇑ ((Rnat → U) → U)) (⇑ ((Rnat → U) → U)) _).
    refine (@RLamN (Γ · Rnat · (⇑ ((Rnat → U) → U)))
                  (⇑(⇑(Rnat → U))) (⇑ (⇑ U)) _).
    refine (@RAppN _ (Rnat → U) _ _ _).
    + now refine (↑#).
    + apply RLamN.
      refine (@RAppN _ Rnat _ _ _).
      * now refine (↑#).
      * now refine (@RAppN _ Rnat _ RS (↑↑↑(Var Rnat))).
Defined.


Definition Rnat_rect {Γ : Ctx} :
  RElt Γ (∏ (Rnat → U) (
              [@RApp (Γ · (Rnat → U)) Rnat U # R0] →
              [∏ Rnat ([@RApp (Γ · (Rnat → U) · Rnat) _ U
                              (@RApp (Γ · (Rnat → U) · Rnat) _ _ Rnat_stor #) (↑#)] →
                       [@RApp (Γ · (Rnat → U) · Rnat) _ U
                              (@RApp (Γ · (Rnat → U) · Rnat) _ _ Rnat_stor
                                     (@RApp (Γ · (Rnat → U) · Rnat) _ _ RS #)) (↑#)])] →
              ∏ Rnat [@RApp (Γ · (Rnat → U) · Rnat) _ U
                            (@RApp (Γ · (Rnat → U) · Rnat) _ _ Rnat_stor #) (↑#)])).
Proof.
  unshelve refine (exist3 _).
  - cbv.
    unshelve refine (fun α γ P p0 pS => _).
    refine (fix g n := match n with
                                 | 0 => p0
                                 | S k => pS k (g k)
                                 end).
  - cbv.
    unshelve refine (fun γ P p0 pS => _).
    simpl.
    refine (fix g n :=
              match n with
              | B0 _ _ => p0
              | BS k => pS k (g k)
              | Bêtanat _ _ => tt
              end).
  - unshelve refine (fun α gamma P p0 pS n => _).
    destruct n as [ho ht he].
    revert he ; revert ho ; revert ht.
    cbv in pS.
    refine (fix g ht ho he :=
              match he with
              | RP0 _ => _
              | RPS _ no nt ne => pS.(q3) (exist3 ne) (exist3 (g nt no ne))
              | RPbêta _ _ _ _ _ => tt
              end).
    exact p0.(q3).
Defined.



Definition RApp_inst {Γ : Ctx} {α : ℙ} {γ : Γ ‡ α} {A : Ty Γ}
           {B : Ty (Γ · A)} (f : Ty_inst (RPi A B) γ) (x : Ty_inst A γ) :
  Ty_inst B (γ ·· x).
Proof.
  unshelve refine (exist3 _).
  - exact (f.(q1) x.(q1)).
  - exact (f.(q2) x.(q2)).
  - exact (f.(q3) x).
Defined.



Inductive Bsig (A : BranchingTYPE X Y)
          (B : A.(fst) -> BranchingTYPE X Y) : Type :=
| Bex : forall (a : A.(fst)) (b :  (B a).(fst)), Bsig A B
| Bêtasig : (Y -> Bsig A B) -> X -> Bsig A B.


Inductive RParasig {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α}
          (A : Ty_inst U γ) (B : Ty_inst ((Var U) → U) (γ ·· A))
  : tsig (B.(q1)) -> Bsig (A.(q2)) (B.(q2)) -> Type :=
| Paraex : forall (a : RElt_inst A) (b : RElt_inst (RApp_inst B a)),
    RParasig A B (@exist _ _ a.(q1) b.(q1)) (Bex A.(q2) B.(q2) a.(q2) b.(q2))
| Parabêtasig : forall (ba : tsig B.(q1)) (f : Y -> Bsig A.(q2) B.(q2))
                       (x : X) (rel : RParasig A B ba (f (α x))),
    RParasig A B ba (Bêtasig A.(q2) B.(q2) f x).

Definition Rsig {Γ : Ctx} : RElt Γ (∏ U (((Var U) → U) → U)).
Proof.
  unshelve refine (exist3 _). 
  - cbv.
    intros alpha gamma A B.
    exact (tsig B). 
  - unshelve refine (fun gamma A B => exist _).
    + refine (Bsig A B).
    + exact (Bêtasig A B).
  - unshelve refine (fun alpha gamma  A B => exist _). 
    + exact (RParasig A B).
    + exact (Parabêtasig A B).
Defined.      

Arguments nil {A}.
Notation "x :: l" := (cons x l).


Definition Ty' (α : X -> Y) :=
  triple
    (fun (a : Type) (b : {A : Type & (Y -> A) -> X -> A}) =>
       {Te : a -> fst b -> Type &
                           forall (a0 : a) (f : Y -> fst b) (x : X),
                             Te a0 (f (α x)) -> Te a0 (snd b f x)}).


Definition RElt' {α : X -> Y} (R : Ty' α) :=
  triple (fun (a : q1 R) (b : fst (q2 R)) => fst (q3 R) a b).

Inductive RParalist {α : X -> Y} (A : Ty' α)
  : list A.(q1) -> (@BranchingList X Y A.(q2)) -> Type :=
| RParanil : RParalist A nil (@Bnil_aux X Y _)
| RParacons : forall (la : list A.(q1)) (lb :  @BranchingList X Y A.(q2))
                     (le : RParalist A la lb)
                     (x : RElt' A),
    RParalist A (x.(q1) :: la) (Bcons_aux x.(q2) lb)
| RParabêtalist : forall (la : list A.(q1))
                         (f : Y -> (@BranchingList X Y A.(q2)))
                         (x : X)
                         (rel : RParalist A la (f (α x))),
    RParalist A la (Bêtalist f x).


Definition Rlist {Γ : Ctx} : RElt Γ (U → U).
Proof.
  unshelve refine (exist3 _).
  - exact (fun alpha gamma A => list A).
  - exact (@Blist X Y Γ.(q2)).
  - unshelve refine (fun alpha gamma A => exist _).    
    + exact (RParalist A).
    + exact (RParabêtalist A).
Defined.


Definition Rnil {Γ : Ctx} : RElt Γ  (∏ U (Rlist • (Var U))). 
Proof.
  unshelve refine (exist3 _).
  - exact (fun _ _ =>  @nil).
  - exact (@Bnil X Y Γ.(q2)).
  - exact (fun alpha gamma _ => RParanil _).
Defined.


Definition Rcons {Γ : Ctx} :
  RElt Γ (∏ U ((Var U) → [RApp Rlist (Var U)] → [RApp Rlist (Var U)])).
Proof.
  unshelve refine (exist3 _).
  - exact (fun alpha gamma A a l => cons a l).
  - exact (@Bcons X Y Γ.(q2)).
  - now cbv ; refine (fun alpha gamma A a l => RParacons A l.(q1) l.(q2) l.(q3) a).
Defined.

(*Non-dependent eliminator for lists*)
Definition Rlist_rec (Γ : Ctx) :
  @RElt Γ (∏ U
            (∏ U
               ([Var U] →
                ([↑(Var U)] → Rlist • ↑ (Var U) → [Var U] → [Var U]) →
                Rlist • ↑ (Var U) →
                [Var U]))).
Proof.
  unshelve refine (exist3 _).
  - exact (@Alist_rec X Y Γ.(q1)).
  - exact (@Blist_rec X Y Γ.(q2)).
  - cbv.
    unshelve refine (fun α gamma R P pnil pcons l => _).
    refine (let fix f la lb le {struct le} :=
                match le as le0 in RParalist _ la0 lb0
                      return
                      fst (q3 P)
                          ((fix g (la : list (q1 R)) : q1 P :=
                              match la with
                              | nil => q1 pnil
                              | (x :: q) => q1 pcons x q (g q)
                              end) la0)
                          ((fix g (lb : BranchingList (Y:=Y)) : fst (q2 P) :=
                              match lb with
                              | @Bnil_aux _ _ => q2 pnil
                              | Bcons_aux x q => q2 pcons x q (g q)
                              | Bêtalist h x => snd (q2 P) (fun y : Y => g (h y)) x
                              end) lb0)
                with
                | RParanil _ => pnil.(q3)
                | RParacons _ qa qb qe x => pcons.(q3) x (exist3 qe) (exist3 (f qa qb qe))
                | RParabêtalist _ qa g x rel => P.(q3).(snd) _ _ _ (f qa (g (α x)) rel)
                end in f l.(q1) l.(q2) l.(q3)).
Defined.

Definition Runit {Γ : Ctx } : Ty Γ.
Proof.
  unshelve refine (exist3 _).
  - exact (fun _ _ => unit).
  - exact (fun _ => @Bunit X Y).
  - unshelve refine (fun _ _ => exist _).
    + exact (fun _ _ => unit).
    + exact (fun _ _ _ _ => tt).
Defined.


    (*Storage operator for lists*)
Definition Rlist_stor{Γ : Ctx } :
  RElt Γ (∏ U (Rlist • (Var U) → (Rlist • (Var U) → U) → U)).
Proof.
    let T1 := constr: (∏ (@U (Γ · U · U)) ([(Var U)] →
                                   ([↑ (Var U)] → Rlist • (↑  (Var U)) → [(Var U)] → [(Var U)]) →
                                               Rlist • (↑(Var U)) →
                                               [(Var U)])) in
  let T := constr: ((@Var (Γ · U) U ) → (([↑ (Var U)] → Rlist • ↑ (Var U) → [Var U] → [Var U]) → Rlist • ↑ (Var U) → [Var U])) in
  pose (r := @RApp (Γ · U) U T (@RApp (Γ · U) U T1 ((@Rlist_rec _)) [@Var Γ U]) ((((@Rlist (Γ · U)) • (@Var Γ U)) → (@U (Γ · U))) → (@U (Γ · U)))).
  let T := constr: (@RElt (Γ · U) ((((Rlist • (Var U)) → U) → U) → ([Var U] → (Rlist • (Var U)) → (((Rlist • (Var U)) → U) → U) → (((Rlist • (Var U)) → U) → U)) → (Rlist • (Var U)) → (((Rlist • (Var U)) → U) → U))) in
  unshelve refine (let r : T := r in _).
  unshelve refine (RLam _ _).
  unshelve refine (RApp (RApp r _) _).
  - unshelve refine (@RLam _ (Rlist • (Var U) → U) _ _).
    unshelve refine (@RAppN _ (Rlist • ↑ (Var U)) (⇑ U) _ _).
    + now refine (@Var _ _).
    + now refine (Rnil • ↑(Var U)).
  - refine (@RLamN _ _ _ _).
    refine (@RLamN _ (⇑ (Rlist • (Var U)))
                   (⇑ (((Rlist • (Var U) → U) → U) → ((Rlist • (Var U) → U) → U))) _).
    refine (@RLamN _ (⇑ ⇑ ((Rlist • (Var U) → U) → U)) (⇑ ⇑ ((Rlist • (Var U) → U) → U)) _).
    refine (@RLamN _ (⇑ ⇑ ⇑ ((Rlist • (Var U) → U))) (⇑ ⇑ ⇑ U) _).
    refine (@RApp _ ((Rlist • ↑ ↑ ↑ ↑ (Var U)) → U) (⇑ (⇑ (⇑ (⇑ U)))) _ _).
    + now refine (↑#).
    + apply RLamN.
      refine (@RAppN _ (Rlist • ↑ ↑ ↑ ↑ ↑ (Var U)) _ _ _).
      * now refine (↑#).
      * refine (@RAppN _ (Rlist • ↑ ↑ ↑ ↑ ↑ (Var U)) _ _ _).
        refine (@RAppN _ [↑ ↑ ↑ ↑ ↑ (Var U)] _ _ _).
        refine (Rcons • (↑ ↑ ↑ ↑ ↑ (Var U))).
        refine (↑ ↑ ↑ ↑  #).
        exact #.
Defined.


(*Restricted dependent-eliminator for lists.*)

Definition Rlist_rect {Γ : Ctx} :
  @RElt Γ (∏ U
            (∏ ((Rlist • (Var U)) → U)
               ((@RAppN (Γ · U · ((Rlist • (Var U)) → U))
                        (⇑(Rlist • ((Var U)))) U # (Rnil • (↑(Var U)))) →
                 (∏ [↑(@Var _ U)]
                    (∏ (Rlist • (↑↑(@Var _ U)))
                       (([(@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (↑#) · (Rlist • (↑↑(@Var _ U))))
                                  ((Rlist • (↑ ↑ ↑(Var U))))
                                  (((Rlist • (↑ ↑ ↑(Var U))) → U) → U)
                                  (Rlist_stor • (↑↑↑(@Var _ U)))
                            (@Var _ ((Rlist • (↑↑(Var U))))))
                            ◊ (↑↑(@Var _ ((Rlist • (Var U)) → U)))]) →
                        ([(@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (↑#) · (Rlist • (↑↑(@Var _ U))))
                                  ((Rlist • (↑ ↑ ↑(Var U))))
                                  (((Rlist • (↑ ↑ ↑(Var U))) → U) → U)                                  (Rlist_stor • (↑↑↑(@Var _ U)))
                                  ((@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (↑#) · (Rlist • (↑↑(@Var _ U))))
                                           (↑ ↑ ↑(Var U))
                                           ((Rlist • (↑ ↑ ↑ (Var U))) → (Rlist • (↑ ↑ ↑ (Var U))))
                                           (Rcons • (↑↑↑(@Var _ U))) (↑#)) ◊ #))
                            ◊ (↑↑(@Var _ ((Rlist • (Var U)) → U)))])))) →
                 ∏ (Rlist • ↑(Var U))
                   [(@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (Rlist • ↑(Var U)))
                            ((Rlist • (↑ ↑ (Var U))))
                            (((Rlist • (↑ ↑(Var U))) → U) → U) 
                            (Rlist_stor • (↑↑(@Var _ U))) #) ◊ (↑#)]))).
Proof.
  unshelve refine (exist3 _).
  - exact (@Alist_rect X Y Γ.(q1)).
  - exact (@Blist_rect X Y Γ.(q2)).
  - refine (fun α gamma A P pnil pcons l => _).
    lazy in l.
    destruct l as [la lb le].
    unfold Alist_rect ; unfold Blist_rect.
    induction le.
    + exact pnil.(q3).
    + simpl in pcons.
      vm_compute.
      unshelve refine (pcons.(q3) x (exist3 le) _).

    refine (let fix f la lb le :=
                match le
                with
                | RParanil _ => _
                | RParacons _ qa qb qe x => _
                | RParabêtalist _ qa g x rel => _
                end
            in f la lb le).
    +  exact (pnil.(q3)).
                
    
    induction le.
    + exact pnil.(q3).
    + refine (pcons.(q3) x (exist3 le) _).
      
  :=
  fun _ B P pnil pcons =>
    fix f l := match l as l0 return
                     ((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
                         match l with
                         | Bnil_aux => fun P => P (Bnil_aux)
                         | Bcons_aux x q =>
                           fun P =>
                             g q (fun l' => P (Bcons_aux x l'))
                         | Bêtalist g x => fun P => Bunit
                         end) l0 P).(fst)
               with
               | Bnil_aux => pnil
               | Bcons_aux x q => pcons x q (f q)
               | Bêtalist _ _ => tt
               end.
Proof.
  unshelve refine (fun gamma B P pnil pcons => _).
  refine (fix f l := match l as l0 return
                           ((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
                              match l with
                              | Bnil_aux => fun P => P (Bnil_aux)
                              | Bcons_aux x q =>
                                fun P =>
                                  g q (fun l' => P (Bcons_aux x l'))
                              | Bêtalist g x => fun P => Bunit
                              end) l0 P).(fst)
                     with
                     | Bnil_aux => pnil
                     | Bcons_aux x q => pcons x q (f q)
                     | Bêtalist _ _ => tt
                     end).*)








Inductive Eq {A : Type} (x : A) : A -> Type :=  Eq_refl : Eq x x.
                                                                
Inductive Beq (A : BranchingTYPE X Y) (a : A.(fst)) : A.(fst) -> Type :=
| Beq_refl : Beq A a a
| Bêtaeq : forall (b : A.(fst)), (Y -> Beq A a b) -> X -> Beq A a b.

Inductive RParaeq {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α} (A : Ty_inst U γ) (a : RElt_inst A) :
  forall (b : RElt_inst A),
  (Eq a.(q1) b.(q1)) -> (Beq A.(q2) a.(q2) b.(q2)) -> Type :=
| RParaeq_refl : RParaeq A a a (Eq_refl a.(q1)) (Beq_refl A.(q2) a.(q2))
| RParabêtaeq : forall (b : RElt_inst A) (e : Eq a.(q1) b.(q1))
                       (f : Y -> Beq A.(q2) a.(q2) b.(q2)) (x : X)
                       (rel : RParaeq A a b e (f (α x))),
    RParaeq A a b e (Bêtaeq A.(q2) a.(q2) b.(q2) f x).


Definition Req {Γ : Ctx} : RElt Γ (∏ U ((Var U) → (Var U) → U)).
Proof.
  unshelve refine (exist3 _).
  - exact (fun alpha gamma => @Eq).
  - unshelve refine (fun gamma A a b => exist _).
    + exact (Beq A a b).
    + exact (Bêtaeq A a b).
  - unshelve refine (fun alpha gamma A a b => exist _).
    + exact (RParaeq A a b).
    + exact (RParabêtaeq A a b).
Defined.

Print Rcons.
(*
Inductive AEqFin {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α} :
  (Ty_inst Rnat γ -> nat) -> Ty_inst [RApp Rlist Rnat] γ -> (Ty_inst Rnat γ -> nat) -> Type :=
| AEqnil : forall (f g : (Ty_inst Rnat γ -> nat)), AEqFin f (Rnil ® γ) g
| AEqcons : forall (f g : (Ty_inst Rnat γ -> nat))
                       (l : Ty_inst [RApp Rlist Rnat] γ)
                       (n : Ty_inst Rnat γ),
    (f n = g n) -> (AEqFin f l g) -> (AEqFin f (Rcons n l) g).*)

Inductive AEqFin : (nat -> nat) -> list nat -> (nat -> nat) -> Type :=
    AEqnil : forall alpha bêta : nat -> nat, AEqFin alpha nil bêta
  | AEqcons : forall (alpha bêta : nat -> nat) (l : list nat) (x : nat),
             Eq (alpha x)  (bêta x) ->
             AEqFin alpha l bêta -> AEqFin alpha (x :: l) bêta.

Definition Bnat' : BranchingTYPE X Y :=
  {| fst := BranchingNat X Y ; snd := @Bêtanat X Y |}.
Print Bcons_aux.
Inductive BEqFin : (BranchingNat X Y -> BranchingNat X Y) ->
                   (@BranchingList X Y Bnat') ->
                   (BranchingNat X Y -> BranchingNat X Y) ->
                   Type :=
| BEqnil : forall (f g : BranchingNat X Y -> BranchingNat X Y),
    BEqFin f (@Bnil_aux X Y Bnat') g
| BEqcons : forall (f g : BranchingNat X Y -> BranchingNat X Y)
                   (l : (@BranchingList X Y Bnat'))
                   (n : Bnat'.(fst)),
    (Beq Bnat' (f n) (g n)) -> (BEqFin f l g) -> (BEqFin f (Bcons_aux n l) g)
| BêtaEqFin : forall (f g : BranchingNat X Y -> BranchingNat X Y)
                     (l : (@BranchingList X Y Bnat'))
                     (h : Y -> BEqFin f l g) (x : X),
    BEqFin f l g.



Definition Rnil_nat {Γ : Ctx} : RElt Γ (([RApp Rlist Rnat])).
Proof.
  unshelve refine (exist3 _).
  - exact (fun _ _  => @nil nat).
  - exact (fun _ => @Bnil_aux X Y _).
  - exact (fun _ _ => RParanil _).
Defined.

  
Definition Rcons_nat {Γ : Ctx} : RElt Γ (Rnat → ([RApp Rlist Rnat] → [RApp Rlist Rnat])).
Proof.
  unshelve refine (exist3 _).
  - exact (fun _ _ => @cons nat).
  - exact (fun _ => @Bcons_aux X Y _).
  - exact (fun _ _ n l => RParacons _ _ _ l.(q3) _).
Defined.


Inductive RParaEqFin {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α} :
  forall (f : Ty_inst [Rnat → Rnat] γ) (l : Ty_inst [RApp Rlist Rnat] γ)
         (g : Ty_inst [Rnat → Rnat] γ),
    AEqFin f.(q1) l.(q1) g.(q1) -> BEqFin f.(q2) l.(q2) g.(q2) -> Type :=
| RParaEqnil : forall (f g : Ty_inst [Rnat → Rnat] γ),
    RParaEqFin f (Rnil_nat ® γ) g (AEqnil f.(q1) g.(q1)) (BEqnil f.(q2) g.(q2))
| RParaEqcons : forall (f g : Ty_inst [Rnat → Rnat] γ)
                       (l : Ty_inst [RApp Rlist Rnat] γ)
                       (n : Ty_inst Rnat γ)
                       (i : AEqFin f.(q1) l.(q1) g.(q1))
                       (j : BEqFin f.(q2) l.(q2) g.(q2))
                       (k : RElt_inst (@RApp_inst Γ α _ Rnat (⇑U)
                                                  (@RApp_inst Γ α γ Rnat ((Rnat → U))
                                                              ((@RApp Γ U ((Var U) → (Var U) → U) Req Rnat) ® γ) (RApp_inst f n))
                                                  (RApp_inst g n))),
    RParaEqFin f l g i j ->
    RParaEqFin f (RApp_inst (RApp_inst (Rcons_nat ® γ) n) l) g
               (AEqcons f.(q1) g.(q1) l.(q1) n.(q1) k.(q1) i)
               (BEqcons f.(q2) g.(q2) l.(q2) n.(q2) k.(q2) j)
| RParabêtaEqFin : forall (f g : Ty_inst [Rnat → Rnat] γ)
                       (l : Ty_inst [RApp Rlist Rnat] γ)
                       (i : AEqFin f.(q1) l.(q1) g.(q1))
                       (h : Y -> BEqFin f.(q2) l.(q2) g.(q2)) (x : X)
                       (rel : RParaEqFin f l g i (h (α x))),
    RParaEqFin f l g i (BêtaEqFin f.(q2) g.(q2) l.(q2) h x). 


Definition REqFin  {Γ : Ctx} :
  RElt Γ ((Rnat → Rnat) →
            [RApp Rlist Rnat] →
               (Rnat → Rnat) → U).
Proof.
  unshelve refine (exist3 _).
  - exact (fun alpha gamma f l g => AEqFin f l g).
  - unshelve refine (fun gamma f l g => exist _).
    + exact (BEqFin f l g).
    + exact (BêtaEqFin f g l).
  - unshelve refine (fun alpha gamma f l g => exist _).
    + exact (RParaEqFin f l g).
    + exact (RParabêtaEqFin f g l).
Defined.

Definition Acontinuous (f : (nat -> nat) -> nat) (u : nat -> nat) :=
  {l : list nat & forall v : nat -> nat, AEqFin u l v -> f u = f v}.

Definition Bcontinuous (f : ((Bnat').(fst) -> (Bnat').(fst)) -> (Bnat').(fst))
           (u : (Bnat').(fst) -> (Bnat').(fst)) : BranchingTYPE X Y.
Proof.
  unshelve refine (exist _).
  unshelve refine (Bsig _ _).
  - unshelve refine (exist _).
    + exact (@BranchingList X Y Bnat').
    + exact (@Bêtalist X Y _).
  - unshelve refine (fun l => exist _).
    + refine (forall v : (BranchingNat X Y) -> (BranchingNat X Y), BEqFin u l v -> Beq _ (f u) (f v)).
    + exact (fun h e v rel => Bêtaeq _ (f u) (f v) (fun y => h y v rel) e).
  - exact (Bêtasig _ _).
Defined.


(*Definition Rcontinuous {Γ : Ctx} :
  RElt Γ (((Rnat → Rnat) → Rnat) →
          (Rnat → Rnat) → U).
Proof.
  (*unshelve refine (exist3 _).
  - unshelve refine (fun alpha gamma f u => _).
    refine ({l : list nat & forall v : nat -> nat, AEqFin u l v -> f u = f v}).
  - unshelve refine (fun gamma f u => exist _).
    + unshelve refine (Bsig (@Blist X Y (@Bnat X Y)) _).
      unshelve refine (fun l => exist _).
      * refine (forall v : (BranchingNat X Y) -> (BranchingNat X Y), BEqFin u l v -> Beq _ (f u) (f v)).
      * exact (fun h e v rel => Bêtaeq _ (f u) (f v) (fun y => h y v rel) e).
    + simpl.
      unshelve refine (Bêtasig _ _).
  - unshelve refine (fun alpha gamma f u => exist _).
    + simpl.
      intros acont bcont.
      refine ({l : BEl (@Blist X Y (@Bnat X Y)) & forall v : (BranchingNat X Y) -> (BranchingNat X Y), BEqFin u l v -> f u = f v}).
    + unshelve refine (fun h e => exist _).
      * refine (Bêtalist (fun y => (h y).(fst)) e).
      * intros v rel.
        have aux := (BêtaEqFin u v (Bêtalist (fun y : Y => fst (h y)) e) _ e).
        exact (BêtaEqFin u v (Bêtalist (fun y : Y => fst (h y)) e) _ e).*)
        
  refine (RLamN _).
  refine (@RLamN (@Ctx_cons Γ ((Rnat → Rnat) → Rnat)) (⇑ ((Rnat → Rnat))) (⇑ U) _).
  refine (@RAppN _ ((@RApp (Γ · ((Rnat → Rnat) → Rnat) · ⇑ (Rnat → Rnat)) _ _ Rlist Rnat) → U) U _ _).
  refine (@RApp _  _ _ Rsig (RApp Rlist Rnat)).
  refine (@RLamN _ _ _ _).
  unshelve refine (RPi (Rnat → Rnat) _).
  unshelve refine (RPi _ _).
  refine (@RAppN _ (Rnat → Rnat) U _ ((Var (Rnat → Rnat)))).
  refine (@RAppN _ (⇑ ⇑(@RApp (Γ · ((Rnat → Rnat) → Rnat) · ⇑ (Rnat → Rnat)) _ _ Rlist Rnat)) ((Rnat → Rnat) → U) _ (↑ (Var (@RApp (Γ · ((Rnat → Rnat) → Rnat) · ⇑ (Rnat → Rnat)) _ _ Rlist Rnat)))).
  refine (@RAppN _ (Rnat → Rnat) (⇑ (⇑ (Rlist • Rnat)) → (Rnat → Rnat) → U) _ (↑↑(Var (Rnat → Rnat)))).
  refine (↑ ↑ REqFin).
  refine (REL _).
  refine (@RAppN _ Rnat U _ _).
  refine (@RAppN _ Rnat (Rnat → U) _ _).
  refine (RApp Req Rnat).
  unshelve refine (@RAppN _ ((Rnat → Rnat)) Rnat _ _).
  - refine (↑ ↑ ↑ ↑ (Var  ((Rnat → Rnat) → Rnat))). 
  - refine (↑ ↑ ↑ (Var (Rnat → Rnat))).
  - unshelve refine (@RAppN _ ((Rnat → Rnat)) Rnat _ _).
    + refine (↑ ↑ ↑ ↑ (Var  ((Rnat → Rnat) → Rnat))).
    + refine (↑ (Var (Rnat → Rnat))).
Defined.

Definition inj1 {Γ : Ctx} (n : nat) : RElt Γ Rnat.
Proof.
  induction n.
  - exact R0.
  - exact (RApp RS IHn).
Defined.
    
Definition inj2 {Γ : Ctx} (u : nat -> nat) : RElt Γ (Rnat → Rnat).
Proof.
  unshelve refine (exist3 _).
  - exact (fun _ _ => u).
  - unshelve refine (fun gamma n => _).
    refine (let fix f v n := match n with
                         | B0 _ _ => BNEta _ _ (v 0)
                         | BS m => f (fun k => v (S k)) m
                         | Bêtanat h x => Bêtanat (fun y => f v (h y)) x
                         end in f u n).
  - unshelve refine (fun alpha gamma n => _).
    simpl.
    destruct n as [na nb ne].
    revert u.
    elim: ne.
    + intro u ; simpl.
      induction (u 0).
      * exact (RP0 alpha).
      * simpl.
        exact (RPS alpha _ _ IHn).
    + simpl.
      intros ma mb me ihme u.
      exact (ihme (fun k => u (S k))).
    + simpl ; intros ma h x rel ih u.
      exact (RPbêta alpha _ _ _ (ih u)).
Defined.*)
      
End AvareXY.



Section Avarenat.

Notation " Γ ‡ α " := (Ctx_El nat nat Γ α) (at level 11).
Notation "r ® γ" := (Inst nat nat r γ) (at level 10, left associativity).
Notation "()" := (ctx_nil nat nat).
Notation "Γ · A" := (Ctx_cons nat nat Γ A) (at level 50, left associativity).
Notation "γ ·· x" := (ctx_cons nat nat γ x) (at level 50, left associativity).
Notation "¿ g" := (Ctx_tl nat nat g) (at level 10).
Notation "⇑ A" := (Lift nat nat A) (at level 10).
Notation "#" := (Var nat nat _) (at level 0).
Notation "↑ M" := (Weaken nat nat M) (at level 10).
Notation "S {{ r }} " := (Sub nat nat S r) (at level 20, left associativity).
Notation "∏" := (RPi nat nat).
Notation "A → B" := (RPi nat nat A (⇑ B)) (at level 99, right associativity, B at level 200).
Notation "'λ'" := (RLam nat nat).
Notation "t • u" := (RApp nat nat t u) (at level 12, left associativity).
Notation "'Ctx'" := (Ctx nat nat).
Notation "'RElt'" := (RElt nat nat).
Notation "'Rnat'" := (@Rnat nat nat).

Definition inj3 {Γ : Ctx} (f : (nat -> nat) -> nat) (alpha : nat -> nat) (γ : Γ ‡ alpha) :
  (forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v) ->
  (Ty_inst nat nat ((Rnat → Rnat) → Rnat) γ).
Proof.
  intro hyp.
  unshelve refine (exist3 _).
  - exact f.
  - simpl ; unshelve refine (fun u => _).
    refine (BNEta nat nat _).
    exact ((f (fun n => BNdialogue (u (BNEta _ _ n)) alpha))).
  - simpl.
    intro v.
    have aux : forall m : nat, RParanat nat nat alpha m (BNEta _ _ m).
    + induction m.
      * exact (RP0 nat nat alpha).
      * exact (RPS nat nat alpha m _ IHm).
    + have aux2 : f (q1 v) = f (fun n : nat => BNdialogue (q2 v (BNEta nat nat n)) alpha).
      * refine (hyp (q1 v) (fun n : nat => BNdialogue (q2 v (BNEta nat nat n)) alpha) _).
      destruct v as [va vb ve].
      simpl.
      cbv in ve.
      intro n.
      specialize ve with (exist3 (aux n)) ; simpl in ve.
      elim: ve ; trivial ; simpl.
      intros ma mb me ; exact: eq_S.
      * rewrite - aux2.
      exact (aux (f (q1 v))).
Defined.

(*Theorem cont_imp_cont (f : (nat -> nat) -> nat)
        (ext : forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v)
        (cont : RElt (Ctx_nil nat nat) (∏ ((Rnat → Rnat) → Rnat)
                                          (∏ (Rnat → Rnat) ((Rcontinuous nat nat • (↑(Var nat nat ((Rnat → Rnat) → Rnat)))) • (Var nat nat (Rnat → Rnat)))))) :
  forall (alpha : nat -> nat), continuous f alpha.
Proof.
  intro alpha.
  have aux : {l : list nat & forall v : nat -> nat, AEqFin alpha l v -> Eq (f alpha) (f v)}.
  exact (cont.(q1) alpha tt f alpha).
  cbv in t.
  exact t.
  destruct cont as [conta contb conte].
  cbv.
  cbv in conta.
  exact (conta alpha tt f alpha).*)
  
Definition RGeneric {Γ : Ctx} : RElt Γ (Rnat → Rnat).
Proof.
  exists  (fun α gamma => α) (fun gamma => Generic_aux 0).
  intros α gamma n.
  destruct n as [no nt ne] ; simpl.
  unshelve refine (let aux :  forall (k : nat),
      RParanat _ _ α (α (k + no)) (Generic_aux k nt) := _ in _).
  - revert ne ; revert no ; revert nt.
    unshelve refine (fix f nt no ne k {struct ne}:= match ne with
                                   | RP0 _ _ _ => RPbêta nat nat _ _ _ _ _
                                   | RPS _ _ _ _ _ _ => _
                                   | RPbêta _ _ _ _ _ _ _ => _
                                   end).
    + rewrite - plus_n_O.
      refine (let fix g n := match n as n0
                                   return (RParanat nat nat α n0 (BNEta nat nat (n0)))
                             with
                             | 0 =>  (RP0 _ _ α)
                             | S k => RPS nat nat α k (BNEta nat nat k) (g k)
                             end
              in g (α k)).
    + rewrite - plus_n_Sm ; rewrite - plus_Sn_m.
      exact (f b n r (S k)).
    + simpl. apply RPbêta. now apply (f (b (α n0)) n r k) .
  - exact: (aux 0).
Defined.      
Print RParanat_equal.

Lemma NaturRadinPGeneric {Γ : Ctx} {α : nat -> nat} (n : RElt Γ Rnat)
  (γ : Γ ‡ α):
  BNdialogue ((RGeneric • n) ® γ).(q2) α = α (n ® γ).(q1). 
Proof.
  destruct n as [no nt ne] ; simpl.
  have aux : forall (k : nat),
      BNdialogue (Generic_aux k (nt (q2 γ))) α = α (k + (no α (q1 γ))).
  - elim: (ne α γ) ; simpl.
    + intros k ; now rewrite NaturBNEtaDialogue ; rewrite - plus_n_O.
    + intros mt mo me ihme k.
      rewrite - plus_n_Sm ; rewrite - plus_Sn_m.
      exact: ihme.
    + intros f x mo me ihme k.
      now specialize ihme with k.
  - exact: aux.
Qed.


Theorem continuity (f : RElt (Ctx_nil nat nat) ((Rnat → Rnat) → Rnat)) (α : nat -> nat) :
  continuous (fun p => f.(q1) p ().(q1) p) α.
Proof.
  pose proof (@RParanat_equal nat nat (Ctx_nil nat nat) (f • RGeneric)) as Eq.
  destruct (BNDialogue_Continuity (f.(q2) (@ctx_nil nat nat α).(q1) (Generic_aux 0)) α)
    as [l ihl].
  exists l ; intros β Finite_Eq.
  simpl in Eq ; rewrite - (Eq α () ) ; rewrite - (Eq β () ).
  exact: ihl.
Qed.  

Arguments nil {A}.
Notation "x :: l" := (cons x l).
Fixpoint upton (n : nat) : list nat :=
  match n with
  | 0 => (0 :: nil)
  | S k => (S k :: (upton k))
  end.

(*Definition uptocontinuous (f : (nat -> nat) -> nat) (alpha : nat -> nat) :=
  {n : nat & forall bêta : nat -> nat, EqFin alpha (upton n) bêta -> f alpha = f bêta}.

Lemma Inconsistency (P : forall (f : (nat -> nat) -> nat)
                                (ext : forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v), forall (alpha : nat -> nat), uptocontinuous f alpha) :
  False.
Proof.
  pose M := P _ _ (fun _ => 0).
  pose m := M (fun _ => 0) (fun _ _ _ => eq_refl).
  Print f_equal.
  pose aux : forall beta : nat -> nat,
      (forall u v : nat -> nat,
          (forall n : nat, u n = v n) -> beta (u m.(fst)) = beta (v m.(fst))) :=
    fun bêta u v hyp => f_equal bêta (hyp m.(fst)).
  - pose f := fun beta => M (fun alpha => beta (alpha m.(fst))) (aux _).
    have aux2 :forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> (f u).(fst) = (f v).(fst).
    + intros u v hyp.
      unfold f.
      unfold aux.
      

      unfold f.
    unfold m.
    unfold aux.
    
Lemma continuity2 (f : (nat -> nat) -> nat) (alpha : nat -> nat)
      (ext : forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v) :
      continuous f alpha.
Proof.
  have p := (RApp_inst _ _ (inj3 f alpha () ext) (RGeneric ® (@ctx_nil nat nat alpha))).(q1) .
  have hyp : forall alpha beta, (RApp_inst _ _ (inj3 f alpha () ext) (RGeneric ® (@ctx_nil nat nat alpha))).(q2) = (RApp_inst _ _ (inj3 f beta () ext) (RGeneric ® (@ctx_nil nat nat beta))).(q2).
  cbn.
  cbv.
<  reflexivity.
  have aux : BNdialogue p.(q2) alpha = p.(q1).
  - destruct p as [pa pb pe] ; simpl.
    elim: pe ; trivial.
    exact (fun _ _ _ => eq_S _ _).
  - About BNDialogue_Continuity.*)
    
End Avarenat.

back to top