diff --git a/FFOL.agda b/FFOL.agda
index 6baeb69..29eb939 100644
--- a/FFOL.agda
+++ b/FFOL.agda
@@ -134,6 +134,47 @@ module FFOL where
     ex5 = {!!}
     -}
 
+  record Mapping (S : FFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} {ℓ⁵}) (D : FFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} {ℓ⁵}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ⁵)) where
+    field
+      
+      -- We first make the base category with its final object
+      mCon : (FFOL.Con S) → (FFOL.Con D)
+      mSub : {Δ : (FFOL.Con S)}{Γ : (FFOL.Con S)} → (FFOL.Sub S Δ Γ) → (FFOL.Sub D (mCon Δ) (mCon Γ))
+      mTm : {Γ : (FFOL.Con S)} → (FFOL.Tm S Γ) → (FFOL.Tm D (mCon Γ))
+      mFor : {Γ : (FFOL.Con S)} → (FFOL.For S Γ) → (FFOL.For D (mCon Γ))
+      m⊢ : {Γ : (FFOL.Con S)} {A : FFOL.For S Γ} → FFOL._⊢_ S Γ A → FFOL._⊢_ D (mCon Γ) (mFor A)
+
+
+  record Morphism (S : FFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} {ℓ⁵}) (D : FFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} {ℓ⁵}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ⁵)) where
+    field m : Mapping S D
+    mCon = Mapping.mCon m
+    mSub = Mapping.mSub m
+    mTm  = Mapping.mTm  m
+    mFor = Mapping.mFor m
+    m⊢   = Mapping.m⊢ m
+    field
+      e∘ : {Γ Δ Ξ : FFOL.Con S}{δ : FFOL.Sub S Δ Ξ}{σ : FFOL.Sub S Γ Δ} → mSub (FFOL._∘_ S δ σ) ≡ FFOL._∘_ D (mSub δ) (mSub σ)
+      eid : {Γ : FFOL.Con S} → mSub (FFOL.id S {Γ}) ≡ FFOL.id D {mCon Γ}
+      e◇ : mCon (FFOL.◇ S) ≡ FFOL.◇ D
+      eε : {Γ : FFOL.Con S} → mSub (FFOL.ε S {Γ}) ≡ subst (FFOL.Sub D (mCon Γ)) (≡sym e◇) (FFOL.ε D {mCon Γ})
+      e[]t : {Γ Δ : FFOL.Con S}{t : FFOL.Tm S Γ}{σ : FFOL.Sub S Δ Γ} → mTm (FFOL._[_]t S t σ) ≡ FFOL._[_]t D (mTm t) (mSub σ)
+      e▹ₜ : {Γ : FFOL.Con S} → mCon (FFOL._▹ₜ S Γ) ≡ FFOL._▹ₜ D (mCon Γ)
+      eπₜ¹ : {Γ Δ : FFOL.Con S}{σ : FFOL.Sub S Δ (FFOL._▹ₜ S Γ)} → mSub (FFOL.πₜ¹ S σ) ≡ FFOL.πₜ¹ D (subst (FFOL.Sub D (mCon Δ)) e▹ₜ (mSub σ))
+      eπₜ² : {Γ Δ : FFOL.Con S}{σ : FFOL.Sub S Δ (FFOL._▹ₜ S Γ)} → mTm (FFOL.πₜ² S σ) ≡ FFOL.πₜ² D (subst (FFOL.Sub D (mCon Δ)) e▹ₜ (mSub σ))
+      e,ₜ : {Γ Δ : FFOL.Con S}{σ : FFOL.Sub S Δ Γ}{t : FFOL.Tm S Δ} → mSub (FFOL._,ₜ_ S σ t) ≡ subst (FFOL.Sub D (mCon Δ)) (≡sym e▹ₜ) (FFOL._,ₜ_ D (mSub σ) (mTm t))
+      e[]f : {Γ Δ : FFOL.Con S}{A : FFOL.For S Γ}{σ : FFOL.Sub S Δ Γ} → mFor (FFOL._[_]f S A σ) ≡ FFOL._[_]f D (mFor A) (mSub σ)
+      -- Proofs are in prop, so no equation needed
+      --[]p : {Γ Δ : FFOL.Con S}{A : FFOL.For S Γ}{pf : FFOL._⊢_ S Γ A}{σ : FFOL.Sub S Δ Γ} → m⊢ (FFOL._[_]p S pf σ) ≡ FFOL._[_]p D (m⊢ pf) (mSub σ)
+      e▹ₚ : {Γ : FFOL.Con S}{A : FFOL.For S Γ} → mCon (FFOL._▹ₚ_ S Γ A) ≡ FFOL._▹ₚ_ D (mCon Γ) (mFor A)
+      eπₚ¹ : {Γ Δ : FFOL.Con S}{A : FFOL.For S Γ}{σ : FFOL.Sub S Δ (FFOL._▹ₚ_ S Γ A)} → mSub (FFOL.πₚ¹ S σ) ≡ FFOL.πₚ¹ D (subst (FFOL.Sub D (mCon Δ)) e▹ₚ (mSub σ))
+      --πₚ² : {Γ Δ : FFOL.Con S}{A : FFOL.For S Γ}{σ : FFOL.Sub S Δ (FFOL._▹ₚ_ S Γ A)} → m⊢ (FFOL.πₚ² S σ) ≡ FFOL.πₚ¹ D (subst (FFOL.Sub D (mCon Δ)) ▹ₚ (mSub σ))
+      e,ₚ : {Γ Δ : FFOL.Con S}{A : FFOL.For S Γ}{σ : FFOL.Sub S Δ Γ}{pf : FFOL._⊢_ S Δ (FFOL._[_]f S A σ)}
+        → mSub (FFOL._,ₚ_ S σ pf) ≡ subst (FFOL.Sub D (mCon Δ)) (≡sym e▹ₚ) (FFOL._,ₚ_ D (mSub σ) (substP (FFOL._⊢_ D (mCon Δ)) e[]f (m⊢ pf)))
+      eR : {Γ : FFOL.Con S}{t u : FFOL.Tm S Γ} → mFor (FFOL.R S t u) ≡ FFOL.R D (mTm t) (mTm u)
+      e⇒ : {Γ : FFOL.Con S}{A B : FFOL.For S Γ} → mFor (FFOL._⇒_ S A B) ≡ FFOL._⇒_ D (mFor A) (mFor B)
+      e∀∀ : {Γ : FFOL.Con S}{A : FFOL.For S (FFOL._▹ₜ S Γ)} → mFor (FFOL.∀∀ S A) ≡ FFOL.∀∀ D (subst (FFOL.For D) e▹ₜ (mFor A))
+      -- No equation needed for lam, app, ∀i, ∀e as their output are in prop
+
   record Tarski : Set₁ where
     field
       TM : Set
diff --git a/FFOLCompleteness.agda b/FFOLCompleteness.agda
index 41defce..00bfb80 100644
--- a/FFOLCompleteness.agda
+++ b/FFOLCompleteness.agda
@@ -153,17 +153,17 @@ module FFOLCompleteness where
   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
+      _-w->_ : World → World → Set ℓ¹ -- arrows
+      -w->id : {w : World} → w -w-> w -- id arrow
+      _∘-w->_ : {w w' w'' : World} → w -w-> w' → w' -w-> w'' → w -w-> w'' -- arrow composition
+      -w->ass : {w w' w'' w''' : World}{a : w -w-> w'}{b : w' -w-> w''}{c : w'' -w-> w'''}
+        → ((a ∘-w-> b) ∘-w-> c) ≡ (a ∘-w-> (b ∘-w-> c))
+      -w->idl : {w w' : World} → {a : w -w-> w'} → (-w->id {w}) ∘-w-> a ≡ a
+      -w->idr : {w w' : World} → {a : w -w-> w'} → a ∘-w-> (-w->id {w'}) ≡ a
       TM : World → Set ℓ¹
-      TM≤ : {w w' : World} → Arr w w' → TM w' → TM w
+      TM≤ : {w w' : World} → w -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)
+      REL≤ : {w w' : World} → {t u : TM w'} → (eq : w -w-> w') → REL w' t u → REL w (TM≤ eq t) (TM≤ eq u)
     infixr 10 _∘_
     Con = World → Set ℓ¹
     Sub : Con → Con → Set ℓ¹
@@ -227,7 +227,7 @@ module FFOLCompleteness where
                                                                                                       
     -- Implication
     _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
-    F ⇒ G = λ w → λ γ → (∀ w' → Arr w w' → (F w γ) → (G w γ))
+    F ⇒ G = λ w → λ γ → (∀ w' → w -w-> w' → (F w γ) → (G w γ))
     
     -- Forall
     ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
@@ -237,7 +237,7 @@ module FFOLCompleteness where
     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 id-a (prf' w γ)
+    app prf prf' = λ w γ → prf w γ w -w->id (prf' w γ)
     -- Again, we don't write the _[_]p equalities as everything is in Prop
     
     -- ∀i and ∀e
@@ -296,43 +296,26 @@ 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)
+  module U where
 
-    {-
-    -- 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) → {!!}
-    -}
 
+    psh : Presheaf
+    psh = record
+            { World = I.Con
+            ; _-w->_ = I.Sub
+            ; -w->id = I.id
+            ; _∘-w->_ = λ σ σ' → σ' I.∘ σ
+            ; -w->ass = ≡sym I.∘-ass
+            ; -w->idl = I.idr
+            ; -w->idr = I.idl
+            ; TM = λ Γ → I.Tm (I.Con.t Γ)
+            ; TM≤ =  λ σ t → t I.[ I.Sub.t σ ]t
+            ; REL = λ Γ t u → I.Pf (I.Con.t Γ) (I.Con.p Γ) (I.R t u)
+            ; REL≤ = λ s pf → (pf I.[ I.Sub.t s ]pₜ) I.[ I.Sub.p s ]p
+            }
 
-
-  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)
+    open Presheaf psh public
 
 
   -- Completeness proof
@@ -344,67 +327,4 @@ module FFOLCompleteness where
     -- We have a model, we construct the Universal Presheaf model of this model
     import FFOLInitial as I
 
-    UniversalPresheaf : Kripke
-    UniversalPresheaf = record
-       { World = (Γₜ : I.Cont) → I.Conp Γₜ
-       ; Arr = λ w₁ w₂ → (Γₜ : I.Cont) → (I.Pf* Γₜ (w₂ Γₜ) (w₁ Γₜ))
-       ; id-a = λ {w} Γₜ → I.Pf*-id
-       ; _∘a_ = λ σ₁ σ₂ Γₜ → I.Pf*-∘ (σ₁ Γₜ) (σ₂ Γₜ)
-       --; ∘a-ass = λ {w} → ≡fun' (λ Γₜ → ≡sym (I.∘ₚ-ass {Γₚ = w Γₜ}))
-       --; idl-a = λ {w} {w'} → ≡fun' (λ Γₜ → I.idrₚ {Γₚ = w Γₜ} {Δₚ = w' Γₜ})
-       --; idr-a = λ {w} {w'} → ≡fun' (λ Γₜ → I.idlₚ {Γₚ = w Γₜ} {Δₚ = w' Γₜ})
-       ; TM = λ w → (Γₜ : I.Cont) → (I.Tm Γₜ)
-       ; TM≤ = λ σ t → t
-       ; REL = λ w t u → (Γₜ : I.Cont) → I.Pf Γₜ (w Γₜ) (I.R (t Γₜ) (u Γₜ))
-       ; REL≤ = λ σ pf → λ Γₜ → I.Pf*Pf {!!} (pf Γₜ)
-       }
-
-    -- I.xx are from initial, xx are from up
-    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.
-    
-    u : {Γₜ : I.Cont}{Γₚ : I.Conp Γₜ}{A : I.For Γₜ} → I.Pf Γₜ Γₚ A → Γₚ ⊫ 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 = {!!}
diff --git a/FFOLInitial.agda b/FFOLInitial.agda
index b14a44b..c1d975b 100644
--- a/FFOLInitial.agda
+++ b/FFOLInitial.agda
@@ -593,8 +593,8 @@ module FFOLInitial where
 
   -- and FINALLY, we compile everything into an implementation of the FFOL record
     
-  imod : FFOL {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero}
-  imod = record
+  ffol : FFOL {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero}
+  ffol = record
     { Con = Con
     ; Sub = Sub
     ; _∘_ = _∘_
@@ -684,3 +684,119 @@ module FFOLInitial where
   Pf*-∘ : {Γₜ : Cont} {Γₚ Δₚ Ξₚ : Conp Γₜ} → Pf* Γₜ Δₚ Ξₚ → Pf* Γₜ Γₚ Δₚ → Pf* Γₜ Γₚ Ξₚ
   Pf*-∘ {Ξₚ = ◇p} α β = tt
   Pf*-∘ {Ξₚ = Ξₚ ▹p⁰ A} α β = ⟨ Pf*-∘ (proj₁ α) β , Pf*Pf β (proj₂ α) ⟩
+
+
+  module InitialMorphism (M : FFOL {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero}) where
+    {-# TERMINATING #-}
+    mCon : Con → (FFOL.Con M)
+    mFor : {Γ : Con} → (For (Con.t Γ)) → (FFOL.For M (mCon Γ))
+    mTm : {Γ : Con} → (Tm (Con.t Γ)) → (FFOL.Tm M (mCon Γ))
+    mSub : {Δ : Con}{Γ : Con} → Sub Δ Γ → (FFOL.Sub M (mCon Δ) (mCon Γ))
+    m⊢ : {Γ : Con} {A : For (Con.t Γ)} → Pf (Con.t Γ) (Con.p Γ) A → FFOL._⊢_ M (mCon Γ) (mFor A)
+    
+    e▹ₜ : {Γ : Con} → mCon (con (Con.t Γ ▹t⁰) (Con.p Γ [ wkₜσₜ idₜ ]c)) ≡ FFOL._▹ₜ M (mCon Γ)
+    e▹ₚ : {Γ : Con}{A : For (Con.t Γ)} → mCon (Γ ▹p A) ≡ FFOL._▹ₚ_ M (mCon Γ) (mFor A)
+    e[]f : {Γ Δ : Con}{A : For (Con.t Γ)}{σ : Sub Δ Γ} → mFor (A [ Sub.t σ ]f) ≡ FFOL._[_]f M (mFor A) (mSub σ)
+
+    mCon (con ◇t ◇p) = FFOL.◇ M
+    mCon (con (Γₜ ▹t⁰) ◇p) = FFOL._▹ₜ M (mCon (con Γₜ ◇p))
+    mCon (con Γₜ (Γₚ ▹p⁰ A)) = FFOL._▹ₚ_ M (mCon (con Γₜ Γₚ)) (mFor {con Γₜ Γₚ} A)
+    mSub {Γ = con ◇t ◇p} (sub εₜ εₚ) = FFOL.ε M
+    mSub {Γ = con (Γₜ ▹t⁰) ◇p} (sub (σₜ ,ₜ t) εₚ) = FFOL._,ₜ_ M (mSub (sub σₜ εₚ)) (mTm t)
+    mSub {Δ = Δ} {Γ = con Γₜ (Γₚ ▹p⁰ A)} (sub σₜ (σₚ ,ₚ pf)) = subst (FFOL.Sub M (mCon Δ)) (≡sym e▹ₚ) (FFOL._,ₚ_ M (mSub (sub σₜ σₚ)) (substP (FFOL._⊢_ M (mCon Δ)) e[]f (m⊢ pf)))
+
+    -- Zero is (πₜ² id)
+    mTm {con (Γₜ ▹t⁰) ◇p} (var tvzero) = FFOL.πₜ² M (FFOL.id M)
+    -- N+1 is wk[tm N]
+    mTm {con (Γₜ ▹t⁰) ◇p} (var (tvnext tv)) = (FFOL._[_]t M (mTm (var tv)) (FFOL.πₜ¹ M (FFOL.id M)))
+    -- If we have a formula in context, we proof-weaken the term (should not change a thing)
+    mTm {con (Γₜ ▹t⁰) (Γₚ ▹p⁰ A)} (var tv) = FFOL._[_]t M (mTm {con (Γₜ ▹t⁰) Γₚ} (var tv)) (FFOL.πₚ¹ M (FFOL.id M))
+    
+    mFor (R t u) = FFOL.R M (mTm t) (mTm u)
+    mFor (A ⇒ B) = FFOL._⇒_ M (mFor A) (mFor B)
+    mFor {Γ} (∀∀ A) = FFOL.∀∀ M (subst (FFOL.For M) (e▹ₜ {Γ = Γ}) (mFor {Γ = Γ ▹t} A))
+
+    e▹ₜ {con Γₜ ◇p} = refl
+    e▹ₜ {con Γₜ (Γₚ ▹p⁰ A)} = ≡tran²
+      (cong₂' (FFOL._▹ₚ_ M) (e▹ₜ {con Γₜ Γₚ}) (cong (subst (FFOL.For M) (e▹ₜ {Γ = con Γₜ Γₚ})) (e[]f {A = A}{σ = πₜ¹* id})))
+      (substP (λ X → (M FFOL.▹ₚ (M FFOL.▹ₜ) (mCon (con Γₜ Γₚ))) X ≡ (M FFOL.▹ₜ) ((M FFOL.▹ₚ mCon (con Γₜ Γₚ)) (mFor A)))
+        (≡tran
+          (coeshift {!!})
+          (cong (λ X → subst (FFOL.For M) _ (FFOL._[_]f M (mFor A) (mSub (sub (wkₜσₜ idₜ) X)))) (≡sym (coecoe-coe {eq1 = ?} {x = idₚ {Δₚ = Γₚ}}))))
+        {!!})
+      (cong (M FFOL.▹ₜ) (≡sym (e▹ₚ {con Γₜ Γₚ})))
+    -- substP (λ X → FFOL._▹ₚ_ M X (mFor {Γ = ?} (A [ wkₜσₜ idₜ ]f)) ≡ (FFOL._▹ₜ M (mCon (con Γₜ (Γₚ ▹p⁰ A))))) (≡sym (e▹ₜ {Γ = con Γₜ Γₚ})) ?
+    
+
+
+    {-
+    
+
+    m⊢ {Γ}{A}(var pvzero) = {!substP (λ X → FFOL._⊢_ M X (mFor A)) (≡sym e▹ₚ) ?!}
+    m⊢ (var (pvnext pv)) = {!!}
+    m⊢ (app pf pf') = FFOL.app M (m⊢ pf) (m⊢ pf')
+    m⊢ (lam pf) = FFOL.lam M {!m⊢ pf!}
+    m⊢ (p∀∀e pf) = {!FFOL.∀e M (m⊢ pf)!}
+    m⊢ {Γ}{∀∀ A}(p∀∀i pf) = FFOL.∀i M (substP (λ X → FFOL._⊢_ M X (subst (FFOL.For M) (≡sym e▹ₜ) (mFor A))) e▹ₜ {!m⊢ pf!})
+
+    e[]f = {!!}
+    
+
+    e∘ : {Γ Δ Ξ : Con}{δ : Sub Δ Ξ}{σ : Sub Γ Δ} → mSub (δ ∘ σ) ≡ FFOL._∘_ M (mSub δ) (mSub σ)
+    e∘ = {!!}
+    eid : {Γ : Con} → mSub (id {Γ}) ≡ FFOL.id M {mCon Γ}
+    eid = {!!}
+    e◇ : mCon ◇ ≡ FFOL.◇ M
+    e◇ = {!!}
+    eε : {Γ : Con} → mSub (sub (εₜ {Con.t Γ}) (εₚ {Con.t Γ} {Con.p Γ})) ≡ subst (FFOL.Sub M (mCon Γ)) (≡sym e◇) (FFOL.ε M {mCon Γ})
+    eε = {!!}
+    e[]t : {Γ Δ : Con}{t : Tm (Con.t Γ)}{σ : Sub Δ Γ} → mTm (t [ Sub.t σ ]t) ≡ FFOL._[_]t M (mTm t) (mSub σ)
+    e[]t = {!!}
+    eπₜ¹ : {Γ Δ : Con}{σ : Sub Δ (Γ ▹t)} → mSub (πₜ¹* σ) ≡ FFOL.πₜ¹ M (subst (FFOL.Sub M (mCon Δ)) e▹ₜ (mSub σ))
+    eπₜ¹ = {!!}
+    eπₜ² : {Γ Δ : Con}{σ : Sub Δ (Γ ▹t)} → mTm (πₜ²* σ) ≡ FFOL.πₜ² M (subst (FFOL.Sub M (mCon Δ)) e▹ₜ (mSub σ))
+    eπₜ² = {!!}
+    e,ₜ : {Γ Δ : Con}{σ : Sub Δ Γ}{t : Tm (Con.t Δ)} → mSub (σ ,ₜ* t) ≡ subst (FFOL.Sub M (mCon Δ)) (≡sym e▹ₜ) (FFOL._,ₜ_ M (mSub σ) (mTm t))
+    e,ₜ = {!!}
+    -- Proofs are in prop, so no equation needed
+    --[]p : {Γ Δ : Con}{A : For Γ}{pf : FFOL._⊢_ S Γ A}{σ : FFOL.Sub S Δ Γ} → m⊢ (FFOL._[_]p S pf σ) ≡ FFOL._[_]p M (m⊢ pf) (mSub σ)
+    e▹ₚ = {!!}
+    eπₚ¹ : {Γ Δ : Con}{A : For (Con.t Γ)}{σ : Sub Δ (Γ ▹p A)} → mSub (πₚ¹* σ) ≡ FFOL.πₚ¹ M (subst (FFOL.Sub M (mCon Δ)) e▹ₚ (mSub σ))
+    eπₚ¹ = {!!}
+    --πₚ² : {Γ Δ : Con}{A : For Γ}{σ : Sub Δ (Γ ▹p A)} → m⊢ (πₚ²* σ) ≡ FFOL.πₚ¹ M (subst (FFOL.Sub M (mCon Δ)) e▹ₚ (mSub σ))
+    e,ₚ : {Γ Δ : Con}{A : For (Con.t Γ)}{σ : Sub Δ Γ}{pf : Pf (Con.t Δ) (Con.p Δ) (A [ Sub.t σ ]f)}
+      → mSub (σ ,ₚ* pf) ≡ subst (FFOL.Sub M (mCon Δ)) (≡sym e▹ₚ) (FFOL._,ₚ_ M (mSub σ) (substP (FFOL._⊢_ M (mCon Δ)) e[]f (m⊢ pf)))
+    e,ₚ = {!!}
+    eR : {Γ : Con}{t u : Tm (Con.t Γ)} → mFor (R t u) ≡ FFOL.R M (mTm t) (mTm u)
+    eR = {!!}
+    e⇒ : {Γ : Con}{A B : For (Con.t Γ)} → mFor (A ⇒ B) ≡ FFOL._⇒_ M (mFor A) (mFor B)
+    e⇒ = {!!}
+    e∀∀ : {Γ : Con}{A : For ((Con.t Γ) ▹t⁰)} → mFor (∀∀ A) ≡ FFOL.∀∀ M (subst (FFOL.For M) e▹ₜ (mFor A))
+    e∀∀ = {!!}
+    -}
+    m : Mapping ffol M
+    m = record { mCon = mCon ; mSub = mSub ; mTm = mTm ; mFor = mFor ; m⊢ = m⊢ }
+    
+  --mor : (M : FFOL) → Morphism ffol M
+  --mor M = record {InitialMorphism M}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+