add strict algebras

.gitignore

@@ -1,2 +1,3 @@
 *.agdai
 *.agda~
+*\#*

IF.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --rewriting #-}
+{-# OPTIONS --prop --rewriting #-}
 
 module IF where
 

IFA.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --rewriting #-}
+{-# OPTIONS --prop --rewriting #-}
 module IFA where
 
 open import Lib hiding (id; _∘_)

IFD.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --rewriting --allow-unsolved-meta #-}
+{-# OPTIONS --prop --rewriting --allow-unsolved-meta #-}
 module IFD where
 
 open import Lib hiding (id; _∘_)

IFSzumi.agda

@@ -55,7 +55,7 @@ F0t : ∀{Γc B}(t : Tm Γc B) → F0S' Γc B
 F0t {B = U}      (var vvz) = inr _
 F0t {B = T ⇒̂S B} (var vvz) = λ τ → F0S'fun B (λ { (inl x) → inl x ;
                                                   (inr x) → inr (τ , x) }) (F0t {B = B} (var vvz))
-F0t {Γc}{B}      (var (vvs x)) = F0S'fun B inl (F0t (var x))
+F0t {B = B}      (var (vvs x)) = F0S'fun B inl (F0t (var x))
 F0t              (t $S τ)      = F0t t τ
 
 F0P : ∀{Ωc B}(t : Tm Ωc B) → (CodS B ᵃP) (_ , F0c Ωc)

IFVec.agda

@@ -13,7 +13,6 @@ postulate Ns  : N → N
 
 open import IFW
 
-
 Γvec : Con (∙c ▶c N ⇒̂S U)
 Γvec = ∙ ▶P El (vz $S Nz) ▶P (Π̂P A (λ a → Π̂P N λ m → (vz $S m) ⇒P El (vz $S Ns m)))
 
@@ -24,18 +23,11 @@ postulate cᴱ : A → N → vᴱ → vᴱ
 nʷ = ₂ (₁ (ʷC Γvec (_ , nᴱ , cᴱ) idP))
 cʷ = ₂ (ʷC Γvec (_ , nᴱ , cᴱ) idP)
 
-foo = ˢc (ᴱc (∙c ▶c (N ⇒̂S U))) (ʷc Γvec (_ , nᴱ , cᴱ) id)
-
-postulate s : foo
-
-bar = ˢC (ᴱC Γvec) s {_ , nᴱ , cᴱ} (ʷC Γvec (_ , nᴱ , cᴱ) idP)
-
-postulate s' : bar
+postulate s : ˢc (ᴱc (∙c ▶c (N ⇒̂S U))) (ʷc Γvec (_ , nᴱ , cᴱ) id)
+postulate s' : ˢC (ᴱC Γvec) s {_ , nᴱ , cᴱ} (ʷC Γvec (_ , nᴱ , cᴱ) idP)
 postulate a : A
 
 baz = happly (₂ (₁ s')) Nz ⁻¹
 
---{-# REWRITE baz #-}
-
 baz' : ₂ s (cᴱ a Nz nᴱ) (Ns Nz)
 baz' = coe (happly (₂ s' a Nz nᴱ) (Ns Nz) ⁻¹) (_ , coe (happly (₂ (₁ s')) Nz ⁻¹) (_ , refl) , refl)

IFW'.agda

@@ -1,10 +1,11 @@
 {-# OPTIONS --rewriting --allow-unsolved-metas #-}
 
+-- This is a version of wellformedness where we assume erasure does nothing
+
 open import Lib hiding (id; _∘_)
 open import IF
 open import IFA
 open import IFD
-open import IFE
 
 module IFW' {Ωc}(Ω : Con Ωc)
   {ωc : _ᵃc {zero} Ωc}(ω : (Ω ᵃC) ωc) where
@@ -20,8 +21,7 @@ module IFW' {Ωc}(Ω : Con Ωc)
 ʷt : ∀{Γc}(σ : Sub Ωc Γc){B}(t : Tm Γc B) → ᵈt t (ʷc σ) ≡ ʷS B ((t ᵃt) ((σ ᵃs) ωc))
 ʷt (σ , s) (var vvz)     = refl
 ʷt (σ , s) (var (vvs x)) = ʷt σ (var x)
-ʷt ε       (t $S τ)      = happly (ʷt ε t) τ
-ʷt (σ , s) (t $S τ)      = happly (ʷt (σ , s) t) τ
+ʷt σ       (t $S τ)      = happly (ʷt σ t) τ
 
 ʷtid : ∀{B}(t : Tm Ωc B) → ᵈt t (ʷc id) ≡ ʷS B ((t ᵃt) ωc)
 ʷtid t = ʷt id t

IFW.agda

@@ -36,9 +36,9 @@ cur (T ⇒̂S B) X f = λ τ → cur B X λ l → f (τ , l)
 f2 : {B : TyS} → (unc B ⊤ → unc B ⊤ → Set ℓ) → ʷS' B (ʷS' B (Set ℓ))
 f2 {B} f = cur B (ʷS' B (Set ℓ)) λ l → cur B (Set ℓ) (f l)
 
-ʷv' : (B : TyS) (A : Set ℓ) → ʷ²S B
-ʷv' U        A = A
-ʷv' (T ⇒̂S B) A = λ τ τ' → ʷv' B (A × (τ ≡ τ'))
+ʷEl : (B : TyS) (A : Set ℓ) → ʷ²S B
+ʷEl U        A = A
+ʷEl (T ⇒̂S B) A = λ τ τ' → ʷEl B (A × (τ ≡ τ'))
 
 hd : ∀{B}{Γc}(t : Tm Γc B) → TyS
 hd {B} (var x)  = B
@@ -63,7 +63,7 @@ hdfill (t $S τ) α = hdfill t α τ
 {-# REWRITE ʷt=id #-}
 
 ʷP : ∀ A (α : (ᴱP A ᵃP) ωc)(X : Set ℓ) → ᵈP (ᴱP A) (ʷc id) α -- maybe put the term itself into the signature
-ʷP (El a)   α X = hdfill a (f2 (f1 (ʷv' (hd a) X))) -- check again, maybe revive old ʷt'
+ʷP (El a)   α X = hdfill a (f2 (f1 (ʷEl (hd a) X))) -- check again, maybe revive old ʷt'
 ʷP (Π̂P T A) ϕ X = λ τ → ʷP (A τ) (ϕ τ) X
 ʷP (a ⇒P A) ϕ X = λ α αᵈ → ʷP A (ϕ α) (X × hdfill a αᵈ)
 

Lib.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --rewriting --allow-unsolved-metas #-}
+{-# OPTIONS --prop --rewriting --allow-unsolved-metas #-}
 
 module Lib where
 
@@ -285,6 +285,12 @@ irrel refl refl = refl
 Lift-irrel : ∀{ℓ ℓ'}{A : Set ℓ}{a₀ a₁ : A}(p₀ p₁ : Lift ℓ' (a₀ ≡ a₁)) → p₀ ≡ p₁
 Lift-irrel (lift refl) (lift refl) = refl
 
+data PLift {ℓ} : Prop ℓ → Set ℓ where
+  plift : ∀ {A} → A → PLift A
+
+plower : ∀{ℓ A} → PLift {ℓ} A → A
+plower (plift a) = a
+
 ≡≡ : ∀{ℓ}{A : Set ℓ}{a₀ a₀' a₁ a₁' : A}(p : a₀ ≡ a₀')(q : a₁ ≡ a₁')
   → (a₀ ≡ a₁) ≡ (a₀' ≡ a₁')
 ≡≡ refl refl = refl

W.agda

@@ -9,20 +9,19 @@ module W (Ω : E.Con)
 
   module Ω = E.Con Ω
 
-{-
-infixl 7 _[_]TS
-infixl 7 _[_]TP
-infixl 7 _[_]T
-infix  6 _∘_
-infixl 8 _[_]tS
-infixl 8 _[_]tP
-infixl 8 _[_]t
-infixl 5 _,tS_
-infixl 5 _,tP_
-infixl 5 _,t_
-infixl 3 _▶_
-infixl 3 _▶P_
--}
+
+  infixl 7 _[_]TS
+  infixl 7 _[_]TP
+  --infixl 7 _[_]T
+  infix  6 _∘_
+  infixl 8 _[_]tS
+  infixl 8 _[_]tP
+  --infixl 8 _[_]t
+  infixl 5 _,tS_
+  infixl 5 _,tP_
+  --infixl 5 _,t_
+  --infixl 3 _▶_
+  infixl 3 _▶P_
   infixl 3 _▶S_
 
   record Con : Set₃ where
@@ -34,20 +33,21 @@ infixl 3 _▶P_
     module Γ = Con Γ
     field
       E : E.TyS Γ.E
-      w : _ᵃc {zero} (E.Con.Ec Γ.E) → Set₁
+      w : Set₁ → Set₁
 
   record TyP (Γ : Con) : Set₃ where
     module Γ = Con Γ
     field
       E : E.TyP Γ.E
+      w : ∀(σ : E.Sub Ω Γ.E) α → ᵈP (E.TyP.E E) (Γ.wc σ) α
 
   record TmS (Γ : Con) (B : TyS Γ) : Set₃ where
     module Γ = Con Γ
     module B = TyS B
     field
-      E  : E.TmS Γ.E B.E
-      w' : Set₁
-      w  : ∀(σ : E.Sub Ω Γ.E) α → ᵈt (E.TmS.E E) (Γ.wc σ) α ≡ w'
+      E   : E.TmS Γ.E B.E
+      hTy : TyS Γ
+      w   : ∀(σ : E.Sub Ω Γ.E) α → ᵈt (E.TmS.E E) (Γ.wc σ) α ≡ {!!}
 
   record TmP (Γ : Con) (A : TyP Γ) : Set₃ where
     module Γ = Con Γ
@@ -67,7 +67,7 @@ infixl 3 _▶P_
 
   _▶S_ : (Γ : Con) → TyS Γ → Con
   Γ ▶S B = record { E  = Γ.E E.▶S B.E
-                  ; wc = λ σ → Γ.wc (E.π₁S σ) , λ _ → B.w ((E.Sub.Ec (E.π₁S σ) ᵃs) ωc)
+                  ; wc = λ σ → Γ.wc (E.π₁S σ) , λ _ → B.w Set
                   }
     where
       module Γ = Con Γ
@@ -90,14 +90,15 @@ infixl 3 _▶P_
 
   El : {Γ : Con} (a : TmS Γ U) → TyP Γ
   El {Γ} a = record { E = E.El a.E
+                    ; w = λ σ α → {!!} --coe (a.w σ α ⁻¹) {!!}
                     }
     where
       module Γ = Con Γ
       module a = TmS a
 
   ΠS : {Γ : Con} → (a : TmS Γ U) → (B : TyS (Γ ▶P El a)) → TyS Γ
   ΠS {Γ} a B = record { E = E.ΠS a.E B.E
-                      ; w = λ γ → (aS.E ᵃt) γ → B.w γ
+                      ; w = λ X → B.w X
                       }
     where
       module Γ = Con Γ
@@ -107,6 +108,7 @@ infixl 3 _▶P_
 
   ΠP : {Γ : Con} → (a : TmS Γ U) → (A : TyP (Γ ▶P El a)) → TyP Γ
   ΠP {Γ} a A = record { E = E.ΠP a.E A.E
+                      ; w = λ σ ϕ α αᵈ → A.w (σ E.,tP {!!}) (ϕ α)
                       }
     where
       module Γ = Con Γ
@@ -115,9 +117,9 @@ infixl 3 _▶P_
       module A = TyP A
 
   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 { E  = E.appS t.E
-                            ; w' = t.w'
-                            ; w  = λ σ α → t.w (E.π₁P {A = E.El a.E} σ) α
+  appS {Γ}{a}{B} t = record { E    = E.appS t.E
+                            ; hTy  = {!!}
+                            ; w    = λ σ α → t.w _ α ◾ {!!} --t.w (E.π₁P {A = E.El a.E} σ) α
                             }
     where
       module Γ = Con Γ
@@ -135,23 +137,24 @@ infixl 3 _▶P_
 
   _[_]TS : ∀{Γ Δ} → TyS Δ → Sub Γ Δ → TyS Γ
   _[_]TS B σ = record { E = B.E E.[ σ.E ]TS
-                      ; w = λ γ → B.w ((E.Sub.Ec σ.E ᵃs) γ)
+                      ; w = λ X → {!!}
                       }
     where
       module B = TyS B
       module σ = Sub σ
 
   _[_]TP : ∀{Γ Δ} → TyP Δ → Sub Γ Δ → TyP Γ
   _[_]TP A σ = record { E = A.E E.[ σ.E ]TP
+                      ; w = λ δ α → coe {!!} (A.w (σ.E E.∘ δ) α)
                       }
     where
       module A = TyP A
       module σ = Sub σ
 
   _[_]tS : ∀{Γ Δ}{A : TyS Δ} → TmS Δ A → (σ : Sub Γ Δ) → TmS Γ (A [ σ ]TS)
-  _[_]tS {Γ}{Δ}{A} a σ = record { E  = a.E E.[ σ.E ]tS
-                                ; w' = a.w' -- ???
-                                ; w  = λ δ α → {!!} ◾ a.w (σ.E E.∘ δ) α
+  _[_]tS {Γ}{Δ}{A} a σ = record { E   = a.E E.[ σ.E ]tS
+                                ; hTy = {!!}
+                                ; w   = λ δ α → {!!} ◾ a.w (σ.E E.∘ δ) α
                                 }
     where
       module A = TyS A
@@ -206,7 +209,10 @@ infixl 3 _▶P_
       module σ = Sub σ
 
   π₂S : ∀{Γ Δ}{B : TyS Δ}(σ : Sub Γ (Δ ▶S B)) → TmS Γ (B [ π₁S {B = B} σ ]TS)
-  π₂S {Γ}{Δ}{B} σ = record { E = E.π₂S {B = B} σ.E }
+  π₂S {Γ}{Δ}{B} σ = record { E   = E.π₂S {B = TyS.E B} σ.E
+                           ; hTy = {!!}
+                           ; w   = λ δ α → {!!}
+                           }
     where
       module σ = Sub σ