I FINALLY HAVE A SYNTAX !!!!

FFOLCompleteness.agda

@@ -0,0 +1,327 @@
+{-# OPTIONS --prop --rewriting #-}
+
+open import PropUtil
+
+module FFOLCompleteness where
+
+  open import Agda.Primitive
+  open import FinitaryFirstOrderLogic
+  open import ListUtil
+
+  record Family : Set (lsuc (ℓ¹)) where
+    field
+      World : Set ℓ¹
+      _≤_ : World → World → Prop
+      ≤refl : {w : World} → w ≤ w
+      ≤tran : {w w' w'' : World} → w ≤ w' → w' ≤ w'' → w ≤ w'
+      TM : World → Set ℓ¹
+      TM≤ : {w w' : World} → w ≤ w' → TM w → TM w'
+      REL : (w : World) → TM w → TM w → Prop ℓ¹
+      REL≤ : {w w' : World} → {t u : TM w} → (eq : w ≤ w') → REL w t u → REL w' (TM≤ eq t) (TM≤ eq u)
+    infixr 10 _∘_
+    Con = World → Set ℓ¹
+    Sub : Con → Con → Set ℓ¹
+    Sub Δ Γ = (w : World) → Δ w → Γ w
+    _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
+    α ∘ β = λ w γ → α w (β w γ)
+    id : {Γ : Con} → Sub Γ Γ
+    id = λ w γ → γ
+    ◇ : Con -- The initial object of the category
+    ◇ = λ w → ⊤ₛ
+    ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object
+    ε w Γ = ttₛ
+                                                                    
+    -- Functor Con → Set called Tm
+    Tm : Con → Set ℓ¹
+    Tm Γ = (w : World) → (Γ w) → TM w
+    _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms
+    t [ σ ]t = λ w → λ γ → t w (σ w γ)
+
+    -- Tm⁺
+    _▹ₜ : Con → Con
+    Γ ▹ₜ = λ w → (Γ w) × (TM w)
+    πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ
+    πₜ¹ σ = λ w → λ x → proj×₁ (σ w x)
+    πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ
+    πₜ² σ = λ w → λ x → proj×₂ (σ w x) 
+    _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ)
+    σ ,ₜ t = λ w → λ x → (σ w x) ,× (t w x)
+                                                                      
+    -- Functor Con → Set called For
+    For : Con → Set (lsuc ℓ¹)
+    For Γ = (w : World) → (Γ w) → Prop ℓ¹
+    _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms
+    F [ σ ]f = λ w → λ x → F w (σ w x)
+
+    -- Formulas with relation on terms
+    R : {Γ : Con} → Tm Γ → Tm Γ → For Γ
+    R t u = λ w → λ γ → REL w (t w γ) (u w γ)
+
+                                                                                                        
+    -- Proofs
+    _⊢_ : (Γ : Con) → For Γ → Prop ℓ¹
+    Γ ⊢ F = ∀ w (γ : Γ w) →  F w γ
+    _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms
+    prf [ σ ]p = λ w → λ γ → prf w (σ w γ)
+    -- Equalities below are useless because Γ ⊢ F is in prop
+    -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf
+    -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
+                                                                                                                               
+    -- → Prop⁺
+    _▹ₚ_ : (Γ : Con) → For Γ → Con
+    Γ ▹ₚ F = λ w → (Γ w) ×'' (F w)
+    πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
+    πₚ¹ σ w δ = proj×''₁ (σ w δ)
+    πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f)
+    πₚ² σ w δ = proj×''₂ (σ w δ)
+    _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
+    _,ₚ_ {F = F} σ pf w δ = (σ w δ) ,×'' pf w δ
+    
+                                                                                                      
+                                                                                                      
+    -- Implication
+    _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
+    F ⇒ G = λ w → λ γ → (∀ w' → w ≤ w' → (F w γ) → (G w γ))
+    
+    -- Forall
+    ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
+    ∀∀ F = λ w → λ γ → ∀ t → F w (γ ,× t)
+                                                                                                                           
+    -- Lam & App
+    lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
+    lam prf = λ w γ w' s h → prf w (γ ,×'' h)
+    app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
+    app prf prf' = λ w γ → prf w γ w ≤refl (prf' w γ)
+    -- Again, we don't write the _[_]p equalities as everything is in Prop
+                                                                      
+    -- ∀i and ∀e
+    ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
+    ∀i p w γ = λ t → p w (γ ,× t)
+    ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
+    ∀e p {t} w γ = p w γ (t w γ)
+
+
+    tod : FFOL
+    tod = record
+      { Con = Con
+      ; Sub = Sub
+      ; _∘_ = _∘_
+      ; ∘-ass = refl
+      ; id = id
+      ; idl = refl
+      ; idr = refl
+      ; ◇ = ◇
+      ; ε = ε
+      ; ε-u = refl
+      ; Tm = Tm
+      ; _[_]t = _[_]t
+      ; []t-id = refl
+      ; []t-∘ = refl
+      ; _▹ₜ = _▹ₜ
+      ; πₜ¹ = πₜ¹
+      ; πₜ² = πₜ²
+      ; _,ₜ_ = _,ₜ_
+      ; πₜ²∘,ₜ = refl
+      ; πₜ¹∘,ₜ = refl
+      ; ,ₜ∘πₜ = refl
+      ; ,ₜ∘ = refl
+      ; For = For
+      ; _[_]f = _[_]f
+      ; []f-id = refl
+      ; []f-∘ = refl
+      ; _⊢_ = _⊢_
+      ; _[_]p = _[_]p
+      ; _▹ₚ_ = _▹ₚ_
+      ; πₚ¹ = πₚ¹
+      ; πₚ² = πₚ²
+      ; _,ₚ_ = _,ₚ_
+      ; ,ₚ∘πₚ = refl
+      ; πₚ¹∘,ₚ = refl
+      ; ,ₚ∘ = refl
+      ; _⇒_ = _⇒_
+      ; []f-⇒ = refl
+      ; ∀∀ = ∀∀
+      ; []f-∀∀ = refl
+      ; lam = lam
+      ; app = app
+      ; ∀i = ∀i
+      ; ∀e = ∀e
+      ; R = R
+      ; R[] = refl
+      }
+
+  record Presheaf : Set (lsuc (ℓ¹)) where
+    field
+      World : Set ℓ¹
+      _≤_ : World → World → Set ℓ¹ -- arrows
+      ≤refl : {w : World} → w ≤ w -- id arrow
+      ≤tran : {w w' w'' : World} → w ≤ w' → w' ≤ w'' → w ≤ w'' -- arrow composition
+      ≤-ass : {w w' w'' w''' : World}{a : w ≤ w'}{b : w' ≤ w''}{c : w'' ≤ w'''}
+        → (≤tran (≤tran a b) c) ≡ (≤tran a (≤tran b c))
+      ≤-idl : {w w' : World} → {a : w ≤ w'} → ≤tran (≤refl {w}) a ≡ a
+      ≤-idr : {w w' : World} → {a : w ≤ w'} → ≤tran a (≤refl {w'}) ≡ a
+      TM : World → Set ℓ¹
+      TM≤ : {w w' : World} → w ≤ w' → TM w → TM w'
+      REL : (w : World) → TM w → TM w → Prop ℓ¹
+      REL≤ : {w w' : World} → {t u : TM w} → (eq : w ≤ w') → REL w t u → REL w' (TM≤ eq t) (TM≤ eq u)
+    infixr 10 _∘_
+    Con = World → Set ℓ¹
+    Sub : Con → Con → Set ℓ¹
+    Sub Δ Γ = (w : World) → Δ w → Γ w
+    _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
+    α ∘ β = λ w γ → α w (β w γ)
+    id : {Γ : Con} → Sub Γ Γ
+    id = λ w γ → γ
+    ◇ : Con -- The initial object of the category
+    ◇ = λ w → ⊤ₛ
+    ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object
+    ε w Γ = ttₛ
+                                                                    
+    -- Functor Con → Set called Tm
+    Tm : Con → Set ℓ¹
+    Tm Γ = (w : World) → (Γ w) → TM w
+    _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms
+    t [ σ ]t = λ w → λ γ → t w (σ w γ)
+
+    -- Tm⁺
+    _▹ₜ : Con → Con
+    Γ ▹ₜ = λ w → (Γ w) × (TM w)
+    πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ
+    πₜ¹ σ = λ w → λ x → proj×₁ (σ w x)
+    πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ
+    πₜ² σ = λ w → λ x → proj×₂ (σ w x) 
+    _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ)
+    σ ,ₜ t = λ w → λ x → (σ w x) ,× (t w x)
+                                                                      
+    -- Functor Con → Set called For
+    For : Con → Set (lsuc ℓ¹)
+    For Γ = (w : World) → (Γ w) → Prop ℓ¹
+    _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms
+    F [ σ ]f = λ w → λ x → F w (σ w x)
+
+    -- Formulas with relation on terms
+    R : {Γ : Con} → Tm Γ → Tm Γ → For Γ
+    R t u = λ w → λ γ → REL w (t w γ) (u w γ)
+
+                                                                                                        
+    -- Proofs
+    _⊢_ : (Γ : Con) → For Γ → Prop ℓ¹
+    Γ ⊢ F = ∀ w (γ : Γ w) →  F w γ
+    _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms
+    prf [ σ ]p = λ w → λ γ → prf w (σ w γ)
+    -- Equalities below are useless because Γ ⊢ F is in prop
+    -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf
+    -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
+                                                                                                                               
+    -- → Prop⁺
+    _▹ₚ_ : (Γ : Con) → For Γ → Con
+    Γ ▹ₚ F = λ w → (Γ w) ×'' (F w)
+    πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
+    πₚ¹ σ w δ = proj×''₁ (σ w δ)
+    πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f)
+    πₚ² σ w δ = proj×''₂ (σ w δ)
+    _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
+    _,ₚ_ {F = F} σ pf w δ = (σ w δ) ,×'' pf w δ
+    
+                                                                                                      
+                                                                                                      
+    -- Implication
+    _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
+    F ⇒ G = λ w → λ γ → (∀ w' → w ≤ w' → (F w γ) → (G w γ))
+    
+    -- Forall
+    ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
+    ∀∀ F = λ w → λ γ → ∀ t → F w (γ ,× t)
+                                                                                                                           
+    -- Lam & App
+    lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
+    lam prf = λ w γ w' s h → prf w (γ ,×'' h)
+    app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
+    app prf prf' = λ w γ → prf w γ w ≤refl (prf' w γ)
+    -- Again, we don't write the _[_]p equalities as everything is in Prop
+                                                                      
+    -- ∀i and ∀e
+    ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
+    ∀i p w γ = λ t → p w (γ ,× t)
+    ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
+    ∀e p {t} w γ = p w γ (t w γ)
+
+
+    tod : FFOL
+    tod = record
+      { Con = Con
+      ; Sub = Sub
+      ; _∘_ = _∘_
+      ; ∘-ass = refl
+      ; id = id
+      ; idl = refl
+      ; idr = refl
+      ; ◇ = ◇
+      ; ε = ε
+      ; ε-u = refl
+      ; Tm = Tm
+      ; _[_]t = _[_]t
+      ; []t-id = refl
+      ; []t-∘ = refl
+      ; _▹ₜ = _▹ₜ
+      ; πₜ¹ = πₜ¹
+      ; πₜ² = πₜ²
+      ; _,ₜ_ = _,ₜ_
+      ; πₜ²∘,ₜ = refl
+      ; πₜ¹∘,ₜ = refl
+      ; ,ₜ∘πₜ = refl
+      ; ,ₜ∘ = refl
+      ; For = For
+      ; _[_]f = _[_]f
+      ; []f-id = refl
+      ; []f-∘ = refl
+      ; _⊢_ = _⊢_
+      ; _[_]p = _[_]p
+      ; _▹ₚ_ = _▹ₚ_
+      ; πₚ¹ = πₚ¹
+      ; πₚ² = πₚ²
+      ; _,ₚ_ = _,ₚ_
+      ; ,ₚ∘πₚ = refl
+      ; πₚ¹∘,ₚ = refl
+      ; ,ₚ∘ = refl
+      ; _⇒_ = _⇒_
+      ; []f-⇒ = refl
+      ; ∀∀ = ∀∀
+      ; []f-∀∀ = refl
+      ; lam = lam
+      ; app = app
+      ; ∀i = ∀i
+      ; ∀e = ∀e
+      ; R = R
+      ; R[] = refl
+      }
+
+  -- Completeness proof
+
+  -- We first build our universal Kripke model
+  
+  module ComplenessProof where
+    
+    -- We have a model, we construct the Universal Presheaf model of this model
+    open import FFOLInitial as I
+    
+    World : Set₁
+    World = I.Con
+    
+    _≤_ : World → World → Set₁
+    Γ ≤ Δ = I.Sub Γ Δ
+
+    UP : Presheaf
+    UP = record
+           { World = I.Con
+           ; _≤_ = I.Sub
+           ; ≤refl = I.id
+           ; ≤tran = λ σ σ' → σ' I.∘ σ
+           ; ≤-ass = λ {w}{w'}{w''}{w'''}{a}{b}{c} → ≡sym I.∘-ass
+           ; ≤-idl = I.idr
+           ; ≤-idr = I.idl
+           ; TM = λ Γ → I.Tm (Con.t Γ)
+           ; TM≤ = {!!}
+           ; REL = λ Γ t u → {!I.r t u!}
+           ; REL≤ = {!!}
+           }

FFOLInitial.agda

@@ -134,7 +134,8 @@ module FFOLInitial where
   ∘ₜ-ass {α = α} {β} {γ ,ₜ x} = cong₂ _,ₜ_ ∘ₜ-ass (≡sym ([]t-∘ {t = x}))
   []f-∀∀ : {A : For (Γₜ ▹t⁰)} → {σₜ : Subt Δₜ Γₜ} → (∀∀ A) [ σₜ ]f ≡ (∀∀ (A [ (σₜ ∘ₜ πₜ¹ idₜ) ,ₜ πₜ² idₜ ]f))
   []f-∀∀ {A = A} = cong ∀∀ (cong (_[_]f A) (cong₂ _,ₜ_ (≡tran (cong wkₜσt (≡sym σ-idr)) (≡sym lem3)) refl))
-
+  εₜ-u : {σₜ : Subt Γₜ ◇t} → σₜ ≡ εₜ
+  εₜ-u {σₜ = εₜ} = refl
 
   data Conp : Cont → Set₁ -- pu tit in Prop
   variable
@@ -240,8 +241,6 @@ module FFOLInitial where
   ∈ₚ*→Sub zero∈ₚ* = εₚ
   ∈ₚ*→Sub (next∈ₚ* x s) = ∈ₚ*→Sub s ,ₚ var x
 
-  idₚ : Subp {Δₜ} Δₚ Δₚ
-  idₚ = ∈ₚ*→Sub refl∈ₚ*
 
   wkₚp : {A : For Δₜ} → Δₚ ∈ₚ* Δₚ' → Pf (con Δₜ Δₚ) A → Pf (con Δₜ Δₚ') A
   wkₚp s (var pv) = var (mon∈ₚ∈ₚ* pv s)
@@ -253,8 +252,23 @@ module FFOLInitial where
   lliftₚ s εₚ = εₚ
   lliftₚ s (σₚ ,ₚ pf) = lliftₚ s σₚ ,ₚ wkₚp s pf
 
+  wkₚσt : {Δₜ : Cont} {Δₚ Γₚ : Conp Δₜ}{A : For Δₜ} → Subp {Δₜ} Δₚ Γₚ → Subp {Δₜ} (Δₚ ▹p⁰ A) Γₚ
+  wkₚσt εₚ = εₚ
+  wkₚσt (σₚ ,ₚ pf) = (wkₚσt σₚ) ,ₚ wkₚp (right∈ₚ* refl∈ₚ*) pf
+  --wkₜσt-wkₜt : {tv : TmVar Γₜ} → {σ : Subt Δₜ Γₜ} → wkₜt (var tv [ σ ]t) ≡ var tv [ wkₜσt σ ]t
+  --wkₜσt-wkₜt {tv = tvzero} {σ = σ ,ₜ x} = refl
+  --wkₜσt-wkₜt {tv = tvnext tv} {σ = σ ,ₜ x} = wkₜσt-wkₜt {tv = tv} {σ = σ}
+  
+  -- From a substitution into n variables, we construct a substitution from n+1 variables to n+1 variables which maps it to itself
+  -- i.e. 0 -> 0 and for all i ->(old) σ(i) we get i+1 -> σ(i)+1
+  liftₚσ : {Δₜ : Cont}{Δₚ Γₚ : Conp Δₜ}{A : For Δₜ} → Subp {Δₜ} Δₚ Γₚ → Subp {Δₜ} (Δₚ ▹p⁰ A) (Γₚ ▹p⁰ A)
+  liftₚσ σ = (wkₚσt σ) ,ₚ (var pvzero)
 
+  idₚ : Subp {Δₜ} Δₚ Δₚ
+  idₚ {Δₚ = ◇p} = εₚ
+  idₚ {Δₚ = Δₚ ▹p⁰ x} = liftₚσ (idₚ {Δₚ = Δₚ})
 
+  
 
 
 
@@ -282,7 +296,6 @@ module FFOLInitial where
   εₚ [ σₜ ]σₚ = εₚ
   (σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ)
 
-
   lem9 : (Δₚ [ wkₜσt idₜ ]c) ≡ (Δₚ ▹tp)
   lem9 {Δₚ = ◇p} = refl
   lem9 {Δₚ = Δₚ ▹p⁰ x} = cong₂ _▹p⁰_ lem9 refl
@@ -302,33 +315,118 @@ module FFOLInitial where
   _∘ₚ_ : {Γₚ Δₚ Ξₚ : Conp Δₜ} → Subp {Δₜ} Δₚ Ξₚ → Subp {Δₜ} Γₚ Δₚ → Subp {Δₜ} Γₚ Ξₚ
   εₚ ∘ₚ β = εₚ
   (α ,ₚ pf) ∘ₚ β = (α ∘ₚ β) ,ₚ (pf [ β ]p)
+  ε-u : {Γₚ : Conp Γₜ} → {σ : Subp Γₚ ◇p} → σ ≡ εₚ {Δₚ = Γₚ}
+  ε-u {σ = εₚ} = refl
+  lemJ : {Δₜ : Cont}{Δₚ : Conp Δₜ}{A : For Δₜ} → Pf (con Δₜ Δₚ) A → (Pf (con Δₜ (Δₚ [ idₜ ]c)) (A [ idₜ ]f))
+  lemJ {Δₜ}{Δₚ}{A} pf = substP (Pf (con Δₜ (Δₚ [ idₜ ]c))) (≡sym []f-id) (substP (λ Ξₚ → Pf (con Δₜ Ξₚ) A) (≡sym []c-id) pf)
+  []σₚ-id : {σₚ : Subp {Δₜ} Δₚ Δₚ'} → coe (cong₂ Subp []c-id []c-id) (σₚ [ idₜ ]σₚ) ≡ σₚ
+  []σₚ-id {σₚ = εₚ} = ε-u
+  []σₚ-id {Δₜ}{Δₚ}{Δₚ' ▹p⁰ A} {σₚ = σₚ ,ₚ x} = substP (λ ξ → coe (cong₂ Subp []c-id []c-id) (ξ ,ₚ (x [ idₜ ]pₜ)) ≡ (σₚ ,ₚ x)) (≡sym (coeshift ([]σₚ-id)))
+    (≡sym (coeshift {eq = cong₂ Subp (≡sym []c-id) (≡sym []c-id)}
+    (substfpoly'' {A = (Conp Δₜ) × (Conp Δₜ)}{P = λ W F → Subp (proj×₁ W) ((proj×₂ W) ▹p⁰ F)}{R = λ W → Subp (proj×₁ W) (proj×₂ W)}{Q = λ W F → Pf (con Δₜ (proj×₁ W)) F}{α = Δₚ ,× Δₚ'}{ε = A}{eq = ×≡ (≡sym []c-id) (≡sym []c-id)}{eq'' = ≡sym []f-id}{f = λ {W} {F} ξ pf → _,ₚ_ ξ pf}{x = σₚ}{y = x})))
+  []σₚ-∘ : {Ξₚ Ξₚ' : Conp Ξₜ}{α : Subt Δₜ Ξₜ} {β : Subt Γₜ Δₜ} {σₚ : Subp {Ξₜ} Ξₚ Ξₚ'}
+    --{eq₅ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ]c) ≡ Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)}
+    → coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) ((σₚ [ α ]σₚ) [ β ]σₚ) ≡ σₚ [ α ∘ₜ β ]σₚ 
+  []σₚ-∘ {σₚ = εₚ} = ε-u
+  []σₚ-∘ {Ξₜ}{Δₜ}{Γₜ}{Ξₚ}{Δₚ' ▹p⁰ A}{α}{β}{σₚ = σₚ ,ₚ pf} =
+    substP (λ ξ → coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) (ξ ,ₚ ((pf [ α ]pₜ) [ β ]pₜ)) ≡ ((σₚ [ α ∘ₜ β ]σₚ) ,ₚ (pf [ α ∘ₜ β ]pₜ))) (≡sym (coeshift []σₚ-∘))
+    (≡sym (coeshift {eq = cong₂ Subp []c-∘ []c-∘}
+    (substfpoly''
+      {A = (Conp Γₜ) × (Conp Γₜ)}
+      {P = λ W F → Subp (proj×₁ W) ((proj×₂ W) ▹p⁰ F)}
+      {R = λ W → Subp (proj×₁ W) (proj×₂ W)}
+      {Q = λ W F → Pf (con Γₜ (proj×₁ W)) F}
+      {eq = cong₂ _,×_ []c-∘ []c-∘}
+      {eq'' = []f-∘ {α = β} {β = α} {F = A}}
+      {f = λ {W} {F} ξ pf → _,ₚ_ ξ pf}{x = σₚ [ α ∘ₜ β ]σₚ}{y = pf [ α ∘ₜ β ]pₜ})
+    ))
+  wkₚ∘, : {Δₜ : Cont}{Γₚ Δₚ Ξₚ : Conp Δₜ}{α : Subp {Δₜ} Γₚ Δₚ}{β : Subp {Δₜ} Ξₚ Γₚ}{A : For Δₜ}{pf : Pf (con Δₜ Ξₚ) A} → (wkₚσt α) ∘ₚ (β ,ₚ pf) ≡ (α ∘ₚ β)
+  wkₚ∘, {α = εₚ} = refl
+  wkₚ∘, {α = α ,ₚ pf} {β = β} {pf = pf'} = cong (λ ξ → ξ ,ₚ (pf [ β ]p)) wkₚ∘,
   idlₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → (idₚ {Δₚ = Δₚ}) ∘ₚ σₚ ≡ σₚ
-  idlₚ {Δₚ = ◇p} = ?
+  idlₚ {Δₚ = ◇p} {εₚ} = refl
-  idlₚ {Δₚ = Δₚ ▹p⁰ x} = ?
+  idlₚ {Δₚ = Δₚ ▹p⁰ pf} {σₚ ,ₚ pf'} = cong (λ ξ → ξ ,ₚ pf') (≡tran wkₚ∘, (idlₚ {σₚ = σₚ}))
   idrₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} →  σₚ ∘ₚ (idₚ {Δₚ = Γₚ}) ≡ σₚ
-  idrₚ = {!!}  
+  idrₚ {σₚ = εₚ} = refl
+  idrₚ {σₚ = σₚ ,ₚ prf} = cong (λ X → X ,ₚ prf) (idrₚ {σₚ = σₚ})
+  wkₚ[] : {σₜ : Subt Γₜ Δₜ} {σₚ : Subp Δₚ Δₚ'} {A : For Δₜ} → (wkₚσt {A = A} σₚ) [ σₜ ]σₚ ≡ wkₚσt (σₚ [ σₜ ]σₚ)
+  wkₚ[] {σₚ = εₚ} = refl
+  wkₚ[] {σₚ = σₚ ,ₚ x} = cong (λ ξ → ξ ,ₚ _) (wkₚ[] {σₚ = σₚ})
+  idₚ[] : {σₜ : Subt Γₜ Δₜ} → ((idₚ {Δₜ} {Δₚ}) [ σₜ ]σₚ) ≡ idₚ {Γₜ} {Δₚ [ σₜ ]c}
+  idₚ[] {Δₚ = ◇p} = refl
+  idₚ[] {Δₚ = Δₚ ▹p⁰ A} = cong (λ ξ → ξ ,ₚ var pvzero) (≡tran wkₚ[] (cong wkₚσt idₚ[]))
+  
 
   id : Sub Γ Γ
   id {Γ} = sub idₜ (subst (Subp _) (≡sym []c-id) idₚ)
   _∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
   sub αₜ αₚ ∘ sub βₜ βₚ = sub (αₜ ∘ₜ βₜ) (subst (Subp _) (≡sym []c-∘) (αₚ [ βₜ ]σₚ) ∘ₚ βₚ)
   idl : {Γ Δ : Con} {σ : Sub Γ Δ} →  (id {Δ}) ∘ σ ≡ σ
-  idl {σ = sub σₜ σₚ} = cong₂' sub σ-idl {!!}
+  idl {Δ = Δ} {σ = sub σₜ σₚ} = cong₂' sub σ-idl (≡tran (substfpoly {α = ((Con.p Δ) [ idₜ ∘ₜ σₜ ]c)} {β = ((Con.p Δ) [ σₜ ]c)} {eq = cong (λ ξ → Con.p Δ [ ξ ]c) σ-idl} {f = λ {Ξₚ} ξ → _∘ₚ_ {Ξₚ = Ξₚ} ξ σₚ}) (≡tran (cong₂ _∘ₚ_ (≡tran³ coecoe-coe (substfpoly {eq = []c-id} {f = λ {Ξₚ} ξ → _[_]σₚ {Δₚ = Con.p Δ} {Δₚ' = Ξₚ} ξ σₜ}) (cong (λ ξ → ξ [ σₜ ]σₚ) coeaba) idₚ[]) refl) idlₚ))
+  lemK : {Γ Δ : Con}{σₜ : Subt (Con.t Γ) (Con.t Δ)}{σₚ : Subp (Con.p Γ [ idₜ ]c) ((Con.p Δ [ σₜ ]c)[ idₜ ]c)}
+    {eq1 : Subp (Con.p Γ) ((Con.p Δ [ σₜ ]c) [ idₜ ]c) ≡ Subp (Con.p Γ) (Con.p Δ [ σₜ ]c)}
+    {eq2 : Subp (Con.p Γ) (Con.p Γ) ≡ Subp (Con.p Γ) (Con.p Γ [ idₜ ]c)}
+    {eq3 : Subp (Con.p Γ [ idₜ ]c) ((Con.p Δ [ σₜ ]c)[ idₜ ]c) ≡ Subp (Con.p Γ) (Con.p Δ [ σₜ ]c)}
+    → coe eq1 (σₚ ∘ₚ coe eq2 idₚ)
+      ≡ (coe eq3 σₚ ∘ₚ idₚ)
+  lemK {Γ}{Δ}{σₚ = σₚ}{eq1}{eq2}{eq3} = substP (λ X → coe eq1 (X ∘ₚ coe eq2 idₚ) ≡  (coe eq3 σₚ ∘ₚ idₚ)) (coeaba {eq1 = eq3}{eq2 = ≡sym eq3}) (coep∘ {p = λ {Γₚ}{Δₚ}{Ξₚ} x y → _∘ₚ_ {Δₚ = Γₚ} x y} {eq1 = refl}{eq2 = ≡sym []c-id}{eq3 = ≡sym []c-id})
   idr : {Γ Δ : Con} {σ : Sub Γ Δ} →  σ ∘ (id {Γ}) ≡ σ
-  idr {σ = sub σₜ σₚ} = cong₂' sub σ-idr {!!}
+  idr {Γ} {Δ} {σ = sub σₜ σₚ} = cong₂' sub σ-idr (≡tran⁴ (cong (coe _) (≡sym (substfpoly {eq = ≡sym ([]c-∘ {α = σₜ} {β = idₜ}{Ξₚ = Con.p Δ})} {f = λ {Ξₚ} ξ → _∘ₚ_ {Ξₚ = Ξₚ} ξ (coe (cong (Subp (Con.p Γ)) (≡sym []c-id)) idₚ)} {x = σₚ [ idₜ ]σₚ}))) coecoe-coe lemK idrₚ []σₚ-id)
-  {-
+  ∘ₚ-ass : {Γₚ Δₚ Ξₚ Ψₚ : Conp Γₜ}{αₚ : Subp Γₚ Δₚ}{βₚ : Subp Δₚ Ξₚ}{γₚ : Subp Ξₚ Ψₚ} → (γₚ ∘ₚ βₚ) ∘ₚ αₚ ≡ γₚ ∘ₚ (βₚ ∘ₚ αₚ)
-  ∘ₚ-ass :
+  ∘ₚ-ass {γₚ = εₚ} = refl
+  ∘ₚ-ass {αₚ = αₚ} {βₚ} {γₚ ,ₚ x} = cong (λ ξ → ξ ,ₚ (x [ βₚ ∘ₚ αₚ ]p)) ∘ₚ-ass
+
+  lemG' :
+    {Γₜ Δₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Δₜ}{Ψₚ : Conp Δₜ}
+    {αₜ : Subt Γₜ Δₜ}{γₚ : Subp Ξₚ Ψₚ}{βₚ : Subp Δₚ Ξₚ}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)}
+    → ((γₚ ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ ≡ (γₚ [ αₜ ]σₚ) ∘ₚ ((βₚ [ αₜ ]σₚ) ∘ₚ αₚ)
+  lemG' {γₚ = εₚ} = refl
+  lemG' {αₜ = αₜ}{γₚ ,ₚ x}{βₚ}{αₚ} = cong (λ ξ → ξ ,ₚ (((x [ βₚ ]p) [ αₜ ]pₜ) [ αₚ ]p)) (lemG' {γₚ = γₚ})
+  lemG : 
     {Γₜ Δₜ Ξₜ Ψₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Ξₜ}{Ψₚ : Conp Ψₜ}
     {αₜ : Subt Γₜ Δₜ}{βₜ : Subt Δₜ Ξₜ}{γₜ : Subt Ξₜ Ψₜ}{γₚ : Subp Ξₚ (Ψₚ [ γₜ ]c)}{βₚ : Subp Δₚ (Ξₚ [ βₜ ]c)}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)}
-    {eq₁ : Subp (Δₚ [ αₜ ]c) ((Ψₚ [ γₜ ∘ₜ βₜ ]c)[ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c)}
+    {eq₁ : Subp Γₚ (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c) ≡ Subp Γₚ (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)}
-    {eq₂ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c)[ βₜ ]c) ≡  Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)}
+    {eq₂ : Subp (Δₚ [ αₜ ]c) ((Ψₚ [ γₜ ∘ₜ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c)}
-    {eq₃ : Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ∘ₜ αₜ ]c) ≡ {!Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)!}}
+    {eq₃ : Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ∘ₜ αₜ ]c) ≡ Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)}
     {eq₄ : Subp (Δₚ [ αₜ ]c) ((Ξₚ [ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ξₚ [ βₜ ∘ₜ αₜ ]c)}
-    → (coe eq₁ (((coe eq₂ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ) ≡ (coe eq₃ (γₚ [ βₜ ∘ₜ αₜ ]σₚ)) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ) ∘ₚ αₚ))
+    {eq₅ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ]c) ≡ Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)}
-  -}
+    → coe eq₁ ((coe eq₂ (((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ)) ∘ₚ αₚ) ≡ (coe eq₃ (γₚ [ βₜ ∘ₜ αₜ ]σₚ)) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ)
-  postulate ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α)
+  lemG {Γₜ}{Δₜ}{Ξₜ}{Ψₜ}{Γₚ}{Δₚ}{Ξₚ}{Ψₚ}{αₜ = αₜ}{βₜ}{γₜ}{γₚ}{βₚ}{αₚ}{eq₁}{eq₂}{eq₃}{eq₄}{eq₅} =
-  -- ∘-ass {Γ}{Δ}{Ξ}{Ψ}{α = sub αₜ αₚ} {β = sub βₜ βₚ} {γ = sub γₜ γₚ} = {!Subp (Con.p Ξ [ βₜ ∘ₜ αₜ ]c) (Con.p Ψ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)!}
+    substP (λ X → coe eq₁ ((coe eq₂ (((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ)) ∘ₚ αₚ) ≡ (coe eq₃ X) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ)) []σₚ-∘ (
-
+    ≡tran⁵
+    (cong (coe eq₁) (≡tran (
+      ≡sym (substfpoly
+        {R = λ X → Subp (Δₚ [ αₜ ]c) X}
+        {eq = ≡sym []c-∘}
+        {f = λ ξ → ξ ∘ₚ αₚ}
+        {x = ((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ}))
+      (cong (coe (cong (λ z → Subp Γₚ z) (≡sym []c-∘)))
+      (≡sym (substfpoly
+        {R = λ X → Subp (Ξₚ [ βₜ ]c) X}
+        {eq = ≡sym []c-∘}
+        {f = λ ξ → ((ξ ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ}
+        {x = γₚ [ βₜ ]σₚ}
+      )))
+      ))
+    (≡tran coecoe-coe coecoe-coe)
+    (cong (coe  (≡tran (cong (λ z → Subp Γₚ (z [ αₜ ]c)) (≡sym []c-∘)) (≡tran (cong (λ z → Subp Γₚ z) (≡sym []c-∘)) eq₁))) lemG')
+    (≡sym coecoe-coe)
+    (cong (coe (cong (λ z → Subp Γₚ z) (≡sym []c-∘))) (substppoly
+      {A = (Conp Γₜ) × (Conp Γₜ)}
+      {R = λ W → Subp (proj×₁ W) (proj×₂ W)}
+      {Q = λ W → Subp (Δₚ [ αₜ ]c) (proj×₁ W)}
+      {eq = ×≡ (≡sym []c-∘) (≡sym []c-∘)}
+      {f = λ x y → x ∘ₚ (y ∘ₚ αₚ)}
+      {x = (γₚ [ βₜ ]σₚ) [ αₜ ]σₚ}
+      {y = βₚ [ αₜ ]σₚ}
+    ))(substfpoly
+      {R = λ X → Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) X}
+      {eq = ≡sym []c-∘}
+      {f = λ {τ} ξ → (ξ ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ))}
+      {x = (coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) ((γₚ [ βₜ ]σₚ) [ αₜ ]σₚ))}
+    ))
+  ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α)
+  ∘-ass {Γ}{Δ}{Ξ}{Ψ}{α = sub αₜ αₚ} {β = sub βₜ βₚ} {γ = sub γₜ γₚ} = cong₂' sub ∘ₜ-ass lemG
 
   -- SUB-ization
 
@@ -380,18 +478,11 @@ module FFOLInitial where
 
   ,ₚ∘πₚ : {Γ Δ : Con} → {F : For (Con.t Γ)} → {σ : Sub Δ (Γ ▹p F)} → (πₚ¹* σ) ,ₚ* (πₚ² σ) ≡ σ
   ,ₚ∘πₚ {σ = sub σₜ (σₚ ,ₚ p)} = refl
-  --funlol : {Γₜ Δₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Ξₜ}{σₜ : Subt Γₜ Ξₜ}{δₜ : Subt Δₜ Γₜ}{δₚ : Subp Δₚ (Γₚ [ δₜ ]c)}{A : For Ξₜ}{prf : Pf (con Δₜ (Γₚ [ δₜ ]c)) ((A [ σₜ ∘ₜ δₜ ]f))} → Subp {Δₜ} (Γₚ [ δₜ ]c) ((Ξₚ [ σₜ ∘ₜ δₜ ]c) ▹p⁰ ((A [ σₜ ]f) [ δₜ ]f)) → Subp {Δₜ} (Δₚ) ((Ξₚ [ σₜ ∘ₜ δₜ ]c) ▹p⁰ (A [ σₜ ∘ₜ δₜ ]f))
+  ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For (Con.t Ξ)}{prf : Pf Γ (F [ Sub.t σ ]f)}
-  --funlol {Γₚ = Γₚ} {Ξₚ = Ξₚ} {σₜ = σₜ} {δₜ = δₜ} {δₚ = δₚ} {prf = prf} (ξ ,ₚ pf) = ((subst (λ X → Subp (Γₚ [ δₜ ]c) ((Ξₚ [ σₜ ∘ₜ δₜ ]c) ▹p⁰ X)) (≡sym []f-∘) ξ) ,ₚ ?) ∘ₚ δₚ
+      → (σ ,ₚ* prf) ∘ δ ≡ (σ ∘ δ) ,ₚ* (substP (λ F → Pf Δ F) (≡sym []f-∘) ((prf [ Sub.t δ ]pₜ) [ Sub.p δ ]p))
-  postulate ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For (Con.t Ξ)}{prf : Pf Γ (F [ Sub.t σ ]f)} → (σ ,ₚ* prf) ∘ δ ≡ (σ ∘ δ) ,ₚ* (substP (λ F → Pf Δ F) (≡sym []f-∘) ((prf [ Sub.t δ ]pₜ) [ Sub.p δ ]p))
+  ,ₚ∘ {Γ}{Δ}{Ξ}{σ = sub σₜ σₚ} {sub δₜ δₚ} {F = A} {prf} = cong (sub (σₜ ∘ₜ δₜ)) (cong (λ ξ → ξ ∘ₚ δₚ)
-  {-,ₚ∘ {Γ = Γ} {Δ = Δ} {σ = sub σₜ σₚ} {sub δₜ δₚ} {F = A} {prf} = cong (sub (σₜ ∘ₜ δₜ)) (cong {!funlol!} 
+    (substfpoly⁴ {P = λ W → Subp (Con.p Γ [ δₜ ]c) ((proj×₁ W) ▹p⁰ (proj×₂ W))}{R = λ W → Subp (Con.p Γ [ δₜ ]c) (proj×₁ W)}{Q = λ W → Pf (con (Con.t Δ) (Con.p Γ [ δₜ ]c)) (proj×₂ W)}{α = ((Con.p Ξ [ σₜ ]c) [ δₜ ]c) ,× ((A [ σₜ ]f) [ δₜ ]f)}{eq = cong₂ _,×_ (≡sym []c-∘) (≡sym []f-∘)}{f = λ ξ p → ξ ,ₚ p} {x = σₚ [ δₜ ]σₚ}{y = prf [ δₜ ]pₜ})) -- 
-    (substfpoly
+  
-      {P = λ X → Subp (Con.p Γ [ δₜ ]c) (X ▹p⁰ ((A [ σₜ ]f) [ δₜ ]f))}
-      {R = λ X → Subp (Con.p Γ [ δₜ ]c) X}
-      {eq = ≡sym []c-∘}
-      {f = λ ξ → ξ ,ₚ (prf [ δₜ ]pₜ)}
-      {x = σₚ [ δₜ ]σₚ}
-    ))
-  -}
   --_,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹t)
   --πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t
   --πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ
@@ -415,11 +506,11 @@ module FFOLInitial where
     ; _∘_ = _∘_
     ; ∘-ass = ∘-ass
     ; id = id
-    ; idl = {!!}
+    ; idl = idl
-    ; idr = {!!}
+    ; idr = idr
     ; ◇ = ◇
     ; ε = sub εₜ εₚ
-    ; ε-u = {!!}
+    ; ε-u = cong₂' sub εₜ-u ε-u
     ; Tm = λ Γ → Tm (Con.t Γ)
     ; _[_]t = λ t σ → t [ Sub.t σ ]t
     ; []t-id = []t-id
@@ -438,8 +529,8 @@ module FFOLInitial where
     ; []f-∘ = []f-∘
     ; R = r
     ; R[] = refl
-    ; _⊢_ = λ Γ A → Pf Γ A
+    ; _⊢_ = Pf
-    ; _[_]p = λ {Γ}{Δ}{F} pf σ → (pf [ Sub.t σ ]pₜ) [ Sub.p σ ]p
+    ; _[_]p = λ pf σ → (pf [ Sub.t σ ]pₜ) [ Sub.p σ ]p
     ; _▹ₚ_ = _▹p_
     ; πₚ¹ = πₚ¹*
     ; πₚ² = πₚ²

PropUtil.agda

@@ -78,10 +78,16 @@ module PropUtil where
   ≡tran² : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₀ ≡ a₃
   ≡tran³ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₀ ≡ a₄
   ≡tran⁴ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₀ ≡ a₅
+  ≡tran⁵ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ a₆ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₅ ≡ a₆ → a₀ ≡ a₆
+  ≡tran⁶ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₅ ≡ a₆ → a₆ ≡ a₇ → a₀ ≡ a₇
+  ≡tran⁷ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₅ ≡ a₆ → a₆ ≡ a₇ → a₇ ≡ a₈ → a₀ ≡ a₈
   ≡tran  refl refl = refl
   ≡tran² refl refl refl = refl
   ≡tran³ refl refl refl refl = refl
   ≡tran⁴ refl refl refl refl refl = refl
+  ≡tran⁵ refl refl refl refl refl refl = refl
+  ≡tran⁶ refl refl refl refl refl refl refl = refl
+  ≡tran⁷ refl refl refl refl refl refl refl refl = refl
 
   cong : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (f : A → B) → {a a' : A} → a ≡ a' → f a ≡ f a'
   cong f refl = refl
@@ -93,6 +99,11 @@ module PropUtil where
   -- We can make a proof-irrelevant substitution
   substP      : ∀{ℓ}{A : Set ℓ}{ℓ'}(P : A → Prop ℓ'){a a' : A} → a ≡ a' → P a → P a'
   substP P refl h = h
+  substPP      : ∀{ℓ}{A B : Set ℓ}{Q : A → Prop ℓ}{ℓ'}(P : {k : A} → Q k → Prop ℓ'){a a' : A}{x : Q a}
+    → (eq : a ≡ a') → P x → P (substP Q eq x)
+  substPP P refl h = h
+  substP² : ∀{ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Set ℓ'}(P : A → B → Prop ℓ''){a a' : A}{b b' : B} → a ≡ a' → b ≡ b' → P a b → P a' b'
+  substP² P refl refl p = p
 
 
   postulate coe : ∀{ℓ}{A B : Set ℓ} → A ≡ B → A → B
@@ -111,15 +122,25 @@ module PropUtil where
 
   coecong f = ≡tran (cong f coerefl) (≡sym coerefl)
 
+  coecoe-coe : {ℓ : Level}{A B C : Set ℓ}{eq1 : B ≡ A}{eq2 : C ≡ B}{x : C} → coe eq1 (coe eq2 x) ≡ coe (≡tran eq2 eq1) x
+  coecoe-coe {eq1 = refl} {refl} = coerefl
+
   coe-f : {ℓ : Level}{A B C D : Set ℓ} → (A → B) → A ≡ C → B ≡ D → C → D
   coe-f f ac bd x = coe bd (f (coe (≡sym ac) x))
   coewtf : {ℓ : Level}{A B C D E F G H : Set ℓ}{ab : A ≡ B}{cd : C ≡ D}{ef : E ≡ F}{gh : G ≡ H}{f : F → B}{g : H → E}{x : G} →
               {fd : F ≡ D} → f (coe ef (g (coe gh x))) ≡ coe ab ((coe-f f fd (≡sym ab)) (coe cd ((coe-f g (≡sym gh) (≡tran² ef fd (≡sym cd))) x)))
   coewtf {ab = refl} {refl} {refl} {refl} {f} {g} {fd = refl} = ≡tran (cong f (cong (coe _) (≡sym coeaba))) (≡sym coeaba)
 
+  coeshift : {ℓ : Level}{A B : Set ℓ}{x : A} {y : B} {eq : A ≡ B} → coe eq x ≡ y → x ≡ coe (≡sym eq) y
+  coeshift {eq=refl} refl = ≡sym coeaba
+
   subst : ∀{ℓ}{A : Set ℓ}{ℓ'}(P : A → Set ℓ'){a a' : A} → a ≡ a' → P a → P a'
   subst P eq p = coe (cong P eq) p
-
+  subst² : ∀{ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Set ℓ'}(P : A → B → Set ℓ''){a a' : A}{b b' : B} → a ≡ a' → b ≡ b' → P a b → P a' b'
+  subst² P eq eq' p = coe (cong₂ P eq eq') p
+  subst¹P : ∀{ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Prop ℓ'}(P : A → B → Set ℓ''){a a' : A}{b : B} → a ≡ a' → P a b → P a' b
+  subst¹P P {b = b} eq p = coe (cong (λ x → P x b) eq) p
+  
   --{-# REWRITE transprefl   #-}
 
   coereflrefl : {ℓ : Level}{A : Set ℓ}{eq eq' : A ≡ A}{a : A} → coe eq (coe eq' a) ≡ a
@@ -141,6 +162,26 @@ module PropUtil where
     {eq : α ≡ β} {f : {ξ : A} → R ξ → P ξ} {x : R α}
     → coe (cong P eq) (f {α} x) ≡ f (coe (cong R eq) x)
   substfpoly {eq = refl} {f} = ≡tran coerefl (cong f (≡sym coerefl))
+  substppoly : {ℓ ℓ' ℓ'' ℓ''' : Level}{A : Set ℓ}{P : A → Set ℓ'}{R : A → Set ℓ''}{Q : A → Set ℓ'''}{α β : A}
+    {eq : α ≡ β}{f : {ξ : A} → R ξ → Q ξ → P ξ} {x : R α} {y : Q α}
+    → coe (cong P eq) (f {α} x y) ≡ f {β} (coe (cong R eq) x) (coe (cong Q eq) y)
+  substppoly {eq = refl} {f}{x}{y} = ≡tran coerefl (cong₂ f (≡sym coerefl) (≡sym coerefl))
+  substfpoly' : {ℓ ℓ' ℓ'' : Level}{A B : Set ℓ}{P R : A → Set ℓ'}{Q : B → Prop ℓ''}{α β : A}{γ δ : B}
+    {eq : α ≡ β}{eq' : γ ≡ δ} {f : {ξ : A}{ι : B} → R ξ → Q ι → P ξ} {x : R α} {y : Q γ}
+    → coe (cong P eq) (f {α} {γ} x y) ≡ f {β} {δ} (coe (cong R eq) x) (substP Q eq' y)
+  substfpoly' {eq = refl} {refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl
+  substfpoly⁴ : {ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{P R : A → Set ℓ'}{Q : A → Prop ℓ''}{α β : A}
+    {eq : α ≡ β} {f : {ξ : A} → R ξ → Q ξ → P ξ} {x : R α} {y : Q α}
+    → coe (cong P eq) (f {α} x y) ≡ f {β} (coe (cong R eq) x) (substP Q eq y)
+  substfpoly⁴ {eq = refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl
+  substfpoly³ : {ℓ ℓ' ℓ'' ℓ''' : Level}{A B C : Set ℓ}{R : A → Set ℓ'}{Q : B → Prop ℓ''}{P : C → Set ℓ'''}{α β : A}{γ δ : B}{ε φ : C}
+    {eq : α ≡ β}{eq' : γ ≡ δ}{eq'' : ε ≡ φ} {f : {ξ : A}{ι : B}{τ : C} → R ξ → Q ι → P τ} {x : R α} {y : Q γ}
+    → coe (cong P eq'') (f {α} {γ} {ε} x y) ≡ f {β} {δ} {φ} (coe (cong R eq) x) (substP Q eq' y)
+  substfpoly³ {eq = refl} {refl} {refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl
+  substfpoly'' : {ℓ ℓ' ℓ'' : Level}{A C : Set ℓ}{P : A → C → Set ℓ'}{R : A → Set ℓ'}{Q : A → C → Prop ℓ''}{α β : A}{ε φ : C}
+    {eq : α ≡ β}{eq'' : ε ≡ φ} {f : {ξ : A}{κ : C} → R ξ → Q ξ κ → P ξ κ} {x : R α} {y : Q α ε}
+    → coe (cong₂ P eq eq'') (f {α} {ε} x y) ≡ f {β} {φ} (coe (cong R eq) x) (substP (λ X → Q X φ) eq (substP (Q α) eq'' y))
+  substfpoly'' {eq = refl} {refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl
 
   substfgpoly : {ℓ ℓ' : Level}{A B : Set ℓ} {P Q : A → Set ℓ'} {R : B → Set ℓ'} {F : B → A} {α β : A} {ε φ : B}
        {eq₁ : α ≡ β} {eq₂ : F ε ≡ α} {eq₃ : F φ ≡ β} {eq₄ : ε ≡ φ}
@@ -150,9 +191,43 @@ module PropUtil where
 
   {-# BUILTIN EQUALITY _≡_ #-}
 
+  coep² : {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set ℓ₁} {R : A → Set ℓ₂}{T : A → Set ℓ₃}{S : A → Set ℓ₄}{α β : A}
+    {p : {ξ : A} → R ξ → T ξ → S ξ}{x : R α}{y : T α}{eq : α ≡ β}
+    → subst S (≡sym eq) (p {β} (subst R eq x) (subst T eq y)) ≡ p {α} x y
+  coep² {S = S}{p = p}{x}{y}{refl} = ≡tran (substrefl {P = S} {e = refl}) (cong₂ p (substrefl {a = x} {e = refl}) (substrefl {a = y} {e = refl}))
+  coep²'' : {ℓ ℓ' : Level} {A : Set ℓ} {R S : A → Set ℓ'}{T : A → Prop ℓ'}{α β : A}
+    {p : {ξ : A} → R ξ → T ξ → S ξ}{x : R α}{y : T α}{eq : α ≡ β}
+    → subst S (≡sym eq) (p {β} (subst R eq x) (substP T eq y)) ≡ p {α} x y
+  coep²'' {S = S}{p = p}{x}{y}{refl} = ≡tran (substrefl {P = S} {e = refl}) (cong (λ X → p X y) (substrefl {a = x} {e = refl}))
+  coep²' : {ℓ ℓ' : Level} {A : Set ℓ} {R T S : A → Set ℓ'}{α β : A}
+    {p : {ξ : A} → R ξ → T ξ → S ξ}{x : R β}{y : T α}{eq : α ≡ β}
+    → subst S (≡sym eq) (p {β} x (subst T eq y)) ≡ p {α} (subst R (≡sym eq) x) y
+  coep²' {S = S}{p = p}{x}{y}{refl} = ≡tran (substrefl {P = S} {e = refl}) (cong₂ p (≡sym (substrefl {a = x} {e = refl})) (substrefl {a = y} {e = refl}))
 
-
+  coep∘ : {ℓ ℓ' : Level}{A : Set ℓ} {R : A → A → Set ℓ'} {α β γ δ ε φ : A}
-
+        {p : {x y z : A} → R x y → R z x → R z y}{x : R β γ}{y : R α β}
+        {eq1 : α ≡ δ} {eq2 : β ≡ ε} {eq3 : γ ≡ φ} →
+        coe (cong₂ R (≡sym eq1) (≡sym eq3)) (p (coe (cong₂ R eq2 eq3) x) (coe (cong₂ R eq1 eq2) y)) ≡ p x y
+  coep∘ {p = p}{eq1 = refl}{refl}{refl} = ≡tran coerefl (cong₂ p coerefl coerefl)
+  coep∘-helper = λ {ℓ ℓ' ℓ'' : Level}{B : Set ℓ}{A : B → Set ℓ''} {R : (b : B) → A b → A b → Set ℓ'}
+    {b₁ b₂ : B} {α γ : A b₁} {δ φ : A b₂}
+        {eq0 : b₁ ≡ b₂}{eqa : subst A eq0 α ≡ δ}{eqb : subst A eq0 γ ≡ φ}
+     → (≡tran² (cong (R b₂ δ) (≡sym eqb)) (cong (λ X → R b₂ X (subst A eq0 γ)) (≡sym eqa)) (≡tran (≡sym (substrefl {P = λ X → Set ℓ'}{a = R b₂ (subst A eq0 α) (subst A eq0 γ)}{e = refl})) (coep² {p = λ {t} x y → R t x y}{eq = eq0})))
+  coep∘-helper-coe : {ℓ ℓ' ℓ'' : Level}{B : Set ℓ}{A : B → Set ℓ''} {R : (b : B) → A b → A b → Set ℓ'}
+    {b₁ b₂ : B} {α γ : A b₁} {δ φ : A b₂}
+        {eq0 : b₁ ≡ b₂}{eqa : subst A eq0 α ≡ δ}{eqb : subst A eq0 γ ≡ φ} → {a : R b₂ δ φ}{a' : R b₁ α γ} → coe (coep∘-helper {eq0 = eq0} {eqa = eqa} {eqb = eqb}) a ≡ a
+  coep∘-helper-coe {eq0 = refl}{refl}{refl} = coerefl
+  {-coep∘' : {ℓ ℓ' ℓ'' : Level}{B : Set ℓ}{A : B → Set ℓ''} {R : (b : B) → A b → A b → Set ℓ'}
+      {b₁ b₂ : B} {α β γ : A b₁} {δ ε φ : A b₂}
+        {p : {b : B}{x y z : A b} → R b x y → R b z x → R b z y}{x : R b₁ β γ}{y : R b₁ α β}
+        {eq0 : b₁ ≡ b₂}{eq1 : subst A eq0 α ≡ δ} {eq2 : subst A eq0 β ≡ ε} {eq3 : subst A eq0 γ ≡ φ}
+        {eq4 : R b₂ δ φ ≡ R b₁ α γ}{eq5 : R b₂ ε φ ≡ R b₁ β γ}{eq6 : R b₂ δ ε ≡ R b₁ α β}
+        → coe eq4
+        (p {b₂} {ε} {φ} {δ} (coe (≡sym (eq5)) x) (coe (≡sym (
+        eq6
+        )) y)) ≡ p {b₁} {β} {γ} {α} x y
+  --coep∘' {p = p} {x} {y} {eq0 = refl} {refl} {refl} {refl} {eq4} = {!!}
+  -}
 
 
 
@@ -184,6 +259,13 @@ module PropUtil where
       a : A
       b : B a
 
+  record _×ᵈ_ (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
+    constructor _,×ᵈ_
+    field
+      a : A
+      b : B a
+
+
   proj×₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (A × B) → A
   proj×₁ p = _×_.a p
   proj×₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (A × B) → B
@@ -199,4 +281,14 @@ module PropUtil where
   proj×''₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (p : A ×'' B) → B (proj×''₁ p)
   proj×''₂ p = _×''_.b p
 
+  proj×ᵈ₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Set ℓ'} → (A ×ᵈ B) → A
+  proj×ᵈ₁ p = _×ᵈ_.a p
+  proj×ᵈ₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Set ℓ'} → (p : A ×ᵈ B) → (B (proj×ᵈ₁ p))
+  proj×ᵈ₂ p = _×ᵈ_.b p
   
+
+  ×≡ : {A : Set ℓ}{B : Set ℓ'}{a a' : A}{b b' : B} →  a ≡ a' → b ≡ b' → a ,× b ≡ a' ,× b'
+  ×≡ refl refl = refl
+
+  ×ᵈ≡ : {A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'} →  (eq : a ≡ a') → subst B eq b ≡ b' → a ,×ᵈ b ≡ a' ,×ᵈ b'
+  ×ᵈ≡ {B = B} {a = a}{b = b} refl refl = cong₂' _,×ᵈ_ refl refl