Trying Presheaf model

FFOLCompleteness.agda

@@ -296,6 +296,45 @@ module FFOLCompleteness where
       ; R[] = refl
       }
 
+  record Presheaf' : Set (lsuc (ℓ¹)) where
+    field
+      World : Set ℓ¹
+      Arr : World → World → Set ℓ¹ -- arrows
+      id-a : {w : World} → Arr w w -- id arrow
+      _∘a_ : {w w' w'' : World} → Arr w w' → Arr w' w'' → Arr w w'' -- arrow composition
+      ∘a-ass : {w w' w'' w''' : World}{a : Arr w w'}{b : Arr w' w''}{c : Arr w'' w'''}
+        → ((a ∘a b) ∘a c) ≡ (a ∘a (b ∘a c))
+      idl-a : {w w' : World} → {a : Arr w w'} → (id-a {w}) ∘a a ≡ a
+      idr-a : {w w' : World} → {a : Arr w w'} → a ∘a (id-a {w'}) ≡ a
+      TM : World → Set ℓ¹
+      TM≤ : {w w' : World} → Arr w w' → TM w' → TM w
+      REL : (w : World) → TM w → TM w → Set ℓ¹
+      REL≤ : {w w' : World} → {t u : TM w'} → (eq : Arr w w') → REL w' t u → REL w (TM≤ eq t) (TM≤ eq u)
+
+    {-
+    -- Now we try to interpret formulæ and contexts
+    import FFOLInitial as I
+    _⊩ᶠ_  : World → (I.For I.◇t) → Set ℓ¹
+    w ⊩ᶠ I.R t u = REL w {!!} {!!}
+    w ⊩ᶠ (A I.⇒ B) = ∀ (w' : World) → Arr w w' → w' ⊩ᶠ A → w' ⊩ᶠ B
+    w ⊩ᶠ I.∀∀ A = ∀ (t : TM w) → {!!}
+    -}
+
+
+
+  record Kripke : Set (lsuc (ℓ¹)) where
+    field
+      World : Set ℓ¹
+      Arr : World → World → Prop ℓ¹ -- arrows
+      id-a : {w : World} → Arr w w -- id arrow
+      _∘a_ : {w w' w'' : World} → Arr w w' → Arr w' w'' → Arr w w'' -- arrow composition
+      -- associativity and id rules are trivial cause arrows are in prop
+      TM : World → Set ℓ¹
+      TM≤ : {w w' : World} → Arr w w' → TM w' → TM w
+      REL : (w : World) → TM w → TM w → Prop ℓ¹
+      REL≤ : {w w' : World} → {t u : TM w'} → (eq : Arr w w') → REL w' t u → REL w (TM≤ eq t) (TM≤ eq u)
+
+
   -- Completeness proof
 
   -- We first build our universal Kripke model
@@ -305,26 +344,67 @@ module FFOLCompleteness where
     -- We have a model, we construct the Universal Presheaf model of this model
     import FFOLInitial as I
 
-    UniversalPresheaf : Presheaf
+    UniversalPresheaf : Kripke
     UniversalPresheaf = record
-       { World = I.Con
+       { World = (Γₜ : I.Cont) → I.Conp Γₜ
-       ; Arr = I.Sub
+       ; Arr = λ w₁ w₂ → (Γₜ : I.Cont) → (I.Pf* Γₜ (w₂ Γₜ) (w₁ Γₜ))
-       ; id-a = I.id
+       ; id-a = λ {w} Γₜ → I.Pf*-id
-       ; _∘a_ = λ σ σ' → σ' I.∘ σ
+       ; _∘a_ = λ σ₁ σ₂ Γₜ → I.Pf*-∘ (σ₁ Γₜ) (σ₂ Γₜ)
-       ; ∘a-ass = ≡sym I.∘-ass
+       --; ∘a-ass = λ {w} → ≡fun' (λ Γₜ → ≡sym (I.∘ₚ-ass {Γₚ = w Γₜ}))
-       ; idl-a = I.idr
+       --; idl-a = λ {w} {w'} → ≡fun' (λ Γₜ → I.idrₚ {Γₚ = w Γₜ} {Δₚ = w' Γₜ})
-       ; idr-a = I.idl
+       --; idr-a = λ {w} {w'} → ≡fun' (λ Γₜ → I.idlₚ {Γₚ = w Γₜ} {Δₚ = w' Γₜ})
-       ; TM = λ Γ → I.Tm (I.Con.t Γ)
+       ; TM = λ w → (Γₜ : I.Cont) → (I.Tm Γₜ)
-       ; TM≤ = λ σ t → t I.[ I.Sub.t σ ]t
+       ; TM≤ = λ σ t → t
-       ; REL = λ Γ t u → I.Pf Γ (I.r t u)
+       ; REL = λ w t u → (Γₜ : I.Cont) → I.Pf Γₜ (w Γₜ) (I.R (t Γₜ) (u Γₜ))
-       ; REL≤ = λ σ pf → (pf I.[ I.Sub.t σ ]pₜ) I.[ I.Sub.p σ ]p
+       ; REL≤ = λ σ pf → λ Γₜ → I.Pf*Pf {!!} (pf Γₜ)
        }
 
     -- I.xx are from initial, xx are from up
-    open Presheaf UniversalPresheaf
+    open Kripke UniversalPresheaf
+
+    -- We now create the forcing relation for our Universal presheaf
+    -- We need the world to depend of a term context (i guess), so i think i cannot make it so
+    -- the forcing relation works for every Kripke Model.
+    _⊩f_ : (w : World) → {Γₜ : I.Cont} → I.For Γₜ → Prop₁
+    _⊩f_ w {Γₜ} (I.R t v) = I.Pf Γₜ (w Γₜ) (I.R t v)
+    w ⊩f (A I.⇒ B) = ∀ w' → Arr w w' → w' ⊩f A → w' ⊩f B
+    w ⊩f I.∀∀ A = w ⊩f A
+
+    ⊩f-mon : {w w' : World} → Arr w w' → {Γₜ : I.Cont} → {A : I.For Γₜ} → w ⊩f A → w' ⊩f A
+    ⊩f-mon s {Γₜ} {I.R t v} wh = I.Pf*Pf (s Γₜ) wh
+    ⊩f-mon s {A = A I.⇒ B} wh w'' s' w''h = wh w'' (s ∘a s' ) w''h
+    ⊩f-mon s {A = I.∀∀ A} wh = ⊩f-mon s {A = A} wh
+
+    ⊩fPf : {Γₜ : I.Cont}{w : World}{A : I.For Γₜ} → w ⊩f A → I.Pf Γₜ (w Γₜ) A
+    ⊩fPf {A = I.R t v} pf = pf
+    ⊩fPf {A = A I.⇒ A₁} pf = {!I.app!}
+    ⊩fPf {A = I.∀∀ A} pf = I.p∀∀i (substP (λ X → I.Pf _ X A) {!!} (⊩fPf pf))
+
+
+    _⊩c_ : (w : World) → {Γₜ : I.Cont} → I.Conp Γₜ → Prop₁
+    w ⊩c I.◇p = ⊤
+    w ⊩c (Γₚ I.▹p⁰ A) = (w ⊩c Γₚ) ∧ (w ⊩f A)
+
+    ⊩c-mon : {w w' : World} → Arr w w' → {Γₜ : I.Cont} → {Γₚ : I.Conp Γₜ} → w ⊩c Γₚ → w' ⊩c Γₚ
+    ⊩c-mon s {Γₚ = I.◇p} wh = tt
+    ⊩c-mon s {Γₜ} {Γₚ = Γₚ I.▹p⁰ A} wh = ⟨ (⊩c-mon s (proj₁ wh)) , ⊩f-mon s {Γₜ} {A} (proj₂ wh) ⟩
+
+    ⊩cPf* : {Γₜ : I.Cont}{w : World}{Γₚ : I.Conp Γₜ} → w ⊩c Γₚ → I.Pf* Γₜ (w Γₜ) Γₚ
+    ⊩cPf* {Γₚ = I.◇p} h = tt
+    ⊩cPf* {Γₚ = Γₚ I.▹p⁰ x} h = ⟨ (⊩cPf* (proj₁ h)) , {!proj₂ h!} ⟩
+
+    _⊫_ : {Γₜ : I.Cont} → (I.Conp Γₜ) → I.For Γₜ → Prop₁
+    Γₚ ⊫ A = ∀ w → w ⊩c Γₚ → w ⊩f A
     
     -- Now we want to show universality of this model, that is
     -- if you have a proof in UP, you have the same in I.
     
-    q : {Γ : Con}{A : For Γ} → Γ ⊢ A → I.Pf {!!} {!!}
+    u : {Γₜ : I.Cont}{Γₚ : I.Conp Γₜ}{A : I.For Γₜ} → I.Pf Γₜ Γₚ A → Γₚ ⊫ A
-    u : {Γ : Con}{A : For Γ} → I.Pf {!!} {!!} → Γ ⊢ A
+    q : {Γₜ : I.Cont}{Γₚ : I.Conp Γₜ}{A : I.For Γₜ} → Γₚ ⊫ A → I.Pf Γₜ Γₚ A
+
+    u {A = I.R t s} pf w wh = {!!}
+    u {A = A I.⇒ B} pf w wh w' s w'h  = u {A = B} (I.app pf (q λ w'' w''h → {!!})) w' (⊩c-mon s wh)
+    u {A = I.∀∀ A} pf w wh = {!!}
+    q {A = I.R t s} h = {!!}
+    q {A = A I.⇒ B} h = {!!}
+    q {A = I.∀∀ A} h = {!!}

FFOLInitial.agda

@@ -200,7 +200,7 @@ module FFOLInitial where
 
 
   -- With those contexts, we have everything to define proofs
-  data PfVar : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Set₁ where
+  data PfVar : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁ where
     pvzero : {A : For Γₜ} → PfVar Γₜ (Γₚ ▹p⁰ A) A
     pvnext : {A B : For Γₜ} → PfVar Γₜ Γₚ A → PfVar Γₜ (Γₚ ▹p⁰ B) A
                                                                 
@@ -389,9 +389,6 @@ module FFOLInitial where
       {f = λ {W} ξ pf → _,ₚ_ ξ pf}{x = σₚ [ α ∘ₜ β ]σₚ}{y = pf [ α ∘ₜ β ]pₜ})
     ))
 
-
-
-
   -- How ∘ₚ and ∘ₜ interact to make associativity (to be proven later for Sub)
   
   ∘ₚₜ-ass⁰ :
@@ -645,3 +642,45 @@ module FFOLInitial where
     ; ∀e = λ {Γ} {F} pf {t} → p∀∀e pf
     }
 
+
+  -- We define normal and neutral forms
+  data Ne : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁
+  data Nf : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁
+  data Ne where
+    var : {A : For Γₜ} → PfVar Γₜ Γₚ A → Ne Γₜ Γₚ A
+    app : {A B : For Γₜ} → Ne Γₜ Γₚ (A ⇒ B) → Nf Γₜ Γₚ A → Ne Γₜ Γₚ B
+    p∀∀e : {A : For (Γₜ ▹t⁰)} → {t : Tm Γₜ} → Ne Γₜ Γₚ (∀∀ A) → Ne Γₜ Γₚ (A [ idₜ ,ₜ t ]f)
+  data Nf where
+    R : {t u : Tm Γₜ} → Ne Γₜ Γₚ (R t u) → Nf Γₜ Γₚ (R t u)
+    lam : {A B : For Γₜ} → Nf Γₜ (Γₚ ▹p⁰ A) B → Nf Γₜ Γₚ (A ⇒ B)
+    p∀∀i : {A : For (Γₜ ▹t⁰)} → Nf (Γₜ ▹t⁰) (Γₚ ▹tp) A → Nf Γₜ Γₚ (∀∀ A)
+
+
+  Pf* : (Γₜ : Cont) → Conp Γₜ → Conp Γₜ → Prop₁
+  Pf* Γₜ Γₚ ◇p = ⊤
+  Pf* Γₜ Γₚ (Γₚ' ▹p⁰ A) = (Pf* Γₜ Γₚ Γₚ') ∧ (Pf Γₜ Γₚ A)
+
+  Sub→Pf* : {Γₜ : Cont} {Γₚ Γₚ' : Conp Γₜ} →  Subp {Γₜ} Γₚ Γₚ' → Pf* Γₜ Γₚ Γₚ'
+  Sub→Pf* εₚ = tt
+  Sub→Pf* (σₚ ,ₚ pf) = ⟨ (Sub→Pf* σₚ) , pf ⟩
+  Pf*-id : {Γₜ : Cont} {Γₚ : Conp Γₜ} → Pf* Γₜ Γₚ Γₚ
+  Pf*-id = Sub→Pf* idₚ
+
+  Pf*▹p : {Γₜ : Cont}{Γₚ Γₚ' : Conp Γₜ}{A : For Γₜ} → Pf* Γₜ Γₚ Γₚ' → Pf* Γₜ (Γₚ ▹p⁰ A) Γₚ'
+  Pf*▹p {Γₚ' = ◇p} s = tt
+  Pf*▹p {Γₚ' = Γₚ' ▹p⁰ x} s = ⟨ (Pf*▹p (proj₁ s)) , (wkᵣp (rightRen reflRen) (proj₂ s)) ⟩
+  Pf*▹tp : {Γₜ : Cont}{Γₚ Γₚ' : Conp Γₜ} → Pf* Γₜ Γₚ Γₚ' → Pf* (Γₜ ▹t⁰) (Γₚ ▹tp) (Γₚ' ▹tp)
+  Pf*▹tp {Γₚ' = ◇p} s = tt
+  Pf*▹tp {Γₚ' = Γₚ' ▹p⁰ A} s = ⟨ Pf*▹tp (proj₁ s) , (proj₂ s) [ wkₜσₜ idₜ ]pₜ ⟩
+
+  Pf*Pf : {Γₜ : Cont} {Γₚ Γₚ' : Conp Γₜ} {A : For Γₜ} → Pf* Γₜ Γₚ Γₚ' → Pf Γₜ Γₚ' A → Pf Γₜ Γₚ A
+  Pf*Pf s (var pvzero) = proj₂ s
+  Pf*Pf s (var (pvnext pv)) = Pf*Pf (proj₁ s) (var pv)
+  Pf*Pf s (app p p') = app (Pf*Pf s p) (Pf*Pf s p')
+  Pf*Pf s (lam p) = lam (Pf*Pf (⟨ (Pf*▹p s) , (var pvzero) ⟩) p)
+  Pf*Pf s (p∀∀e p) = p∀∀e (Pf*Pf s p)
+  Pf*Pf s (p∀∀i p) = p∀∀i (Pf*Pf (Pf*▹tp s) p)
+
+  Pf*-∘ : {Γₜ : Cont} {Γₚ Δₚ Ξₚ : Conp Γₜ} → Pf* Γₜ Δₚ Ξₚ → Pf* Γₜ Γₚ Δₚ → Pf* Γₜ Γₚ Ξₚ
+  Pf*-∘ {Ξₚ = ◇p} α β = tt
+  Pf*-∘ {Ξₚ = Ξₚ ▹p⁰ A} α β = ⟨ Pf*-∘ (proj₁ α) β , Pf*Pf β (proj₂ α) ⟩

PropUtil.agda

@@ -13,7 +13,7 @@ module PropUtil where
   -- ⊥ is a data with no constructor
   -- ⊤ is a record with one always-available constructor
   data ⊥ : Prop where
-  record ⊤ : Prop where
+  record ⊤ : Prop ℓ where
     constructor tt
 
 
@@ -21,7 +21,7 @@ module PropUtil where
     inj₁ : {P Q : Prop} → P → P ∨ Q
     inj₂ : {P Q : Prop} → Q → P ∨ Q
 
-  record _∧_ (P Q : Prop) : Prop where
+  record _∧_ (P Q : Prop ℓ) : Prop ℓ where
     constructor ⟨_,_⟩
     field
       p : P
@@ -31,9 +31,9 @@ module PropUtil where
   infixr 11 _∨_
 
   -- ∧ elimination
-  proj₁ : {P Q : Prop} → P ∧ Q → P
+  proj₁ : {P Q : Prop ℓ} → P ∧ Q → P
   proj₁ pq = _∧_.p pq
-  proj₂ : {P Q : Prop} → P ∧ Q → Q
+  proj₂ : {P Q : Prop ℓ} → P ∧ Q → Q
   proj₂ pq = _∧_.q pq
 
   -- ∨ elimination