diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
index a6271cf6042af36ae417ae35303ec58e3d12d3f5..04db6717ac4ce223c428666e063849274e5de46c 100644
--- a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda
@@ -29,6 +29,7 @@ open Category
 open Functor
 open BinCoproduct
 open BinProduct
+open IsMonad
 
 record Model â„“ â„“' : Type (â„“-suc (â„“-max â„“ â„“')) where
   field
@@ -67,6 +68,9 @@ record Model â„“ â„“' : Type (â„“-suc (â„“-max â„“ â„“')) where
 
   T = monad .fst
 
+  ret : ∀ {a} → cat [ a , T ⟅ a ⟆ ]
+  ret = monad .snd .η .NT.NatTrans.N-ob _
+
   _⇀_ : (a b : cat .ob) → cat .ob
   a ⇀ b = a ⇒ T ⟅ b ⟆
 
diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda
index 73c9b3fb371f9bdc3f81027aba476e7cbe2add82..9a0eb56fbd19f36e359f93eff52b01dfe776559d 100644
--- a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda
@@ -33,6 +33,7 @@ open Functor
 open NatTrans
 open BinCoproduct
 open BinProduct
+open TyPrec
 
 private
  variable
@@ -43,77 +44,93 @@ private
    E E' F F' : EvCtx Γ R S
    M M' N N' : Comp Γ S
 
-module _ (M : Model â„“ â„“') where
-  module M = Model M
-  module T = IsMonad (M.monad .snd)
-  ⇒F = ExponentialF M.cat M.binProd M.exponentials
-  ⟦_⟧ty : Ty → M.cat .ob
-  ⟦ nat ⟧ty = M.nat
-  ⟦ dyn ⟧ty = M.dyn
-  ⟦ S ⇀ T ⟧ty = ⟦ S ⟧ty M.⇀ ⟦ T ⟧ty
+module _ (𝓜 : Model ℓ ℓ') where
+  module 𝓜 = Model 𝓜
+  module T = IsMonad (𝓜.monad .snd)
+  ⇒F = ExponentialF 𝓜.cat 𝓜.binProd 𝓜.exponentials
+  ⟦_⟧ty : Ty → 𝓜.cat .ob
+  ⟦ nat ⟧ty = 𝓜.nat
+  ⟦ dyn ⟧ty = 𝓜.dyn
+  ⟦ S ⇀ T ⟧ty = ⟦ S ⟧ty 𝓜.⇀ ⟦ T ⟧ty
 
-  ⟦_⟧e : S ⊑ R → M.cat [ ⟦ S ⟧ty , ⟦ R ⟧ty ]
-  ⟦_⟧p : S ⊑ R → M.cat [ ⟦ R ⟧ty , M.T ⟅ ⟦ S ⟧ty ⟆ ]
-  ⟦_⟧p' : S ⊑ R → M.cat [ M.T ⟅ ⟦ R ⟧ty ⟆ , M.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧e : S ⊑ R → 𝓜.cat [ ⟦ S ⟧ty , ⟦ R ⟧ty ]
+  ⟦_⟧p : S ⊑ R → 𝓜.cat [ ⟦ R ⟧ty , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧p' : S ⊑ R → 𝓜.cat [ 𝓜.T ⟅ ⟦ R ⟧ty ⟆ , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
 
 
-  ⟦ nat ⟧e = M.cat .id
-  ⟦ dyn ⟧e = M.cat .id
+  ⟦ nat ⟧e = 𝓜.cat .id
+  ⟦ dyn ⟧e = 𝓜.cat .id
   -- The most annoying one because it's not from bifunctoriality, more like separate functoriality
   -- λ f . λ x . x'  <- p x;
   --             y'  <- app(f,x');
   --             η (e y')
-  ⟦ c ⇀ d ⟧e     = M.lda ((T.η .N-ob _ ∘⟨ M.cat ⟩ ⟦ d ⟧e) M.∘k
-                         (M.app' (M.π₁ ∘⟨ M.cat ⟩ M.π₁) M.π₂ M.∘sk
-                         (⟦ c ⟧p ∘⟨ M.cat ⟩ M.π₂)))
-  ⟦ inj-nat ⟧e   = M.inj ∘⟨ M.cat ⟩ M.σ1
-  ⟦ inj-arr c ⟧e = M.inj ∘⟨ M.cat ⟩ M.σ2 ∘⟨ M.cat ⟩ ⟦ c ⟧e
-
-  ⟦ nat ⟧p = T.η .N-ob M.nat
-  ⟦ dyn ⟧p = T.η .N-ob M.dyn
+  ⟦ c ⇀ d ⟧e     = 𝓜.lda ((𝓜.ret ∘⟨ 𝓜.cat ⟩ ⟦ d ⟧e) 𝓜.∘k
+                         (𝓜.app' (𝓜.π₁ ∘⟨ 𝓜.cat ⟩ 𝓜.π₁) 𝓜.π₂ 𝓜.∘sk
+                         (⟦ c ⟧p ∘⟨ 𝓜.cat ⟩ 𝓜.π₂)))
+  ⟦ inj-nat ⟧e   = 𝓜.inj ∘⟨ 𝓜.cat ⟩ 𝓜.σ1
+  ⟦ inj-arr c ⟧e = 𝓜.inj ∘⟨ 𝓜.cat ⟩ 𝓜.σ2 ∘⟨ 𝓜.cat ⟩ ⟦ c ⟧e
+
+  ⟦ nat ⟧p = 𝓜.ret
+  ⟦ dyn ⟧p = 𝓜.ret
   -- = η ∘ (⟦ c ⟧e ⇒ ⟦ d ⟧p')
-  ⟦ c ⇀ d ⟧p     = T.η .N-ob _ ∘⟨ M.cat ⟩ ⇒F ⟪ ⟦ c ⟧e , ⟦ d ⟧p' ⟫
-  ⟦ inj-nat ⟧p   = (T.η .N-ob _ M.|| M.℧) M.∘k M.prj
-  ⟦ inj-arr c ⟧p = (M.℧ M.|| ⟦ c ⟧p) M.∘k M.prj
+  ⟦ c ⇀ d ⟧p     = 𝓜.ret ∘⟨ 𝓜.cat ⟩ ⇒F ⟪ ⟦ c ⟧e , ⟦ d ⟧p' ⟫
+  ⟦ inj-nat ⟧p   = (𝓜.ret 𝓜.|| 𝓜.℧) 𝓜.∘k 𝓜.prj
+  ⟦ inj-arr c ⟧p = (𝓜.℧ 𝓜.|| ⟦ c ⟧p) 𝓜.∘k 𝓜.prj
 
   ⟦ c ⟧p' = T.bind .N-ob _ ⟦ c ⟧p
 
-  ⟦_⟧ctx : Ctx → M.cat .ob
-  ⟦ [] ⟧ctx = M.𝟙
-  ⟦ A ∷ Γ ⟧ctx = ⟦ Γ ⟧ctx M.× ⟦ A ⟧ty
+  ⟦_⟧ctx : Ctx → 𝓜.cat .ob
+  ⟦ [] ⟧ctx = 𝓜.𝟙
+  ⟦ A ∷ Γ ⟧ctx = ⟦ Γ ⟧ctx 𝓜.× ⟦ A ⟧ty
 
   -- The term syntax
   -- substitutions, values, ev ctxts, terms
 
-  ⟦_⟧S : Subst Δ Γ → M.cat [ ⟦ Δ ⟧ctx , ⟦ Γ ⟧ctx ]
-  ⟦_⟧V : Val Γ S → M.cat [ ⟦ Γ ⟧ctx , ⟦ S ⟧ty ]
-  ⟦_⟧E : EvCtx Γ R S → M.cat [ ⟦ Γ ⟧ctx M.× ⟦ R ⟧ty , M.T ⟅ ⟦ S ⟧ty ⟆ ]
-  ⟦_⟧C : Comp Γ S → M.cat [ ⟦ Γ ⟧ctx , M.T ⟅ ⟦ S ⟧ty ⟆ ]
-
-  ⟦ ids ⟧S = M.cat .id
-  ⟦ γ ∘s δ ⟧S = ⟦ γ ⟧S ∘⟨ M.cat ⟩ ⟦ δ ⟧S
-  ⟦ ∘IdL {γ = γ} i ⟧S = M.cat .⋆IdR ⟦ γ ⟧S i
-  ⟦ ∘IdR {γ = γ} i ⟧S = M.cat .⋆IdL ⟦ γ ⟧S i
-  ⟦ ∘Assoc {γ = γ}{δ = δ}{θ = θ} i ⟧S = M.cat .⋆Assoc ⟦ θ ⟧S ⟦ δ ⟧S ⟦ γ ⟧S i
-  ⟦ !s ⟧S = M.!t
-  ⟦ []η {γ = γ} i ⟧S = M.𝟙η ⟦ γ ⟧S i
-  ⟦ γ ,s V ⟧S = ⟦ γ ⟧S M.,p ⟦ V ⟧V
-  ⟦ wk ⟧S = M.π₁
-  ⟦ wkβ {δ = γ}{V = V} i ⟧S = M.×β₁ {f = ⟦ γ ⟧S}{g = ⟦ V ⟧V} i
-  ⟦ ,sη {δ = γ} i ⟧S = M.×η {f = ⟦ γ ⟧S} i
-  ⟦ isSetSubst γ γ' p q i j ⟧S = M.cat .isSetHom ⟦ γ ⟧S ⟦ γ' ⟧S (cong ⟦_⟧S p) (cong ⟦_⟧S q) i j
-
-  ⟦ V [ γ ]v ⟧V = ⟦ V ⟧V ∘⟨ M.cat ⟩ ⟦ γ ⟧S
-  ⟦ substId {V = V} i ⟧V = M.cat .⋆IdL ⟦ V ⟧V i
-  ⟦ substAssoc {V = V}{δ = δ}{γ = γ} i ⟧V = M.cat .⋆Assoc ⟦ γ ⟧S ⟦ δ ⟧S ⟦ V ⟧V i
-  ⟦ var ⟧V = M.π₂
-  ⟦ varβ {δ = γ}{V = V} i ⟧V = M.×β₂ {f = ⟦ γ ⟧S}{g = ⟦ V ⟧V} i
-  ⟦ zro ⟧V = {!!}
-  ⟦ suc ⟧V = {!!}
-  ⟦ lda x ⟧V = {!!}
+  ⟦_⟧S : Subst Δ Γ → 𝓜.cat [ ⟦ Δ ⟧ctx , ⟦ Γ ⟧ctx ]
+  ⟦_⟧V : Val Γ S → 𝓜.cat [ ⟦ Γ ⟧ctx , ⟦ S ⟧ty ]
+  ⟦_⟧E : EvCtx Γ R S → 𝓜.cat [ ⟦ Γ ⟧ctx 𝓜.× ⟦ R ⟧ty , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧C : Comp Γ S → 𝓜.cat [ ⟦ Γ ⟧ctx , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
+
+  ⟦ ids ⟧S = 𝓜.cat .id
+  ⟦ γ ∘s δ ⟧S = ⟦ γ ⟧S ∘⟨ 𝓜.cat ⟩ ⟦ δ ⟧S
+  ⟦ ∘IdL {γ = γ} i ⟧S = 𝓜.cat .⋆IdR ⟦ γ ⟧S i
+  ⟦ ∘IdR {γ = γ} i ⟧S = 𝓜.cat .⋆IdL ⟦ γ ⟧S i
+  ⟦ ∘Assoc {γ = γ}{δ = δ}{θ = θ} i ⟧S = 𝓜.cat .⋆Assoc ⟦ θ ⟧S ⟦ δ ⟧S ⟦ γ ⟧S i
+  ⟦ !s ⟧S = 𝓜.!t
+  ⟦ []η {γ = γ} i ⟧S = 𝓜.𝟙η ⟦ γ ⟧S i
+  ⟦ γ ,s V ⟧S = ⟦ γ ⟧S 𝓜.,p ⟦ V ⟧V
+  ⟦ wk ⟧S = 𝓜.π₁
+  ⟦ wkβ {δ = γ}{V = V} i ⟧S = 𝓜.×β₁ {f = ⟦ γ ⟧S}{g = ⟦ V ⟧V} i
+  ⟦ ,sη {δ = γ} i ⟧S = 𝓜.×η {f = ⟦ γ ⟧S} i
+  ⟦ isSetSubst γ γ' p q i j ⟧S = 𝓜.cat .isSetHom ⟦ γ ⟧S ⟦ γ' ⟧S (cong ⟦_⟧S p) (cong ⟦_⟧S q) i j
+
+  ⟦ V [ γ ]v ⟧V = ⟦ V ⟧V ∘⟨ 𝓜.cat ⟩ ⟦ γ ⟧S
+  ⟦ substId {V = V} i ⟧V = 𝓜.cat .⋆IdL ⟦ V ⟧V i
+  ⟦ substAssoc {V = V}{δ = δ}{γ = γ} i ⟧V = 𝓜.cat .⋆Assoc ⟦ γ ⟧S ⟦ δ ⟧S ⟦ V ⟧V i
+  ⟦ var ⟧V = 𝓜.π₂
+  ⟦ varβ {δ = γ}{V = V} i ⟧V = 𝓜.×β₂ {f = ⟦ γ ⟧S}{g = ⟦ V ⟧V} i
+  ⟦ zro ⟧V = 𝓜.nat-fp .fst ∘⟨ 𝓜.cat ⟩ 𝓜.σ1 ∘⟨ 𝓜.cat ⟩ 𝓜.!t
+  ⟦ suc ⟧V = 𝓜.nat-fp .fst ∘⟨ 𝓜.cat ⟩ 𝓜.σ2 ∘⟨ 𝓜.cat ⟩ 𝓜.π₂
+  ⟦ lda M ⟧V = 𝓜.lda ⟦ M ⟧C
   ⟦ fun-η i ⟧V = {!!}
-  ⟦ up S⊑T ⟧V = {!!}
-  ⟦ isSetVal V V' p q i j ⟧V = M.cat .isSetHom ⟦ V ⟧V ⟦ V' ⟧V (cong ⟦_⟧V p) (cong ⟦_⟧V q) i j
+  ⟦ up S⊑T ⟧V = ⟦ S⊑T .ty-prec  ⟧e ∘⟨ 𝓜.cat ⟩ 𝓜.π₂
+  ⟦ isSetVal V V' p q i j ⟧V = 𝓜.cat .isSetHom ⟦ V ⟧V ⟦ V' ⟧V (cong ⟦_⟧V p) (cong ⟦_⟧V q) i j
+
+  -- | TODO: potential for generalization
+  -- | This is a general construction of a category from a strong monad, the "simple Kleisli slice"
+  ⟦ ∙E ⟧E = 𝓜.ret ∘⟨ 𝓜.cat ⟩ 𝓜.π₂
+  ⟦ E ∘E F ⟧E = {!!}
+  ⟦ ∘IdL i ⟧E = {!!}
+  ⟦ ∘IdR i ⟧E = {!!}
+  ⟦ ∘Assoc i ⟧E = {!!}
+  ⟦ E [ γ ]e ⟧E = {!!}
+  ⟦ substId i ⟧E = {!!}
+  ⟦ substAssoc i ⟧E = {!!}
+  ⟦ ∙substDist i ⟧E = {!!}
+  ⟦ ∘substDist i ⟧E = {!!}
+  ⟦ bind x ⟧E = {!!}
+  ⟦ ret-η i ⟧E = {!!}
+  ⟦ dn S⊑T ⟧E = ⟦ S⊑T .ty-prec ⟧p ∘⟨ 𝓜.cat ⟩ 𝓜.π₂
+  ⟦ isSetEvCtx E F p q i j ⟧E = 𝓜.cat .isSetHom ⟦ E ⟧E ⟦ F ⟧E (cong ⟦_⟧E p) (cong ⟦_⟧E q) i j
 
-  ⟦_⟧E = {!!}
   ⟦_⟧C = {!!}
diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength.agda
index 5f8f39dd900d2aca19504253308056dd11029a08..f63a72b2d73cca8f192fd0052283e787d99e8cee 100644
--- a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength.agda
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical #-}
 module Semantics.Abstract.TermModel.Strength where
 
-{- Strength of a functor between *cartesian* categories -}
+{- Strength of a monad an a *cartesian* category -}
+{- TODO: generalize to monoidal -}
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
@@ -60,6 +61,14 @@ module _ (C : Category â„“ â„“') (term : Terminal C) (bp : BinProducts C) (T : M
   module StrengthNotation (str : Strength) where
     open Notation _ bp renaming (_×_ to _×c_)
     σ = str .fst
+
+
+    strength-η : StrengthUnit σ
+    strength-η = str .snd .snd .snd .fst
+
+    strength-μ : StrengthMult σ
+    strength-μ = str .snd .snd .snd .snd
+
     -- TODO: move this upstream in Monad.Notation
     _∘k_ : ∀ {a b c} → C [ b , T .fst ⟅ c ⟆ ] → C [ a , T .fst ⟅ b ⟆ ] → C [ a , T .fst ⟅ c ⟆ ]
     f ∘k g = (IsMonad.bind (T .snd)) .N-ob _ f ∘⟨ C ⟩ g
@@ -68,3 +77,4 @@ module _ (C : Category â„“ â„“') (term : Terminal C) (bp : BinProducts C) (T : M
     strong-bind f m = f ∘k σ .N-ob _ ∘⟨ C ⟩ (C .id ,p m)
 
     _∘sk_ = strong-bind
+    -- TODO: lemma for how strength interacts with bind
diff --git a/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength/KleisliSlice.agda b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength/KleisliSlice.agda
new file mode 100644
index 0000000000000000000000000000000000000000..412f3bff23252cf3ad7f95bfacda5fa974bb26df
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Abstract/TermModel/Strength/KleisliSlice.agda
@@ -0,0 +1,72 @@
+{-# OPTIONS --cubical --lossy-unification #-}
+module Semantics.Abstract.TermModel.Strength.KleisliSlice where
+
+{- Given a strong monad on a cartesian category and a fixed object Γ,
+we get a paramaterized version of the Kleisli category -}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Limits.Terminal
+open import Cubical.Categories.Limits.BinProduct
+open import Cubical.Categories.Monad.Base
+
+open import Cubical.Categories.Limits.BinProduct.More
+open import Semantics.Abstract.TermModel.Strength
+
+private
+  variable
+    â„“ â„“' : Level
+
+open Category
+open Functor
+open NatTrans
+open BinProduct
+open IsMonad
+
+--
+module _ (C : Category â„“ â„“') (term : Terminal C) (bp : BinProducts C) (T : Monad C) (s : Strength C term bp T) where
+  module C = Category C
+  open Notation C bp
+  open StrengthNotation C term bp T s
+  module _ (Γ : C .ob) where
+    KleisliSlice : Category â„“ â„“'
+    KleisliSlice .ob = C .ob
+    KleisliSlice .Hom[_,_] a b = C [ Γ × a , T .fst ⟅ b ⟆ ]
+    KleisliSlice .id = T .snd .η .N-ob _ C.∘ π₂
+    -- Γ , x → T y    |-> 
+    -- Γ , y → T z
+    --------------
+    -- Γ , x → T z
+    KleisliSlice ._⋆_ f g = bind (T .snd) .N-ob _ g C.∘ σ .N-ob _ C.∘ (π₁ ,p f)
+    -- bind (T .snd) .N-ob _ g C.∘ σ .N-ob _ C.∘ (π₁ ,p T .snd .η .N-ob _ C.∘ π₂)
+    --
+    -- μ ∘ T g ∘ σ ∘ (π1 , η ∘ π₂)
+    -- μ ∘ T g ∘ σ ∘ (id × η)
+    -- μ ∘ T g ∘ η
+    -- μ ∘ η ∘ g
+    -- ≡ g
+    KleisliSlice .⋆IdL g =
+      cong₂ C._∘_ refl (cong₂ C._∘_ refl (cong₂ _,p_ (sym (C.⋆IdR _)) refl) ∙ (λ i → strength-η (~ i) _ _))
+      ∙ sym (C.⋆Assoc _ _ _)
+      ∙ cong₂ C._∘_ refl (sym (T .snd .η .N-hom _))
+      ∙ C.⋆Assoc _ _ _
+      ∙ cong (C._∘ g) (λ i → T .snd .idl-μ i .N-ob _)
+      ∙ C.⋆IdR g
+    -- μ ∘ T (T η ∘ π₂) ∘ σ ∘ (π₁ , f)
+    -- μ ∘ T^2 η ∘ T π₂ ∘ σ ∘ (π₁ , f)
+    -- T η ∘ μ ∘ T π₂ ∘ σ ∘ (π₁ , f)
+    -- T π₂ ∘ σ ∘ (π₁ , f)
+    -- ≡ f
+    KleisliSlice .⋆IdR f = {!!}
+    KleisliSlice .⋆Assoc = {!!}
+    KleisliSlice .isSetHom = C.isSetHom
+
+  module _ {Δ : C .ob} {Γ : C .ob} where
+    _^* : (γ : C [ Δ , Γ ]) → Functor (KleisliSlice Γ) (KleisliSlice Δ)
+    (γ ^*) .F-ob a = a
+    (γ ^*) .F-hom f = f C.∘ (γ ×p C.id)
+    (γ ^*) .F-id = sym (C.⋆Assoc _ _ _) ∙ cong₂ C._⋆_ (×β₂ ∙ C .⋆IdR π₂) refl
+    (γ ^*) .F-seq f g = {!!}