New notations + Monad definition

theories/LContexts.v

@@ -170,9 +170,13 @@ Notation " l ≤ε l' " := (wfLCon_le l l') (at level 40).
 
 Definition wfLCon_le_id l : l ≤ε l := fun n b ne => ne.
 
+Notation " 'idε' " := (wfLCon_le_id) (at level 40).
+
 Definition wfLCon_le_trans {l l' l''} : l ≤ε l' -> l' ≤ε l'' -> l ≤ε l'' :=
   fun f f' n b ne => f n b (f' n b ne).
 
+Notation " a •ε b " := (wfLCon_le_trans a b) (at level 40).
+
 Lemma LCon_le_in_LCon {l l' n b} {ne : not_in_LCon (pi1 l') n} :
   l ≤ε l' -> in_LCon l n b -> l ≤ε (l' ,,l (ne , b)).
 Proof.
@@ -527,7 +531,7 @@ Proof.
           | cons a q => _
           end) ; intros.
   - refine (P wl _ _).
-    now eapply wfLCon_le_id.
+    now eapply (idε).
     eapply Lack_nil_AllInLCon.
     now symmetry.
   - refine (max _ _).
@@ -542,9 +546,9 @@ Proof.
         now eapply Lack_n_add.
       * intros * τ allinl.
         refine (P wl' _ allinl).
-        eapply wfLCon_le_trans ; try eassumption.
-        eapply LCon_le_step.
-        now eapply wfLCon_le_id.
+        unshelve eapply (_ •ε _).
+        3: eapply LCon_le_step ; now eapply wfLCon_le_id.
+        eassumption.
     + unshelve refine (Max_Bar_aux _ n q _ _).
       * unshelve eapply wfLCons ; [exact wl | exact a | | exact false].
         eapply Lack_n_notinLCon.

theories/LogicalRelation.v

@@ -1,6 +1,6 @@
 (** * LogRel.LogicalRelation: Definition of the logical relation *)
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping.
+From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping Monad.
 
 Set Primitive Projections.
 Set Universe Polymorphism.
@@ -272,7 +272,29 @@ Notation "[ R | Γ ||-U t ≅ u : A | l ]< wl >" := (URedTmEq R wl Γ t u A l) (
 (** ** Reducibility of product types *)
 
 Module PiRedTy.
-
+  Lemma ez  `{ta : tag}
+    `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
+    {l : wfLCon} {Γ : context} {A : term} : True.
+  Proof.
+    assert (dom : term) by admit.
+    assert (cod : term) by admit.
+    assert (domRed : forall Δ (ρ : Δ ≤ Γ),
+               Weak l (fun l' alpha => [ |- Δ ]< l' > -> LRPack l' Δ dom⟨ρ⟩)) by admit.
+    assert (Δ : context) by admit.
+    assert (ρ : Δ ≤ Γ) by admit.
+
+
+    pose (zfe := fun Q => BType l _ Q (domRed _ ρ) ) ; cbn in zfe.
+    assert ( forall wl' : wfLCon,
+               ([ |-[ ta ] Δ ]< wl' > -> LRPack wl' Δ dom⟨ρ⟩) -> Type).
+    intros wl' Dom.
+    refine (forall (Hd : [ |-[ ta ] Δ ]< wl' >), _).
+    refine (forall a : term, _).
+    refine (forall ha : [ Dom Hd |  Δ ||- a : dom⟨ρ⟩]< wl' >, _).
+    refine (Dial wl' _).
+    intros wl''.
+    eapply LRPack.
+    exact wl''.
   Record PiRedTy@{i} `{ta : tag}
     `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
     {l : wfLCon} {Γ : context} {A : term}
@@ -283,9 +305,8 @@ Module PiRedTy.
     domTy : [Γ |- dom]< l >;
     codTy : [Γ ,, dom |- cod]< l > ;
     eq : [Γ |- tProd dom cod ≅ tProd dom cod]< l > ;
-    domN : nat ;
-    domRed {Δ l'} (ρ : Δ ≤ Γ) (τ : l' ≤ε l) (Ninfl : AllInLCon domN l') :
-      [ |- Δ ]< l' > -> LRPack@{i} l' Δ dom⟨ρ⟩ ;
+    dom {Δ} (ρ : Δ ≤ Γ) : Weak l (fun l' τ => [ |- Δ ]< l' > -> LRPack@{i} l' Δ dom⟨ρ⟩) ;
+    }.
     codomN {Δ a l'} (ρ : Δ ≤ Γ) (τ : l' ≤ε l) (Ninfl : AllInLCon domN l')
       (h : [ |- Δ ]< l' >)
       (ha : [ (domRed ρ τ Ninfl h) |  Δ ||- a : dom⟨ρ⟩]< l' >) :

theories/LogicalRelation/Application.v

@@ -123,6 +123,7 @@ Section AppTerm.
     refine (max (max (max RFN RuN)
                (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))) _).
     unshelve refine (Max_Bar _ _ _).
+    About Max_Bar_Bar_lub.
     + assumption.
     + exact (max (max RFN RuN)
                (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))).
@@ -194,11 +195,6 @@ About AppTyN_subproof.
                 now eapply Nat.le_max_l).
            + now eapply Bar_lub_ub. 
            + now eapply Bar_lub_AllInLCon.
-           + clear Ninfl τ wl'.
-             (intros ;
-              rewrite (AllInLCon_Irrel _ _ ne0 ne') ;
-              rewrite (wfLCon_le_Irrel _ _ τ τ');
-              reflexivity).
       }
       reflexivity.
       Defined. 

theories/LogicalRelation/Weakening.v

@@ -17,12 +17,14 @@ Section Weakenings.
     [Δ ||-Π< l > A⟨ρ⟩]< wl >.
   Proof.
     destruct ΠA as[dom cod];  cbn in *.
-    assert (domRed' : forall Δ' wl' (ρ' : Δ' ≤ Δ) (τ : wl' ≤ε wl)
+    unshelve refine (let domRed' : forall Δ' wl' (ρ' : Δ' ≤ Δ) (τ : wl' ≤ε wl)
                              (Ninfl : AllInLCon domN wl'),
-               [|- Δ']< wl' > -> [Δ' ||-< l > dom⟨ρ⟩⟨ρ'⟩ ]< wl' >).
+               [|- Δ']< wl' > -> [Δ' ||-< l > dom⟨ρ⟩⟨ρ'⟩ ]< wl' > := _ in _).
     {
-      intros ? ? ρ' ??; replace (_⟨_⟩) with (dom⟨ρ' ∘w ρ⟩) by now bsimpl.
-      econstructor ; now unshelve eapply domRed.
+      intros ? ? ρ' ??.
+      replace (_⟨_⟩) with (dom⟨ρ' ∘w ρ⟩) by now bsimpl.
+      econstructor.
+      now unshelve eapply domRed.
     }
     set (cod' := cod⟨wk_up dom ρ⟩).
     unshelve refine
@@ -144,7 +146,8 @@ Section Weakenings.
       + exact (dom⟨ρ⟩).
       + exact (cod⟨wk_up dom ρ⟩).
       + exact domN.
-      + unfold wkΠ'. intros ; unshelve eapply (codomN Δ0 a l' (ρ0 ∘w ρ) τ Ninfl Ninfl' h).
+      + unfold wkΠ'.
+        intros ; unshelve eapply (codomN Δ0 a l' (ρ0 ∘w ρ) τ Ninfl Ninfl' h).
         subst X.
         irrelevance.
       + change (tProd _ _) with ((tProd dom cod)⟨ρ⟩);  gen_typing.

theories/LogicalRelation2.v

@@ -269,10 +269,10 @@ Export URedTm(URedTm,Build_URedTm,URedTmEq,Build_URedTmEq).
 Notation "[ R | Γ ||-U t : A | l ]< wl >" := (URedTm R wl Γ t A l) (at level 0, R, Γ, t, A, wl, l at level 50).
 Notation "[ R | Γ ||-U t ≅ u : A | l ]< wl >" := (URedTmEq R wl Γ t u A l) (at level 0, R, Γ, t, u, A, wl, l at level 50).
 
+
 (** ** Reducibility of product types *)
 
 Module PiRedTy.
-  Print BType.
 
   Lemma ez  `{ta : tag}
     `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
@@ -297,6 +297,15 @@ Module PiRedTy.
     exact wl''.
     exact Δ.
     exact (cod[a .: (ρ >> tRel)]).
+
+    pose (Y := BType l _ (fun (wl' : wfLCon) (Dom : [ |-[ ta ] Δ ]< wl' > -> LRPack wl' Δ dom⟨ρ⟩) =>
+                 forall (Hd : [ |-[ ta ] Δ ]< wl' >) (a : term)
+                        (ha : [ Dom Hd |  Δ ||- a : dom⟨ρ⟩]< wl' >),
+                   Dial wl' (fun wl'' => (LRPack wl'' Δ (cod[a .: (ρ >> tRel)]))))
+                 (domRed _ ρ)).
+    cbn in Y.
+    pose (tzfd := zfe X).
+    apply zfe in X.
     pose (test:= fun R => BType_dep l _
          (fun wl' Dom => forall (a : term)
                                 (Hd : [ |-[ ta ] Δ ]< wl' >)

theories/Monad.v

@@ -0,0 +1,125 @@
+From LogRel.AutoSubst Require Import core unscoped Ast Extra.
+Require Import PeanoNat.
+From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping.
+
+Record Psh (wl : wfLCon) :=
+  { typ : forall wl',  wl' ≤ε wl -> Type ;
+    mon : forall wl' wl''  (alpha : wl' ≤ε wl) (beta : wl'' ≤ε wl')
+    (delta : wl'' ≤ε wl),
+      typ wl' alpha -> typ wl'' delta
+  }.
+
+Arguments typ [_] _.
+Arguments mon [_ _ _] _.
+
+Record Weak (wl : wfLCon) (P : forall wl', wl' ≤ε wl  -> Type) : Type :=
+  { PN : nat ;
+    WP : forall (wl' : wfLCon) (alpha : wl' ≤ε wl),
+      AllInLCon PN wl' -> P wl' alpha ;
+  }.
+
+
+Lemma monot (wl wl' wl'' : wfLCon)
+  (P : forall wl',  wl' ≤ε wl -> Type)
+  (alpha :  wl' ≤ε wl)
+  (beta :  wl'' ≤ε wl') :
+  Weak wl' (fun wl'' dzeta => P wl'' (dzeta •ε alpha)) ->
+  Weak wl'' (fun wl''' dzeta => P wl''' ((dzeta •ε beta) •ε alpha)).
+Proof.
+  intros [N WN].
+  exists N.
+  intros wl''' dzeta allinl.
+  exact (WN wl''' (dzeta •ε beta) allinl).
+Qed.  
+
+
+Definition Wbind (wl : wfLCon) (P Q : forall wl', wl' ≤ε wl  -> Type)
+  (Pe : forall wl' (alpha : wl' ≤ε wl) wl'' (beta : wl'' ≤ε wl),
+      wl'' ≤ε wl' -> P wl' alpha -> P wl'' beta)
+  (Qe : forall wl' (alpha : wl' ≤ε wl) wl'' (beta : wl'' ≤ε wl),
+      wl'' ≤ε wl' -> Q wl' alpha -> Q wl'' beta)
+  (f : forall wl' (alpha : wl' ≤ε wl),
+      P wl' alpha -> Weak wl' (fun wl'' beta => Q wl'' (beta •ε alpha))) :
+  forall wl' (alpha : wl' ≤ε wl),
+    Weak wl' (fun wl'' beta => P wl'' (beta •ε alpha)) ->
+    Weak wl' (fun wl'' beta => Q wl'' (beta •ε alpha)).
+Proof.
+  intros * [N W].
+  unshelve econstructor.
+  { unshelve eapply (max N _).
+    unshelve eapply Max_Bar.
+    - exact wl'.
+    - exact N.
+    - intros wl'' beta allinl.
+      unshelve eapply (f wl'' (beta •ε alpha)).
+      now eapply W.
+  }
+  intros wl'' beta allinl.
+  unshelve eapply Qe.
+  4: unshelve eapply f.
+  { unshelve eapply (Bar_lub (Bar_lub wl' wl'' N beta _) wl'').
+    3: now eapply Bar_lub_smaller.
+    3: eassumption.
+    eapply AllInLCon_le.
+    eapply Nat.le_max_l.
+    eassumption.
+  }
+  + unshelve eapply Bar_lub_smaller.
+  + eapply (Bar_lub wl' wl'' N beta _).
+  + now eapply Bar_lub_ub.
+  + unshelve eapply (_ •ε alpha).
+    now eapply Bar_lub_ub.
+  + eapply W.
+    now eapply Bar_lub_AllInLCon.
+  + eapply AllInLCon_le ; [ | now eapply Bar_lub_AllInLCon].
+    etransitivity ; [ |now eapply Nat.le_max_r].
+    etransitivity ; [ | now eapply Max_Bar_Bar_lub].
+    cbn.
+    reflexivity.
+Qed.    
+
+
+Definition Wret (wl : wfLCon) (P : forall wl', wl' ≤ε wl  -> Type)
+  (Pe : forall wl' (alpha : wl' ≤ε wl) wl'' (beta : wl'' ≤ε wl),
+      wl'' ≤ε wl' -> P wl' alpha -> P wl'' beta)
+  (p : P wl (idε wl)) : Weak wl P.
+Proof.
+  unshelve econstructor.
+  - exact 0.
+  - intros ; now eapply Pe.
+Defined.
+
+
+(*
+Definition Wbind (wl : wfLCon) (P Q : wfLCon -> Type)
+  (Pe : forall wl' wl'', wl'' ≤ε wl' -> P wl' -> P wl'')
+  (Qe : forall wl' wl'', wl'' ≤ε wl' -> Q wl' -> Q wl'')
+  (f : forall wl', wl' ≤ε wl -> P wl' -> Weak wl' Q)
+  (p : Weak wl P) : Weak wl Q.
+Proof.
+  unshelve econstructor.
+  - unshelve refine (max (PN wl P p) (Max_Bar _ _ _)).
+    + exact wl.
+    + exact (PN _ _ p).
+    + intros wl' tau Ninfl.
+      eapply PN.
+      eapply f.
+      * eassumption.
+      * eapply WP ; try eassumption.
+  - intros wl' tau Ninfl.
+    unshelve eapply WP.
+    4:{ eapply AllInLCon_le ; try eassumption.
+        etransitivity.
+        eapply (Max_Bar_Bar_lub _ _
+                  (fun wl'0 tau0 Ninfl0 => PN wl'0 Q (f wl'0 tau0 (WP wl P p wl'0 tau0 Ninfl0)))).
+        eapply Nat.le_max_r.
+    }
+    eapply Bar_lub_smaller.
+    Unshelve.
+    + eassumption.
+    + eapply AllInLCon_le ; try eassumption.
+      now eapply Nat.le_max_l.
+    + now eapply Bar_lub_ub.
+    + now eapply Bar_lub_AllInLCon.
+Defined.      
+*)

theories/Monad2.v

@@ -32,30 +32,19 @@ Proof.
       now eapply wfLCon_le_id.
 Qed.
 
-(*Fixpoint BType (wl : wfLCon) (P : wfLCon -> Type)
-  (Pe : forall wl' wl'', wl'' ≤ε wl' -> P wl' -> P wl'')
+Fixpoint BType (wl : wfLCon) (P : wfLCon -> Type)
   (Q : forall wl', P wl' -> Type)
-  (Qe : forall wl' wl'' (f : wl'' ≤ε wl') (p : P wl') (p' : P wl''),
-      Q wl' p -> Q wl'' p')
-  (p : Dial wl P) : Type.
-Proof.
-  refine ( match p with
-  | eta _ _ x => _
-  | ϝdig _ _ pt pf => _
-           end).
-  - clear p.
-    
-    :=
+  (p : Dial wl P) : Type    :=
   match p with
   | eta _ _ x => Q wl x
-  | ϝdig _ _ pt pf => prod (BType _ P Q pt) (BType _ P Q pf)
+  | ϝdig _ _ pt pf => prod (@BType _ P Q pt) (BType _ P Q pf)
   end.
 
-Fixpoint BType_dep (wl : wfLCon) (P : wfLCon -> Type)
+(*Fixpoint BType_dep (wl : wfLCon) (P : wfLCon -> Type)
   (Q : forall wl', P wl' -> Type)
   (R : forall wl' p, Q wl' p -> Type)
   (p : Dial wl P) :
-  BType wl P Q p -> Type :=
+  BType wl P Pe Q Qe p -> Type :=
   match p with
   | eta _ _ x => fun H => R wl x H
   | ϝdig _ _ pt pf => fun H => prod (BType_dep _ P Q R pt (fst H))