##### https://gitlab.inria.fr/mbaillon/gardening-with-the-pythia
Revision 1c783fb2a09f78c7d1bd2f27008221724fe204d0 authored by Martin Baillon on 08 July 2021, 22:02:58 UTC, committed by Martin Baillon on 08 July 2021, 22:02:58 UTC
1 parent 2a2e136
Tip revision: 1c783fb
Dialogue.v
``````(* Set Universe Polymorphism. *)
(* Set Primitive Projections. *)
(* Set Polymorphic Inductive Cumulativity. *)
Require Import List.
Require Import Streams.
Require Import ssreflect.
Set Implicit Arguments.
Set Primitive Projections.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section DialogueTrees.

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

Inductive Dialogue A : Type :=
| êta : A -> Dialogue A
| bêta : (Y -> Dialogue A) -> X -> Dialogue A.

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

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

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

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

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

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

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

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

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

(* From mathcomp Require Import all_ssreflect. *)

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

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

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

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

End DialogueTrees.

Section DialogueStreams.

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

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

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

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

End DialogueStreams.

Section NatDialogueStreams.

Variable (Y : Type).

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

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

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

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

End NatDialogueStreams.

Section BranchingNaturalNumbers.

Variable (X Y : Type).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(*DialoguetoBN and BNtoDialogue preserve the dialogue function*)

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

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

End BranchingNaturalNumbers.

Section BranchingNatStreams.

Variable (Y : Type).

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

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

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

End BranchingNatStreams.

Section Continuity.

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

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

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

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

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

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

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

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

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

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

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

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

End Continuity.

Section StreamContinuity.

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

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

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

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

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

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

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

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

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

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

End StreamContinuity.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Notation "∏" := (@RPi).

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

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

Notation "'λ'" := RLam.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

``````

Computing file changes ...