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.