diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 98c0045..4ae4ad9 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -135,9 +135,9 @@ jobs:
       - name: Download categorical-logic from github
         run : |
           cd ~
-          git clone https://github.com/maxsnew/cubical-categorical-logic --branch master
+          git clone https://github.com/maxsnew/cubical-categorical-logic --branch main
           cd cubical-categorical-logic
-          git checkout 295cc5defa414b861959f89f52325e098b9db6ec
+          git checkout 4e7b1c3a2ba7ed528b3cd9a4c3a5e7be3ff3449d
           cd ..
           echo "CATLOG_DIR=$PWD/cubical-categorical-logic" >> "$GITHUB_ENV"
 
@@ -146,7 +146,7 @@ jobs:
           mkdir ~/.agda
           touch ~/.agda/libraries
           echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries
-          echo "$CATLOG_DIR/cubical.agda-lib" >> ~/.agda/libraries
+          echo "$CATLOG_DIR/cubical-categorical-logic.agda-lib" >> ~/.agda/libraries
           echo "$GITHUB_WORKSPACE/code/cubical/grammar.agda-lib" >> ~/.agda/libraries
 
       ########################################################################
diff --git a/code/cubical/Examples/Indexed/Dyck.agda b/code/cubical/Examples/Indexed/Dyck.agda
index 2baf3a0..9c484ba 100644
--- a/code/cubical/Examples/Indexed/Dyck.agda
+++ b/code/cubical/Examples/Indexed/Dyck.agda
@@ -10,11 +10,13 @@ open import Cubical.Foundations.Structure
 
 open import Cubical.Data.Bool as Bool hiding (_⊕_ ;_or_)
 import Cubical.Data.Equality as Eq
+import Cubical.Data.Equality.Conversion as Eq
 open import Cubical.Data.Nat as Nat
 open import Cubical.Data.List hiding (init; rec; map)
 open import Cubical.Data.Sigma
 open import Cubical.Data.Sum as Sum hiding (rec; map)
 open import Cubical.Data.FinSet
+open import Cubical.Data.Unit
 
 private
   variable
@@ -45,19 +47,42 @@ open import Grammar.String.Properties Alphabet
 open import Grammar.Equivalence Alphabet
 open import Grammar.Equalizer Alphabet
 open import Grammar.Inductive.Indexed Alphabet
+open import Grammar.Inductive.HLevels Alphabet
+open import Grammar.HLevels Alphabet
+open import Grammar.Coherence Alphabet
 open import Term Alphabet
 
 open StrongEquivalence
 
 data DyckTag : Type ℓ-zero where
   nil' balanced' : DyckTag
+
+isSetDyckTag : isSet DyckTag
+isSetDyckTag = isSetRetract enc dec retr isSetBool where
+  enc : DyckTag → Bool
+  enc nil' = false
+  enc balanced' = true
+  dec : Bool → DyckTag
+  dec false = nil'
+  dec true = balanced'
+  retr : (x : DyckTag) → dec (enc x) ≡ x
+  retr nil' = refl
+  retr balanced' = refl
+
 DyckTy : Unit → Functor Unit
 DyckTy _ = ⊕e DyckTag (λ
   { nil' → k ε
   ; balanced' → ⊗e (k (literal [)) (⊗e (Var _) (⊗e (k (literal ])) (Var _))) })
+
+
 IndDyck : Grammar ℓ-zero
 IndDyck = μ DyckTy _
 
+isSetGrammarDyck : isSetGrammar IndDyck
+isSetGrammarDyck = isSetGrammarμ DyckTy
+  (λ _ → isSetDyckTag , (λ { nil' → isSetGrammarε ; balanced' → isSetGrammarLiteral _ , (tt* , (isSetGrammarLiteral _ , tt*)) }))
+  tt
+
 NIL : ε ⊢ IndDyck
 NIL = roll ∘g ⊕ᴰ-in nil' ∘g liftG
 
@@ -127,6 +152,52 @@ data TraceTag (b : Bool) (n : ℕ) : Type where
   leftovers' : (b Eq.≡ false) → ∀ n-1 → (suc n-1 Eq.≡ n) → TraceTag b n
   unexpected' : b Eq.≡ false → n Eq.≡ zero → TraceTag b n
 
+isSetTraceTag : ∀ b n → isSet (TraceTag b n)
+isSetTraceTag b n = isSetRetract {B = TT} enc dec retr isSetTT where
+  isPropBoolEq : ∀ {b b' : Bool} → isProp (b Eq.≡ b')
+  isPropBoolEq {b}{b'} =
+    subst isProp Eq.PathPathEq (isSetBool _ _)
+
+  isPropℕEq : ∀ {b b' : ℕ} → isProp (b Eq.≡ b')
+  isPropℕEq {b}{b'} =
+    subst isProp Eq.PathPathEq (isSetℕ _ _)
+
+  TT : Type ℓ-zero
+  TT =
+    ((b Eq.≡ true) × (n Eq.≡ zero))
+    ⊎ (Eq.fiber suc n
+    ⊎ (Unit
+    ⊎ (((b Eq.≡ false) × Eq.fiber suc n)
+    ⊎ ((b Eq.≡ false) × (n Eq.≡ zero)))))
+  isSetTT : isSet TT
+  isSetTT =
+    isSet⊎ (isProp→isSet (isProp× isPropBoolEq isPropℕEq))
+    (isSet⊎ (isSetΣ isSetℕ (λ _ → isProp→isSet isPropℕEq))
+    (isSet⊎ isSetUnit
+    (isSet⊎ (isSet× (isProp→isSet isPropBoolEq)
+      (isSetΣ isSetℕ (λ _ → isProp→isSet isPropℕEq)))
+    (isProp→isSet (isProp× isPropBoolEq isPropℕEq)))))
+  enc : TraceTag b n → TT
+  enc (eof' x x₁) = inl (x , x₁)
+  enc (close' n-1 x) = inr (inl (n-1 , x))
+  enc open' = inr (inr (inl tt))
+  enc (leftovers' x n-1 x₁) = inr (inr (inr (inl (x , n-1 , x₁))))
+  enc (unexpected' x x₁) = inr (inr (inr (inr (x , x₁))))
+
+  dec : TT → TraceTag b n
+  dec (inl x) = eof' (x .fst) (x .snd)
+  dec (inr (inl x)) = close' (x .fst) (x .snd)
+  dec (inr (inr (inl x))) = open'
+  dec (inr (inr (inr (inl x)))) = leftovers' (x .fst) _ (x .snd .snd)
+  dec (inr (inr (inr (inr x)))) = unexpected' (x .fst) (x .snd)
+
+  retr : ∀ t → dec (enc t) ≡ t
+  retr (eof' x x₁) = refl
+  retr (close' n-1 x) = refl
+  retr open' = refl
+  retr (leftovers' x n-1 x₁) = refl
+  retr (unexpected' x x₁) = refl
+
 LP = [
 RP = ]
 
@@ -142,6 +213,16 @@ TraceTys b n = ⊕e (TraceTag b n) (λ
 Trace : Bool → ℕ → Grammar _
 Trace b = μ (TraceTys b)
 
+isSetGrammarTrace : ∀ b n → isSetGrammar (Trace b n)
+isSetGrammarTrace b = isSetGrammarμ (TraceTys b) λ n →
+  isSetTraceTag b n
+  , λ { (eof' x x₁) → isSetGrammarε
+      ; (close' n-1 x) → (isSetGrammarLiteral _) , tt*
+      ; open' → (isSetGrammarLiteral _) , tt*
+      ; (leftovers' x n-1 x₁) → isSetGrammarε
+      ; (unexpected' x x₁) → (isSetGrammarLiteral _) , isSetGrammar⊤
+      }
+
 EOF : ε ⊢ Trace true 0
 EOF = roll ∘g ⊕ᴰ-in (eof' Eq.refl Eq.refl) ∘g liftG
 
@@ -267,6 +348,12 @@ GenDyck : ℕ → Grammar _
 GenDyck 0         = IndDyck
 GenDyck (suc n-1) = IndDyck ⊗ literal RP ⊗ GenDyck n-1
 
+isSetGrammarGenDyck : ∀ n → isSetGrammar (GenDyck n)
+isSetGrammarGenDyck zero = isSetGrammarDyck
+isSetGrammarGenDyck (suc n) =
+  isSetGrammar⊗ isSetGrammarDyck
+    (isSetGrammar⊗ (isSetGrammarLiteral _) (isSetGrammarGenDyck n))
+
 -- We extend the balanced constructor and append to our unbalanced
 -- trees
 opaque
@@ -280,13 +367,6 @@ upgradeBuilder (suc n) = ⟜-intro (⟜-app ,⊗ id ∘g ⊗-assoc)
 
 opaque
   unfolding ⊗-intro genBALANCED
-  -- uB-lem' :
-  --   ∀ n (f : Trace true n ⊢ GenDyck n)
-  --       (f' : {!!} ⊢ {!!})
-  --      → (⟜-app ∘g id ,⊗ f) ∘g
-  --       (upgradeBuilder n ∘g ⟜-intro {!!}) ,⊗ id
-  --       ≡ (f ∘g {!!})
-  -- uB-lem' = {!!}
   upgradeNilBuilder :
     ∀ n (f : Trace true n ⊢ GenDyck n)
        → (⟜-app ∘g id ,⊗ f) ∘g
@@ -300,8 +380,7 @@ opaque
     ∙ cong ((⟜-app ,⊗ id) ∘g_) (cong (_∘g (id ,⊗ f)) (⊗-assoc⊗-intro {f' = id}{f'' = id}))
     ∙ ( (λ i → (⟜-β ⊗-unit-l i) ,⊗ id ∘g ⊗-assoc ∘g id ,⊗ f))
     ∙ cong (_∘g (id ,⊗ f)) (cong ((⊗-unit-l ,⊗ id) ∘g_) (sym (⊗-assoc⊗-intro {f' = id}{f'' = id})))
-    -- ∙ cong (_∘g id ,⊗ f) ⊗-unit-l⊗-assoc
-    ∙ {!!}
+    ∙ cong (_∘g id ,⊗ f) (⊗-unit-l⊗-assoc isSetGrammarDyck (isSetGrammar⊗ (isSetGrammarLiteral _) (isSetGrammarGenDyck n)))
     ∙ sym (⊗-unit-l⊗-intro _)
 
   upgradeBalancedBuilder :
@@ -336,7 +415,8 @@ opaque
       ∘g id ,⊗ ((id ,⊗ NIL) ,⊗ id)
       ∘g id ,⊗ (⊗-assoc ∘g id ,⊗ ⊗-unit-l⁻)  --
       ∘g id ,⊗ id ,⊗ id ,⊗ ⟜-app
-      ∘g lowerG ,⊗ lowerG ,⊗ lowerG ,⊗ (id ∘g lowerG) ,⊗ id ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i)
+      ∘g lowerG ,⊗ lowerG ,⊗ lowerG ,⊗ (id ∘g lowerG) ,⊗ id ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i
+      )
     ∙ (λ i → BALANCED
       ∘g id ,⊗ (⟜-app ,⊗ id)
       ∘g id ,⊗ ⊗-assoc⊗-intro {f = id}{f' = NIL}{f'' = id} (~ i)
@@ -368,7 +448,14 @@ opaque
     ∙ (λ i →
        BALANCED ,⊗ id
        ∘g (lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻) ,⊗ lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ id)) ,⊗ id
-       ∘g ⊗-assoc⁻4⊗-assoc i
+       ∘g ⊗-assoc⁻4⊗-assoc
+          (isSetGrammarLift (isSetGrammarLiteral _))
+          (isSetGrammarLift (isSetGrammar⟜ isSetGrammarDyck))
+          (isSetGrammarLift (isSetGrammarLiteral _))
+          (isSetGrammarLift (isSetGrammar⟜ isSetGrammarDyck))
+          isSetGrammarDyck
+          (isSetGrammar⊗ (isSetGrammarLiteral _) (isSetGrammarGenDyck n))
+          i
        ∘g id ,⊗ f)
     ∙ (λ i → BALANCED ,⊗ id
         ∘g ⊗-assoc4⊗-intro {f = lowerG}{f' = ⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻}{f'' = lowerG}{f''' = (⟜-app ∘g lowerG ,⊗ id)}{f'''' = id} (~ i)
@@ -379,7 +466,8 @@ opaque
         ∘g ⊗-assoc4
         ∘g lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻) ,⊗ lowerG ,⊗ ((⟜-app ∘g lowerG ,⊗ id) ,⊗ id)
         ∘g id ,⊗ id ,⊗ id ,⊗ ⊗-assoc
-        ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i)
+        ∘g ⊗-assoc⁻4⊗-intro {f = id}{f' = id}{f'' = id}{f''' = id}{f'''' = f} i
+        )
     ∙ (λ i → BALANCED ,⊗ id
         ∘g ⊗-assoc4
         ∘g lowerG ,⊗ ((⟜-app ∘g (id ,⊗ NIL) ∘g ⊗-unit-r⁻⊗-intro {f = lowerG} (~ i)) ,⊗ lowerG ,⊗ ((⟜-app ∘g lowerG ,⊗ id) ,⊗ id ∘g ⊗-assoc ∘g id ,⊗ f))
@@ -469,14 +557,6 @@ buildTraceAlg _ = ⊕ᴰ-elim (λ
 buildTrace : IndDyck ⊢ TraceBuilder _
 buildTrace = rec DyckTy buildTraceAlg _
 
--- buildTraceβBalanced :
---   buildTrace ∘g roll ∘g ⊕ᴰ-in balanced'
---   ≡ &ᴰ-intro λ n → ⟜-intro
---     (({!\!}
---      ∘g ⊗-assoc⁻4
---     )
---     ∘g (lowerG ,⊗ (buildTrace ∘g lowerG) ,⊗ lowerG ,⊗ (buildTrace ∘g lowerG)) ,⊗ id)
-
 -- we then extend the builder to generalized trees, which *adds*
 -- closed parens to the trace.
 genBuildTrace : ∀ m → GenDyck m ⊢ &[ n ∈ _ ] (Trace true (m + n) ⟜ Trace true n)
@@ -578,7 +658,8 @@ pfAlg _ =
                 ∘g id ,⊗ (⟜-app ∘g &ᴰ-π (suc n) ,⊗ id)
                 ∘g id ,⊗ id ,⊗ CLOSE
                 ∘g id ,⊗ id ,⊗ id ,⊗ (⟜-app ∘g &ᴰ-π n ,⊗ id)
-                ∘g ⊗-assoc⁻4⊗-intro {f = lowerG}{f' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'' = lowerG}{f''' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'''' = id} i)
+                ∘g ⊗-assoc⁻4⊗-intro {f = lowerG}{f' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'' = lowerG}{f''' = buildTrace ∘g eq-π lhs rhs ∘g lowerG}{f'''' = id} i
+                )
             ∙ (λ i → genBALANCED n
                 ∘g id ,⊗ (⟜-β (genMkTree (suc n) ∘g ⟜-app) (~ i) ∘g (&ᴰ-π (suc n) ∘g (buildTrace ∘g eq-π lhs rhs)) ,⊗ id)
                 ∘g id ,⊗ id ,⊗ CLOSE
diff --git a/code/cubical/Grammar/Coherence.agda b/code/cubical/Grammar/Coherence.agda
new file mode 100644
index 0000000..274a509
--- /dev/null
+++ b/code/cubical/Grammar/Coherence.agda
@@ -0,0 +1,73 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.Coherence (Alphabet : hSet ℓ-zero) where
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.List
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Monoidal
+open import Cubical.Categories.Monoidal.Combinators.Base as Combinators
+open import Cubical.Categories.Monoidal.Combinators.Equations as Combinators
+
+open import Grammar.Base Alphabet
+open import Grammar.Lift Alphabet
+open import Grammar.HLevels Alphabet
+open import Grammar.Epsilon Alphabet
+open import Grammar.LinearProduct Alphabet
+open import Term.Base Alphabet
+open import Term.Bilinear Alphabet
+open import Term.Category Alphabet
+
+private
+  variable
+    ℓg ℓh ℓk ℓl ℓ ℓ' : Level
+    g g' g'' g''' g'''' g''''' : Grammar ℓg
+    h h' h'' h''' h'''' h''''' : Grammar ℓh
+    f f' f'' f''' f'''' f''''' : g ⊢ h
+    k : Grammar ℓk
+    l : Grammar ℓl
+
+private
+  G = GRAMMAR ℓ-zero
+  module G = MonoidalCategory G
+
+opaque
+  ⊗-assoc⁻4⊗-assoc :
+    ∀ {g g' g'' g''' g'''' g''''' : Grammar ℓ-zero}
+    → isSetGrammar g
+    → isSetGrammar g'
+    → isSetGrammar g''
+    → isSetGrammar g'''
+    → isSetGrammar g''''
+    → isSetGrammar g'''''
+    → ⊗-assoc⁻4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''}{g'''' = g''''}
+      ,⊗ id {g = g'''''}
+      ∘g ⊗-assoc
+      ≡ ⊗-assoc4 ∘g id ,⊗ id ,⊗ id ,⊗ ⊗-assoc ∘g ⊗-assoc⁻4
+  ⊗-assoc⁻4⊗-assoc isSetG isSetG' isSetG'' isSetG''' isSetG'''' isSetG''''' =
+    α4⁻¹α G (_ , isSetG) (_ , isSetG') (_ , isSetG'')
+            (_ , isSetG''') (_ , isSetG'''') (_ , isSetG''''')
+
+⊗-unit*-l⊗-assoc :
+  {g g' : Grammar ℓ-zero}
+  → isSetGrammar g
+  → isSetGrammar g'
+  → ⊗-unit*-l {ℓ = ℓ-zero} {g = g} ,⊗ id {g = g'} ∘g ⊗-assoc ≡ ⊗-unit*-l
+⊗-unit*-l⊗-assoc isSetG isSetG' =
+  Combinators.ηα G (_ , isSetG) (_ , isSetG')
+
+opaque
+  unfolding ⊗-intro
+  ⊗-unit-l⊗-assoc :
+    {g g' : Grammar ℓ-zero}
+    → isSetGrammar g
+    → isSetGrammar g'
+    → ⊗-unit-l {g = g} ,⊗ id {g = g'} ∘g ⊗-assoc ≡ ⊗-unit-l
+  ⊗-unit-l⊗-assoc isSetG isSetG' =
+    ⊗-unit-l ,⊗ id ∘g ⊗-assoc
+      ≡⟨ cong ((⊗-unit*-l {ℓ-zero} ,⊗ id) ∘g_) ⊗-assoc⊗-intro ⟩
+    (⊗-unit*-l {ℓ-zero} ,⊗ id) ∘g ⊗-assoc ∘g ⊗-intro (liftG {ℓ-zero}) id
+      ≡⟨ cong (_∘g ⊗-intro liftG id) (⊗-unit*-l⊗-assoc isSetG isSetG') ⟩
+    ⊗-unit-l
+    ∎
diff --git a/code/cubical/Grammar/Dependent/Properties.agda b/code/cubical/Grammar/Dependent/Properties.agda
index e1057fc..2375118 100644
--- a/code/cubical/Grammar/Dependent/Properties.agda
+++ b/code/cubical/Grammar/Dependent/Properties.agda
@@ -9,6 +9,7 @@ open import Cubical.Data.FinSet
 open import Cubical.Foundations.Structure
 
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.LinearProduct Alphabet
 open import Grammar.LinearFunction Alphabet
 open import Grammar.Equivalence.Base Alphabet
@@ -79,3 +80,12 @@ module _
   unambiguous⊕ᴰ unambig⊕ a =
     unambiguous'→unambiguous
       (unambiguous'⊕ᴰ (unambiguous→unambiguous' unambig⊕) a)
+
+module _
+  {X : Type ℓS} {A : X → Grammar ℓh}
+  where
+  isSetGrammar&ᴰ : (∀ x → isSetGrammar (A x)) → isSetGrammar (&ᴰ A)
+  isSetGrammar&ᴰ isSetGrammarA w = isSetΠ λ x → isSetGrammarA x w
+
+  isSetGrammar⊕ᴰ : isSet X → (∀ x → isSetGrammar (A x)) → isSetGrammar (⊕ᴰ A)
+  isSetGrammar⊕ᴰ isSetX isSetGrammarA w = isSetΣ isSetX (λ x → isSetGrammarA x w)
diff --git a/code/cubical/Grammar/Epsilon.agda b/code/cubical/Grammar/Epsilon.agda
index 4e91865..8c6bfe4 100644
--- a/code/cubical/Grammar/Epsilon.agda
+++ b/code/cubical/Grammar/Epsilon.agda
@@ -7,6 +7,7 @@ open import Cubical.Data.List
 
 open import Helper
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.Lift Alphabet
 open import Term.Base Alphabet
 open import Term.Nullary Alphabet
@@ -53,5 +54,18 @@ opaque
       (sym (++-unit-r _) ∙ cong (w1 ++_) (sym w2≡[]))
       (f w1 gp)
 
+  isLangε : isLang ε
+  isLangε _ _ _ = isSetString _ _ _ _
+
+  isSetGrammarε : isSetGrammar ε
+  isSetGrammarε = isLang→isSetGrammar isLangε
+
 ε* : ∀ {ℓ : Level} → Grammar ℓ
 ε* {ℓ = ℓ} = LiftG ℓ ε
+
+isLangε* : ∀ {ℓ} → isLang (ε* {ℓ})
+isLangε* = isLangLift isLangε
+
+isSetGrammarε* : ∀ {ℓ} → isSetGrammar (ε* {ℓ})
+isSetGrammarε* = isLang→isSetGrammar isLangε*
+
diff --git a/code/cubical/Grammar/HLevels.agda b/code/cubical/Grammar/HLevels.agda
new file mode 100644
index 0000000..9750e07
--- /dev/null
+++ b/code/cubical/Grammar/HLevels.agda
@@ -0,0 +1,32 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.HLevels (Alphabet : hSet ℓ-zero) where
+
+open import Grammar.Base Alphabet
+
+private
+  variable ℓ ℓG ℓG' ℓH ℓK ℓL : Level
+
+module _ where
+  isLang : Grammar ℓG → Type ℓG
+  isLang A = ∀ w → isProp (A w)
+
+  isSetGrammar : Grammar ℓG → Type ℓG
+  isSetGrammar A = ∀ w → isSet (A w)
+
+  isLang→isSetGrammar : ∀ {A : Grammar ℓG} → isLang A → isSetGrammar A
+  isLang→isSetGrammar isLangA w = isProp→isSet (isLangA w)
+
+  Lang : ∀ (ℓ : Level) →  Type (ℓ-suc ℓ)
+  Lang ℓ = Σ[ A ∈ Grammar ℓ ] isLang A
+
+  SetGrammar : ∀ (ℓ : Level) →  Type (ℓ-suc ℓ)
+  SetGrammar ℓ = Σ[ A ∈ Grammar ℓ ] isSetGrammar A
+
+  Lang→SetGrammar : Lang ℓ → SetGrammar ℓ
+  Lang→SetGrammar L = L .fst , isLang→isSetGrammar (L .snd)
+
+  -- Might be confusing but convenient
+  ⟨_⟩ : SetGrammar ℓ → Grammar ℓ
+  ⟨ A ⟩ = A .fst
diff --git a/code/cubical/Grammar/Inductive/HLevels.agda b/code/cubical/Grammar/Inductive/HLevels.agda
new file mode 100644
index 0000000..9bfe700
--- /dev/null
+++ b/code/cubical/Grammar/Inductive/HLevels.agda
@@ -0,0 +1,163 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.Inductive.HLevels (Alphabet : hSet ℓ-zero)where
+
+open import Cubical.Data.Empty
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+open import Cubical.Data.Unit
+open import Cubical.Data.W.Indexed
+
+open import Helper
+open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
+open import Grammar.Dependent Alphabet
+open import Grammar.Epsilon Alphabet
+open import Grammar.LinearProduct Alphabet
+open import Grammar.Lift Alphabet
+open import Grammar.Inductive.Indexed Alphabet as Inductive
+open import Term.Base Alphabet
+
+private
+  variable ℓG ℓG' ℓ ℓ' ℓ'' ℓ''' : Level
+
+isSetValued : ∀ {A : Type ℓ} → Functor A → Type ℓ
+isSetValued (k g) = isSetGrammar g
+isSetValued {A = A} (Var a) = Unit*
+isSetValued (&e B F) = ∀ b → isSetValued (F b)
+isSetValued (⊕e B F) = isSet B × (∀ b → isSetValued (F b))
+isSetValued (⊗e F G) = isSetValued F × isSetValued G
+
+module _ {A : Type ℓ} where
+  FS : (F : Functor A) → String → Type ℓ
+  FS F = ⟦ F ⟧ (λ a w  → Unit* {ℓ})
+  opaque
+    unfolding _⊗_
+
+    FP : (F : Functor A) → (w : String) → FS F w → Type ℓ
+    FP (k g) w s = ⊥*
+    FP (Var a') w s = Unit*
+    FP (&e B F) w s = Σ[ b ∈ B ] FP (F b) w (s b)
+    FP (⊕e B F) w (b , s) = FP (F b) w s
+    FP (⊗e Fl Fr) _ (((wl , wr), _) , sl , sr) = FP Fl wl sl ⊎ FP Fr wr sr
+
+    F-inX : (F : Functor A) (ix : A × String) (s : FS F (ix .snd))
+      (p : FP F (ix .snd) s)
+      → A × String
+    F-inX (Var a) ix s p = a , (ix .snd)
+    F-inX (&e B F) ix s (b , p) = F-inX (F b) ix (s b) p
+    F-inX (⊕e B F) ix (b , s) p = F-inX (F b) ix s p
+    F-inX (⊗e Fl Fr) ix (sp , sl , sr) (inl p) =
+      F-inX Fl (ix .fst , sp .fst .fst) sl p
+    F-inX (⊗e Fl Fr) ix (sp , sl , sr) (inr p) =
+      F-inX Fr (ix .fst , sp .fst .snd) sr p
+
+  μIW : (A → Functor A) → A × String → Type ℓ
+  μIW F = IW
+    (λ ix → FS (F (ix .fst)) (ix .snd))
+    (λ ix → FP (F (ix .fst)) (ix .snd))
+    λ ix → F-inX (F (ix .fst)) ix
+
+  getShapeF : {g : A → Grammar ℓ'}(F : Functor A)
+    → ∀ w
+    → ⟦ F ⟧ g w → FS F w
+  getShapeF F = Inductive.map F λ a w x → tt*
+
+  opaque
+    unfolding FP _⊗_ ⊗-intro
+    getSubtreeF : (g : A → Grammar ℓ') (F : Functor A)
+      → ∀ w a
+      → (e : ⟦ F ⟧ g w)
+      → (p : FP F w (getShapeF F _ e))
+      →
+      let ix = (F-inX F (a , w) _ p) in
+      g (ix .fst) (ix .snd)
+    getSubtreeF g (Var a') w a e p = e .lower
+    getSubtreeF g (&e B F) w a e (b , p) = getSubtreeF g (F b) w a (e b) p
+    getSubtreeF g (⊕e B F) w a (b , e) p = getSubtreeF g (F b) w a e p
+    getSubtreeF g (⊗e Fl Fr) w a (((wl , wr) , _) , el , er) (inl pl) =
+      getSubtreeF g Fl wl a el pl
+    getSubtreeF g (⊗e Fl Fr) w a (((wl , wr) , _) , el , er) (inr pr) =
+      getSubtreeF g Fr wr a er pr
+
+    nodeF : ∀ {g : A → Grammar ℓ'}(F : Functor A)
+      → ∀ w a
+      → (s : FS F w)
+      → (∀ (p : FP F w s) →
+           let ix = F-inX F (a , w) s p in
+           g (ix .fst) (ix .snd)
+        )
+      → ⟦ F ⟧ g w
+    nodeF (k g) w a s subtree = lift (s .lower)
+    nodeF (Var a') w a s subtree = lift (subtree tt*)
+    nodeF (&e B F) w a s subtree b =
+      nodeF (F b) w a (s b) (λ p → subtree (b , p))
+    nodeF (⊕e B F) w a (b , s) subtree = b , nodeF (F b) w a s subtree
+    nodeF (⊗e Fl Fr) w a (((wl , wr) , w≡wlwr) , sl , sr) subtree =
+      ((wl , wr) , w≡wlwr)
+        , (nodeF Fl wl a sl (λ p → subtree (inl p)))
+        , ((nodeF Fr wr a sr λ p → subtree (inr p)))
+
+    reconstructF : ∀ {g : A → Grammar ℓ'}(F : Functor A)
+      → ∀ w a
+      → (t : ⟦ F ⟧ g w)
+      → nodeF F w a (getShapeF F w t) (getSubtreeF g F w a t) ≡ t
+    reconstructF (k g) w a t = refl
+    reconstructF (Var a') w a t = refl
+    reconstructF (&e B F) w a t i b = reconstructF (F b) w a (t b) i
+    reconstructF (⊕e B F) w a (b , t) i = b , (reconstructF (F b) w a t i)
+    reconstructF (⊗e Fl Fr) w a (((wl , wr), sp) , tl , tr) i =
+      ((wl , wr) , sp) , (reconstructF Fl wl a tl i , reconstructF Fr wr a tr i)
+
+
+    isSet⟦F⟧ : ∀ (F : Functor A)
+      → isSetValued F
+      → (g : A → SetGrammar ℓ')
+      → isSetGrammar (⟦ F ⟧ (λ a → ⟨ g a ⟩))
+    isSet⟦F⟧ (k _) isSetF g = isSetGrammarLift isSetF
+    isSet⟦F⟧ (Var a) isSetF g = isSetGrammarLift (g a .snd)
+    isSet⟦F⟧ (&e B F) isSetF g =
+      isSetGrammar&ᴰ (λ b → isSet⟦F⟧ (F b) (isSetF b) g)
+    isSet⟦F⟧ (⊕e B F) isSetF g =
+      isSetGrammar⊕ᴰ (isSetF .fst) (λ b → isSet⟦F⟧ (F b) (isSetF .snd b) g)
+    isSet⟦F⟧ (⊗e Fl Fr) isSetF g =
+      isSetGrammar⊗ (isSet⟦F⟧ Fl (isSetF .fst) g) (isSet⟦F⟧ Fr (isSetF .snd) g)
+
+    isSetμIW : ∀ (F : A → Functor A) → (∀ a → isSetValued (F a))
+      → ∀ ix → isSet (μIW F ix)
+    isSetμIW F isSetF = isOfHLevelSuc-IW 1 λ ix →
+      isSet⟦F⟧ (F (ix .fst)) (isSetF (ix .fst))
+        (λ x → (λ _ → Lift Unit) , λ _ → isSetUnit*)
+        (ix .snd)
+
+
+  {-# TERMINATING #-}
+  encode : (F : A → Functor A) → ∀ ix → μ F (ix .fst) (ix .snd) → μIW F ix
+  encode F (a , w) (roll .w op⟨m⟩) =
+    node (Inductive.map (F a) (λ _ _ → _) w op⟨m⟩)
+      λ p → encode F _ (getSubtreeF (μ F) (F a) w a _ p)
+
+  decode : (F : A → Functor A) → ∀ ix → μIW F ix → μ F (ix .fst) (ix .snd)
+  decode F (a , w) (node s subtree) =
+    roll _ (nodeF (F a) w a s λ p →
+      decode F (F-inX (F a) (a , w) s p) (subtree p))
+
+  opaque
+    unfolding FP _⊗_ getSubtreeF nodeF
+    {-# TERMINATING #-}
+    isRetract : ∀ (F : A → Functor A) a w
+      → (x : μ F a w) → decode F (a , w) (encode F (a , w) x) ≡ x
+    isRetract F a w (roll .w t) = cong (roll w)
+      (cong (nodeF (F a) w a _) (funExt λ p → isRetract F _ _ _)
+      ∙ reconstructF (F a) w a t)
+
+
+isSetGrammarμ : ∀ {A : Type ℓ}
+  → (F : A → Functor A)
+  → (∀ a → isSetValued (F a))
+  → ∀ a → isSetGrammar (μ F a)
+isSetGrammarμ {A = A} F isSetValuedF a w =
+  isSetRetract (encode F (a , w)) (decode F (a , w)) (isRetract F a w)
+    (isSetμIW F isSetValuedF (a , w))
+
diff --git a/code/cubical/Grammar/Inductive/Indexed.agda b/code/cubical/Grammar/Inductive/Indexed.agda
index 57db5a7..daea061 100644
--- a/code/cubical/Grammar/Inductive/Indexed.agda
+++ b/code/cubical/Grammar/Inductive/Indexed.agda
@@ -5,9 +5,12 @@ open import Cubical.Foundations.HLevels
 module Grammar.Inductive.Indexed (Alphabet : hSet ℓ-zero)where
 
 open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+open import Cubical.Data.Unit
 
 open import Helper
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.Dependent.Base Alphabet
 open import Grammar.LinearProduct Alphabet
 open import Grammar.Lift Alphabet
@@ -133,3 +136,4 @@ module _ where
     unroll' = rec {g = λ a → ⟦ F a ⟧ (μ F)} alg where
       alg : Algebra (λ a → ⟦ F a ⟧ (μ F))
       alg a = map (F a) (λ _ → roll)
+
diff --git a/code/cubical/Grammar/Lift.agda b/code/cubical/Grammar/Lift.agda
index 9f0b834..a05621c 100644
--- a/code/cubical/Grammar/Lift.agda
+++ b/code/cubical/Grammar/Lift.agda
@@ -5,6 +5,7 @@ open import Cubical.Foundations.HLevels
 module Grammar.Lift (Alphabet : hSet ℓ-zero) where
 
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.Equivalence.Base Alphabet
 open import Term.Base Alphabet
 
@@ -32,3 +33,9 @@ module _ ℓ (g : Grammar ℓg) where
   LiftG≅ .inv = lowerG
   LiftG≅ .sec = refl
   LiftG≅ .ret = refl
+
+isLangLift : isLang g → isLang (LiftG ℓ' g)
+isLangLift isLangG w = isOfHLevelLift 1 (isLangG w)
+
+isSetGrammarLift : isSetGrammar g → isSetGrammar (LiftG ℓ' g)
+isSetGrammarLift isSetGrammarG w = isOfHLevelLift 2 (isSetGrammarG w)
diff --git a/code/cubical/Grammar/LinearFunction.agda b/code/cubical/Grammar/LinearFunction.agda
index 30bf57d..b6f4e6b 100644
--- a/code/cubical/Grammar/LinearFunction.agda
+++ b/code/cubical/Grammar/LinearFunction.agda
@@ -9,6 +9,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
 
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.LinearProduct Alphabet
 open import Grammar.Epsilon Alphabet
 open import Term.Base Alphabet
@@ -298,3 +299,9 @@ opaque
   ⟜-intro-natural {f = f}{f' = f'} = ⟜≡ _ _
     ((λ i → ⟜-β f i ∘g (f' ,⊗ id))
     ∙ sym (⟜-β _) )
+
+
+opaque
+  unfolding _⟜_
+  isSetGrammar⟜ : isSetGrammar h → isSetGrammar (h ⟜ g)
+  isSetGrammar⟜ isSetH w = isSetΠ (λ w' → isSet→ (isSetH _))
diff --git a/code/cubical/Grammar/LinearProduct.agda b/code/cubical/Grammar/LinearProduct.agda
index 90091eb..86e0f88 100644
--- a/code/cubical/Grammar/LinearProduct.agda
+++ b/code/cubical/Grammar/LinearProduct.agda
@@ -1,4 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 
@@ -8,6 +7,8 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.List
 
 open import Grammar.Base Alphabet
+open import Grammar.Lift Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.Epsilon Alphabet
 open import Term.Base Alphabet
 open import Term.Bilinear Alphabet
@@ -27,6 +28,11 @@ infixr 5 _⊗'_
 opaque
   _⊗_ : Grammar ℓg → Grammar ℓh → Grammar (ℓ-max ℓg ℓh)
   _⊗_ = _⊗'_
+
+  isSetGrammar⊗ : isSetGrammar g → isSetGrammar h → isSetGrammar (g ⊗ h)
+  isSetGrammar⊗ isSetG isSetH w = isSetΣ (isSetSplitting w)
+    λ _ → isSet× (isSetG _) (isSetH _)
+
 infixr 5 _⊗_
 
 opaque
@@ -114,9 +120,6 @@ opaque
     ⊗-unit-r⁻ _ p =
       ((_ , []) , (sym (++-unit-r _))) , (p , refl)
 
-    isPropε : ∀ w → isProp (ε w)
-    isPropε w = isSetString _ _
-
     rectify :
       ∀ {w w'}{g : Grammar ℓg}
       → {p : g w}{q : g w'}
@@ -141,7 +144,7 @@ opaque
           (sym []'≡[]))
         (ΣPathP
           ( symP (subst-filler g (sym w≡w') p⟨w'⟩)
-          , isProp→PathP (λ _ → isPropε _) refl []'≡[]))
+          , isProp→PathP (λ _ → isLangε _) refl []'≡[]))
 
     ⊗-unit-r⁻r : ∀ {g : Grammar ℓg}
       → ⊗-unit-r {g = g} ∘g ⊗-unit-r⁻ ≡ id
@@ -356,6 +359,100 @@ opaque
 _,⊗_ = ⊗-intro
 infixr 20 _,⊗_
 
+{- ε* versions of the unitors  -}
+⊗-unit*-l : ε* {ℓ} ⊗ g ⊢ g
+⊗-unit*-l = ⊗-unit-l ∘g ⊗-intro lowerG id
+
+⊗-unit*-l⁻ : g ⊢ ε* {ℓ} ⊗ g
+⊗-unit*-l⁻ = ⊗-intro liftG id ∘g ⊗-unit-l⁻
+
+opaque
+  unfolding ⊗-intro
+  ⊗-unit*-l⊗-intro :
+      ∀ (f : g ⊢ h)
+      → f ∘g ⊗-unit*-l {ℓ}
+        ≡ ⊗-unit*-l ∘g (⊗-intro id f)
+  ⊗-unit*-l⊗-intro f =
+    cong₂ _∘g_ (⊗-unit-l⊗-intro f) refl
+  ⊗-unit*-ll⁻ :
+    ⊗-unit*-l⁻ {g = g} {ℓ = ℓ} ∘g ⊗-unit*-l ≡ id
+  ⊗-unit*-ll⁻ i = ⊗-intro liftG id ∘g ⊗-unit-ll⁻ i ∘g ⊗-intro lowerG id
+
+  ⊗-unit*-l⁻l :
+    ⊗-unit*-l {ℓ = ℓ} {g = g} ∘g ⊗-unit*-l⁻ ≡ id
+  ⊗-unit*-l⁻l = ⊗-unit-l⁻l
+
+⊗-unit*-r : g ⊗ ε* {ℓ} ⊢ g
+⊗-unit*-r = ⊗-unit-r ∘g ⊗-intro id lowerG
+
+⊗-unit*-r⁻ : g ⊢ g ⊗ ε* {ℓ}
+⊗-unit*-r⁻ = ⊗-intro id liftG ∘g ⊗-unit-r⁻
+
+opaque
+  unfolding ⊗-intro
+  ⊗-unit*-r⊗-intro :
+      ∀ (f : g ⊢ h)
+      → ⊗-unit*-r {ℓ = ℓ} ∘g (⊗-intro f id)
+        ≡ f ∘g ⊗-unit*-r
+  ⊗-unit*-r⊗-intro {ℓ = ℓ} f = cong₂ _∘g_ (⊗-unit-r⊗-intro f) refl
+
+  ⊗-unit*-rr⁻ :
+    ⊗-unit*-r⁻ {g = g} {ℓ = ℓ} ∘g ⊗-unit*-r ≡ id
+  ⊗-unit*-rr⁻ i = ⊗-intro id liftG ∘g ⊗-unit-rr⁻ i ∘g ⊗-intro id lowerG
+
+  ⊗-unit*-r⁻r :
+    ⊗-unit*-r {g = g} {ℓ = ℓ} ∘g ⊗-unit*-r⁻ ≡ id
+  ⊗-unit*-r⁻r = ⊗-unit-r⁻r
+
+{- Triangle -}
+opaque
+  unfolding ⊗-intro ⊗-unit-r ⊗-unit-l ⊗-assoc
+  ⊗-triangle :
+    ⊗-intro ⊗-unit*-r id ∘g ⊗-assoc {g = g}{h = ε* {ℓ}}{k = h}
+    ≡ ⊗-intro id ⊗-unit*-l
+  ⊗-triangle {g = g}{h = h} = funExt λ w → funExt λ {
+    (((w1 , w2) , w≡w1w2) ,
+     (gp , (((w3 , w4) , w2≡w3w4) , ((lift w3≡[]) , hp)))) →
+    let p1 : w1 ++ w3 ≡ w1
+        p1 = (cong (w1 ++_) w3≡[] ∙ ++-unit-r _)
+        p2 = (cong (_++ w4) (sym w3≡[]) ∙ sym w2≡w3w4)
+        p1' : w1 ≡ w1 ++ w3
+        p1' = λ i → (hcomp
+           (doubleComp-faces (λ _ → w1)
+            (λ i₁ →
+               hcomp (doubleComp-faces (λ _ → w1 ++ []) (λ i₂ → w1 ++ w3) i₁)
+               (w1 ++ w3≡[] (~ i₁)))
+            i)
+           (++-unit-r w1 (~ i)))
+    in
+    ⊗≡ _ _ (≡-× p1 p2)
+     (ΣPathP (rectify {g = g} {w≡ = sym p1'}{w≡' = p1}
+       (symP (transport-filler (cong g p1') gp))
+     , transport-filler (cong h p2) hp))
+    }
+
+{- Pentagon -}
+opaque
+  unfolding ⊗-intro ⊗-assoc
+  ⊗-pentagon :
+    ⊗-intro (⊗-assoc {g = g}) id
+    ∘g ⊗-assoc
+    ∘g ⊗-intro id (⊗-assoc {g = g'}{h = g''}{k = g'''})
+      ≡
+    ⊗-assoc
+    ∘g ⊗-assoc
+  ⊗-pentagon {g = g1}{g' = g2}{g'' = g3}{g''' = g4} =
+    funExt λ w → funExt λ {
+    (((w1 , w234) , w≡w1w234) , p1 ,
+    (((w2 , w34) , w234≡w2w34) , p2 ,
+    (((w3 , w4) , w34≡w3w4) , (p3 , p4)))) →
+    ⊗≡ _ _
+    (≡-× (sym (++-assoc w1 w2 w3)) refl)
+    (ΣPathP ((⊗PathP (≡-× refl refl) refl) , refl))
+    }
+
+{- Big associators and big diagrams -}
+
 ⊗-assoc⁻3 :
   (g ⊗ g' ⊗ g'') ⊗ g''' ⊢ g ⊗ g' ⊗ g'' ⊗ g'''
 ⊗-assoc⁻3 = id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻
@@ -380,19 +477,6 @@ infixr 20 _,⊗_
   g ⊗ g' ⊗ g'' ⊗ g''' ⊗ g'''' ⊢ (g ⊗ g' ⊗ g'' ⊗ g''') ⊗ g''''
 ⊗-assoc4 = ⊗-assoc ∘g id ,⊗ ⊗-assoc3
 
-opaque
-  unfolding ⊗-intro ⊗-assoc ⊗-assoc⁻
-  ⊗-assoc⁻4⊗-assoc :
-    ⊗-assoc⁻4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''}{g'''' = g''''} ,⊗ id {g = g'''''}
-    ∘g ⊗-assoc
-    ≡ ⊗-assoc4 ∘g id ,⊗ id ,⊗ id ,⊗ ⊗-assoc ∘g ⊗-assoc⁻4
-  ⊗-assoc⁻4⊗-assoc = funExt λ w → funExt λ p →
-    ⊗PathP (≡-×
-      ((λ i → p .snd .fst .fst .snd i ++ p .snd .snd .fst .fst .fst)
-       ∙ ++-assoc (p .snd .fst .fst .fst .fst) _ _
-       ∙ {!p .snd  .fst .fst .snd!})
-      refl) (ΣPathP ({!!} , {!!}))
-
 ⊗-assoc⁻4⊗-unit-r⁻ :
   ⊗-assoc⁻4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''} ∘g ⊗-unit-r⁻
   ≡ id ,⊗ id ,⊗ id ,⊗ ⊗-unit-r⁻
@@ -401,25 +485,54 @@ opaque
   ∙ ⊗-intro⊗-intro
   ∙ cong (id ,⊗_) ⊗-assoc⁻3⊗-unit-r⁻
 
-⊗-assoc⁻3⊗-intro :
-  ∀ {f f' f'' f'''} →
-  (⊗-assoc⁻3 {g = g}{g' = g'}{g'' = g''}{g''' = g'''} ∘g (f ,⊗ f' ,⊗ f'') ,⊗ f''')
-  ≡ (f ,⊗ f' ,⊗ f'' ,⊗ f''' ∘g (⊗-assoc⁻3 {g = h}{g' = h'}{g'' = h''}{g''' = h'''}))
-⊗-assoc⁻3⊗-intro =
-  {!!}
-
+-- ⊗-assoc⁻3⊗-intro :
+--   ∀ {f f' f'' f'''} →
+--   (⊗-assoc⁻3 {g = g}{g' = g'}{g'' = g''}{g''' = g'''} ∘g (f ,⊗ f' ,⊗ f'') ,⊗ f''')
+--   ≡ (f ,⊗ f' ,⊗ f'' ,⊗ f''' ∘g (⊗-assoc⁻3 {g = h}{g' = h'}{g'' = h''}{g''' = h'''}))
+-- ⊗-assoc⁻3⊗-intro =
+--   {!!}
 opaque
   unfolding ⊗-intro
   ⊗-assoc⁻4⊗-intro :
     ∀ {f f' f'' f''' f''''} →
     (⊗-assoc⁻4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''}{g'''' = g''''} ∘g (f ,⊗ f' ,⊗ f'' ,⊗ f''') ,⊗ f'''')
     ≡ (f ,⊗ f' ,⊗ f'' ,⊗ f''' ,⊗ f'''' ∘g (⊗-assoc⁻4 {g = h}{g' = h'}{g'' = h''}{g''' = h'''}{g'''' = h''''}))
-  ⊗-assoc⁻4⊗-intro {f = f} {f' = f'} {f'' = f''} {f''' = f'''} {f'''' = f''''} =
-    cong (id ,⊗ ⊗-assoc⁻3 ∘g_) (⊗-assoc⁻⊗-intro {f' = f' ,⊗ f'' ,⊗ f'''})
-    ∙ cong (_∘g ⊗-assoc⁻) {!!} -- (cong (⊗-intro _) ⊗-assoc⁻3⊗-intro {f = ?}{f' = ?}{f'' = ?}{f''' = ?})
-    ∙ {!!}
-
-⊗-assoc4⊗-intro :
-  ⊗-assoc4 ∘g f ,⊗ f' ,⊗ f'' ,⊗ f''' ,⊗ f''''
-  ≡ (f ,⊗ f' ,⊗ f'' ,⊗ f''') ,⊗ f'''' ∘g ⊗-assoc4
-⊗-assoc4⊗-intro = {!!}
+  ⊗-assoc⁻4⊗-intro = refl
+
+opaque
+  unfolding ⊗-intro
+  ⊗-assoc3⊗-assoc⁻3 : ⊗-assoc3 {g = g}{g' = g'}{g'' = g''}{g''' = g'''} ∘g ⊗-assoc⁻3 ≡ id
+  ⊗-assoc3⊗-assoc⁻3 =
+    ⊗-assoc ∘g id ,⊗ ⊗-assoc ∘g id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻
+      ≡⟨ (λ i → ⊗-assoc ∘g id ,⊗ ⊗-assoc∘⊗-assoc⁻≡id i ∘g ⊗-assoc⁻) ⟩
+    ⊗-assoc ∘g ⊗-assoc⁻
+    ≡⟨ ⊗-assoc∘⊗-assoc⁻≡id ⟩ id ∎
+
+  ⊗-assoc4⊗-assoc⁻4 : ⊗-assoc4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''}{g'''' = g''''} ∘g ⊗-assoc⁻4 ≡ id
+  ⊗-assoc4⊗-assoc⁻4 =
+    ⊗-assoc ∘g id ,⊗ ⊗-assoc3 ∘g id ,⊗ ⊗-assoc⁻3 ∘g ⊗-assoc⁻
+      ≡⟨ (λ i → ⊗-assoc ∘g id ,⊗ ⊗-assoc3⊗-assoc⁻3 i ∘g ⊗-assoc⁻) ⟩
+    ⊗-assoc ∘g ⊗-assoc⁻
+      ≡⟨ ⊗-assoc∘⊗-assoc⁻≡id ⟩
+    id ∎
+
+  ⊗-assoc⁻3⊗-assoc3 : ⊗-assoc⁻3 {g = g}{g' = g'}{g'' = g''}{g''' = g'''} ∘g ⊗-assoc3 ≡ id
+  ⊗-assoc⁻3⊗-assoc3 =
+    id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻ ∘g ⊗-assoc ∘g id ,⊗ ⊗-assoc
+      ≡⟨ (λ i → id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻∘⊗-assoc≡id i ∘g id ,⊗ ⊗-assoc) ⟩
+    id ,⊗ (⊗-assoc⁻ ∘g ⊗-assoc) ≡⟨ ((λ i → id ,⊗ ⊗-assoc⁻∘⊗-assoc≡id i)) ⟩
+    id ∎
+
+  ⊗-assoc⁻4⊗-assoc4 : ⊗-assoc⁻4 {g = g}{g' = g'}{g'' = g''}{g''' = g'''}{g'''' = g''''} ∘g ⊗-assoc4 ≡ id
+  ⊗-assoc⁻4⊗-assoc4 =
+    id ,⊗ ⊗-assoc⁻3 ∘g ⊗-assoc⁻ ∘g ⊗-assoc ∘g id ,⊗ ⊗-assoc3
+      ≡⟨ (λ i → id ,⊗ ⊗-assoc⁻3 ∘g ⊗-assoc⁻∘⊗-assoc≡id i ∘g id ,⊗ ⊗-assoc3) ⟩
+    id ,⊗ (⊗-assoc⁻3 ∘g ⊗-assoc3) ≡⟨ ((λ i → id ,⊗ ⊗-assoc⁻3⊗-assoc3 i)) ⟩
+    id ∎
+
+  ⊗-assoc4⊗-intro :
+    ⊗-assoc4 ∘g f ,⊗ f' ,⊗ f'' ,⊗ f''' ,⊗ f''''
+    ≡ (f ,⊗ f' ,⊗ f'' ,⊗ f''') ,⊗ f'''' ∘g ⊗-assoc4
+  ⊗-assoc4⊗-intro {f = f}{f' = f'}{f'' = f''}{f''' = f'''}{f'''' = f''''} =
+    sym (invMoveR {f = ⊗-assoc⁻4} {f⁻ = ⊗-assoc4} ⊗-assoc4⊗-assoc⁻4
+      (cong ((f ,⊗ f' ,⊗ f'' ,⊗ f''' ,⊗ f'''') ∘g_) ⊗-assoc⁻4⊗-assoc4))
diff --git a/code/cubical/Grammar/Literal.agda b/code/cubical/Grammar/Literal.agda
index d5b331e..743ab46 100644
--- a/code/cubical/Grammar/Literal.agda
+++ b/code/cubical/Grammar/Literal.agda
@@ -9,6 +9,7 @@ open import Cubical.Data.List
 
 open import Grammar.Base Alphabet
 open import Grammar.Lift Alphabet
+open import Grammar.HLevels Alphabet hiding (⟨_⟩)
 open import Term.Base Alphabet
 
 private
@@ -25,5 +26,11 @@ opaque
   literal-elim {g = g} gc w w≡[c] =
     subst g (sym w≡[c]) gc
 
+  isLangLiteral : ∀ c → isLang (literal c)
+  isLangLiteral c w = isSetString w [ c ]
+
+isSetGrammarLiteral : ∀ c → isSetGrammar (literal c)
+isSetGrammarLiteral c = isLang→isSetGrammar (isLangLiteral c)
+
 literal* : ∀ {ℓ : Level} → ⟨ Alphabet ⟩ → Grammar ℓ
 literal* {ℓ = ℓ} c = LiftG ℓ (literal c)
diff --git a/code/cubical/Grammar/Top/Properties.agda b/code/cubical/Grammar/Top/Properties.agda
index ade52bd..642c5ff 100644
--- a/code/cubical/Grammar/Top/Properties.agda
+++ b/code/cubical/Grammar/Top/Properties.agda
@@ -5,6 +5,7 @@ open import Cubical.Foundations.Structure
 module Grammar.Top.Properties (Alphabet : hSet ℓ-zero) where
 
 open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
 open import Grammar.Properties Alphabet
 open import Grammar.Top.Base Alphabet
 open import Term.Base Alphabet
@@ -30,3 +31,10 @@ opaque
 unambiguous⊤* : ∀ {ℓg} → unambiguous (⊤* {ℓg})
 unambiguous⊤* = unambiguous'→unambiguous unambiguous'⊤*
 
+opaque
+  unfolding ⊤
+  isLang⊤ : isLang ⊤
+  isLang⊤ w x y = refl
+
+isSetGrammar⊤ : isSetGrammar ⊤
+isSetGrammar⊤ = isLang→isSetGrammar isLang⊤
diff --git a/code/cubical/Term/Base.agda b/code/cubical/Term/Base.agda
index 08124d5..018d0fa 100644
--- a/code/cubical/Term/Base.agda
+++ b/code/cubical/Term/Base.agda
@@ -74,3 +74,14 @@ transportG {g = g}{h = h} p = subst (λ h → g ⊢ h) p id
 transportGRefl :
   transportG {g = g} refl ≡ id
 transportGRefl {g = g} = substRefl {B = λ h → g ⊢ h} _
+
+invMoveR :
+  {f : g ⊢ h} {f⁻ : h ⊢ g}
+  {f' : k ⊢ g} {f'' : k ⊢ h}
+  → f⁻ ∘g f ≡ id
+  → f ∘g f' ≡ f''
+  → f' ≡ f⁻ ∘g f''
+invMoveR {f = f}{f⁻}{f'}{f''} retr p =
+  f' ≡⟨ cong (_∘g f') (sym retr) ⟩
+  f⁻ ∘g f ∘g f' ≡⟨ cong (f⁻ ∘g_) p ⟩
+  f⁻ ∘g f'' ∎
diff --git a/code/cubical/Term/Category.agda b/code/cubical/Term/Category.agda
new file mode 100644
index 0000000..b7f8b82
--- /dev/null
+++ b/code/cubical/Term/Category.agda
@@ -0,0 +1,61 @@
+{- Monoidal Category of SetGrammars and Terms for a fixed hLevel -}
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Term.Category (Alphabet : hSet ℓ-zero) where
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Monoidal.Base
+
+open import Grammar.Base Alphabet
+open import Grammar.HLevels Alphabet
+open import Grammar.Epsilon Alphabet
+open import Grammar.LinearProduct Alphabet as LP
+open import Term.Base Alphabet as Term
+
+module _ (ℓ : Level) where
+  open MonoidalCategory
+  open TensorStr
+  open MonoidalStr
+  open Category
+  open Functor
+  open NatTrans
+  open NatIso
+  open isIso
+  |GRAMMAR| : Category (ℓ-suc ℓ) ℓ
+  |GRAMMAR| .ob = SetGrammar ℓ
+  |GRAMMAR| .Hom[_,_] A B = Term ⟨ A ⟩ ⟨ B ⟩
+  |GRAMMAR| .Category.id = Term.id
+  |GRAMMAR| ._⋆_ = Term.seq
+  |GRAMMAR| .⋆IdL _ = refl
+  |GRAMMAR| .⋆IdR _ = refl
+  |GRAMMAR| .⋆Assoc _ _ _ = refl
+  |GRAMMAR| .isSetHom {y = B} = isSetΠ (λ w → isSet→ (B .snd w))
+
+  GRAMMAR : MonoidalCategory (ℓ-suc ℓ) ℓ
+  GRAMMAR .C = |GRAMMAR|
+  GRAMMAR .monstr .tenstr .unit = ε* , isSetGrammarε*
+  GRAMMAR .monstr .tenstr .─⊗─ .F-ob (A , B) =
+    ⟨ A ⟩ LP.⊗ ⟨ B ⟩ , isSetGrammar⊗ (A .snd) (B .snd)
+  GRAMMAR .monstr .tenstr .─⊗─ .F-hom (f , g) = f ,⊗ g
+  GRAMMAR .monstr .tenstr .─⊗─ .F-id = id,⊗id≡id
+  GRAMMAR .monstr .tenstr .─⊗─ .F-seq _ _ = sym ⊗-intro⊗-intro
+  GRAMMAR .monstr .α .trans .N-ob ABC = ⊗-assoc
+  GRAMMAR .monstr .α .trans .N-hom fgh = ⊗-assoc⊗-intro
+  GRAMMAR .monstr .α .nIso ABC .inv = ⊗-assoc⁻
+  GRAMMAR .monstr .α .nIso ABC .sec = ⊗-assoc∘⊗-assoc⁻≡id
+  GRAMMAR .monstr .α .nIso ABC .ret = ⊗-assoc⁻∘⊗-assoc≡id
+  GRAMMAR .monstr .η .trans .N-ob A = ⊗-unit*-l
+  GRAMMAR .monstr .η .trans .N-hom f = sym (⊗-unit*-l⊗-intro f)
+  GRAMMAR .monstr .η .nIso A .inv = ⊗-unit*-l⁻
+  GRAMMAR .monstr .η .nIso A .sec = ⊗-unit*-l⁻l
+  GRAMMAR .monstr .η .nIso A .ret = ⊗-unit*-ll⁻
+  GRAMMAR .monstr .ρ .trans .N-ob A = ⊗-unit*-r
+  GRAMMAR .monstr .ρ .trans .N-hom f = ⊗-unit*-r⊗-intro f
+  GRAMMAR .monstr .ρ .nIso A .inv = ⊗-unit*-r⁻
+  GRAMMAR .monstr .ρ .nIso A .sec = ⊗-unit*-r⁻r
+  GRAMMAR .monstr .ρ .nIso A .ret = ⊗-unit*-rr⁻
+  GRAMMAR .monstr .pentagon A B C D = ⊗-pentagon
+  GRAMMAR .monstr .triangle A B = ⊗-triangle