add kripke W

javra · Apr 23, 2020 · db2f4ff · db2f4ff
1 parent a943115
commit db2f4ff
Show file tree

Hide file tree

Showing 3 changed files with 69 additions and 7 deletions.
diff --git a/EWRSgRec.agda b/EWRSgRec.agda
@@ -259,7 +259,7 @@ _,t_ {S} = _,tS_
 π₂S : ∀{Γ Δ}{A : TyS Δ}(σ : Sub Γ (Δ ▶S A)) → TmS Γ (A [ π₁S σ ]TS)
 π₂S {Γ}{Δ}{A} σ = record { ᴬ   = λ γ → ₂ (σ.ᴬ γ) ;
                            E   = S.π₂ σ.Ec ;
-                           w   = λ α → ? }
+                           w   = λ α → {!!} }
   where
     module σ = Sub σ
 

diff --git a/IFW.agda b/IFW.agda
@@ -16,13 +16,13 @@ module IFW where
 ʷc ∙c        γc       = lift tt
 ʷc (Γc ▶c B) (γc , α) = ʷc Γc γc , λ _ → ʷS B
 
-ʷP' : (B : TyS)(β : Set₁) → ʷS B
-ʷP' U        β = ⊤
-ʷP' (Π̂S T B) β = λ τ → ʷP' (B τ) β
+ʷP' : (B : TyS) → ʷS B
+ʷP' U        = ⊤
+ʷP' (Π̂S T B) = λ τ → ʷP' (B τ)
 
 ʷt : ∀{Γc B}(t : Tm Γc B){γc : ᴱc Γc ᵃc}(α : (ᴱt t ᵃt) γc)
      → ᵈt (ᴱt t) (ʷc Γc γc) α
-ʷt (var vvz)     {γc , β} αʷ = ʷP' _ β
+ʷt (var vvz)     {γc , β} αʷ = ʷP' _
 ʷt (var (vvs x))          αʷ = ʷt (var x) αʷ
 ʷt (t $S τ)               αʷ = ʷt t αʷ
 

diff --git a/W.agda b/W.agda
@@ -32,8 +32,27 @@ infixl 3 _▶P_
     module Γ = Con Γ
     field
       S : S.TyS Γ.S
-      w : (ω : S.Sub Ω Γ.S)(t : S.TmS Ω (S S.[ ω ]TS)) → Set₁
+      w : Set₁
 
+  record TyP (Γ : Con) : Set₃ where
+    module Γ = Con Γ
+    field
+      S : S.TyP Γ.S
+      w : (ω : S.Sub Ω Γ.S)(t : S.TmP Ω (S S.[ ω ]TP)) → (S.TyP.E S ᵃP) (Γ.w ω)
+
+  record TmS (Γ : Con) (B : TyS Γ) : Set₃ where
+    module Γ = Con Γ
+    module B = TyS B
+    field
+      S : S.TmS Γ.S B.S
+      w : (ω : S.Sub Ω Γ.S) → B.w ≡ (S.TmS.E S ᵃt) (Γ.w ω)
+
+  record TmP (Γ : Con) (A : TyP Γ) : Set₃ where
+    module Γ = Con Γ
+    module A = TyP A
+    field
+      S : S.TmP Γ.S A.S
+      w : (ω : S.Sub Ω Γ.S) → A.w ω (S S.[ ω ]tP) ≡ {!!} -- fix univ levels
 
   ∙ : Con
   ∙ = record { S = S.∙
@@ -42,10 +61,53 @@ infixl 3 _▶P_
 
   _▶S_ : (Γ : Con) → TyS Γ → Con
   Γ ▶S B = record { S = Γ.S S.▶S B.S
-                  ; w = λ ω → Γ.w (S.π₁S ω) , B.w (S.π₁S ω) (S.π₂S ω)
+                  ; w = λ ω → Γ.w (S.π₁S ω) , B.w
                   }
     where
       module Γ = Con Γ
       module B = TyS B
+
+  _▶P_ : (Γ : Con) → TyP Γ → Con
+  Γ ▶P A = record { S = Γ.S S.▶P A.S
+                  ; w = λ ω → Γ.w (S.π₁P ω)
+                  }
+    where
+      module Γ = Con Γ
+      module A = TyP A
+
+  U : {Γ : Con} → TyS Γ
+  U {Γ} = record { S = S.U
+                 ; w = Y }
+    where
+      module Γ = Con Γ
+
+  El : {Γ : Con} (a : TmS Γ U) → TyP Γ
+  El {Γ} a = record { S = S.El a.S
+                    ; w = λ ω t → coe (a.w ω) y
+                    }
+    where
+      module Γ = Con Γ
+      module a = TmS a
+
+  ΠS : {Γ : Con} → (a : TmS Γ U) → (B : TyS (Γ ▶P El a)) → TyS Γ
+  ΠS {Γ} a B = record { S = S.ΠS a.S B.S
+                      ; w = X → B.w
+                      }
+    where
+      module Γ = Con Γ
+      module a = TmS a
+      module B = TyS B
+
+  --add ΠP
+
+  appS : {Γ : Con} {a : TmS Γ U} → {B : TyS (Γ ▶P El a)} → (t : TmS Γ (ΠS a B)) → TmS (Γ ▶P El a) B
+  appS {Γ}{a}{B} t = record { S = S.appS t.S
+                            ; w = λ ω → {!!} ◾ t.w (S.π₁P ω)
+                            }
+    where
+      module Γ = Con Γ
+      module a = TmS a
+      module B = TyS B
+      module t = TmS t