From d127d1fa759b192edd2a4967b261c0be44af37c2 Mon Sep 17 00:00:00 2001
From: "Max S. New" <maxsnew@gmail.com>
Date: Fri, 27 Sep 2024 11:45:14 -0400
Subject: [PATCH] Indexed grammars as a LFP of an endofunctor (#18)

* a generic definition of (non-indexed) inductive grammars (uses TERMINATING)

* syntax for LinPi/Sigma that matches the paper syntax better

* wip on indexed inductives

* Kleene star via mu

* wip on porting the Dyck example to indexed mu

* port the Dyck example to indexed inductives

* id/comp for indexed inductive algebra homomorphisms

* induction principle and case analysis for indexed inductives

* Compatibility with opaque tensor

---------

Co-authored-by: Steven Schaefer <stschaef@umich.edu>
---
 code/cubical/Examples/Indexed/Dyck.agda     | 110 ++++++++++++++
 code/cubical/Grammar/Dependent/Base.agda    |   8 ++
 code/cubical/Grammar/Inductive.agda         | 151 ++++++++++++++++++++
 code/cubical/Grammar/Inductive/Indexed.agda | 117 +++++++++++++++
 code/cubical/Grammar/LinearFunction.agda    |  15 +-
 5 files changed, 399 insertions(+), 2 deletions(-)
 create mode 100644 code/cubical/Examples/Indexed/Dyck.agda
 create mode 100644 code/cubical/Grammar/Inductive.agda
 create mode 100644 code/cubical/Grammar/Inductive/Indexed.agda

diff --git a/code/cubical/Examples/Indexed/Dyck.agda b/code/cubical/Examples/Indexed/Dyck.agda
new file mode 100644
index 0000000..fd8fbd3
--- /dev/null
+++ b/code/cubical/Examples/Indexed/Dyck.agda
@@ -0,0 +1,110 @@
+{-# OPTIONS -WnoUnsupportedIndexedMatch #-}
+module Examples.Indexed.Dyck where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Bool as Bool hiding (_⊕_ ;_or_)
+import Cubical.Data.Equality as Eq
+open import Cubical.Data.Nat as Nat
+open import Cubical.Data.List hiding (init; rec)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as Sum hiding (rec)
+open import Cubical.Data.FinSet
+
+private
+  variable
+    ℓg : Level
+
+open import Examples.Dyck
+open import Grammar Alphabet
+open import Grammar.Maybe Alphabet hiding (μ)
+open import Grammar.Equivalence Alphabet
+open import Grammar.Inductive.Indexed Alphabet
+open import Term Alphabet
+
+data DyckTag : Type ℓ-zero where
+  nil' balanced' : DyckTag
+DyckTy : Unit → Functor Unit
+DyckTy _ = ⊕e DyckTag (λ
+  { nil' → k ε
+  ; balanced' → ⊗e (k (literal [)) (⊗e (Var _) (⊗e (k (literal ])) (Var _))) })
+IndDyck : Grammar ℓ-zero
+IndDyck = μ DyckTy _
+
+data TraceTag : Type where
+  eof' open' close' leftovers' unexpected' : TraceTag
+TraceTys : ℕ × Bool → Functor (ℕ × Bool)
+TraceTys (n , b) = ⊕e TraceTag (λ
+  { eof' → ⊕e (n Eq.≡ zero) (λ _ → ⊕e (b Eq.≡ true) λ _ → k ε)
+  ; open' → ⊗e (k (literal [)) (Var (suc n , b))
+  ; close' → ⊕e (Eq.fiber suc n) λ (n-1 , _) → ⊗e (k (literal ])) (Var (n-1 , b))
+  ; leftovers' → ⊕e (Eq.fiber suc n) λ (n-1 , _) → ⊕e (b Eq.≡ false) λ _ → k ε
+  ; unexpected' → ⊕e ((n , b) Eq.≡ (0 , false)) λ _ → ⊗e (k (literal ])) (k ⊤)
+  })
+
+Trace : ℕ → Bool → Grammar ℓ-zero
+Trace n b = μ TraceTys (n , b)
+
+opaque
+  unfolding _⊗_ ⊗-intro
+  parse : string ⊢ &[ n ∈ ℕ ] ⊕[ b ∈ _ ] Trace n b
+  parse = foldKL*r _ (record { the-ℓ = ℓ-zero ; G = _
+    ; nil-case = LinΠ-intro (Nat.elim
+      (LinΣ-intro true ∘g roll ∘g LinΣ-intro eof' ∘g LinΣ-intro Eq.refl ∘g LinΣ-intro Eq.refl ∘g id)
+      (λ n-1 _ → LinΣ-intro false ∘g roll ∘g LinΣ-intro leftovers' ∘g LinΣ-intro (_ , Eq.refl) ∘g LinΣ-intro Eq.refl ∘g id))
+    ; cons-case = LinΠ-intro λ n → ⟜-intro⁻ (LinΣ-elim (λ
+      { [ → ⟜-intro {k = Goal n} (⊸-intro⁻ (
+        (LinΣ-elim λ b → ⊸-intro {k = Goal n}
+          (LinΣ-intro b ∘g roll ∘g LinΣ-intro open'))
+        ∘g LinΠ-app (suc n)))
+      ; ] → ⟜-intro {k = Goal n} (Nat.elim {A = λ n → _ ⊢ Goal n}
+          (LinΣ-intro false ∘g roll ∘g LinΣ-intro unexpected' ∘g LinΣ-intro Eq.refl ∘g id ,⊗ ⊤-intro)
+          (λ n-1 _ →
+          ⊸-intro⁻ ((LinΣ-elim λ b → ⊸-intro {k = Goal (suc n-1)} (LinΣ-intro b ∘g roll ∘g LinΣ-intro close' ∘g LinΣ-intro (_ , Eq.refl)))
+            ∘g LinΠ-app n-1))
+          n) })) })
+    where
+      Goal : ℕ → Grammar ℓ-zero
+      Goal n = ⊕[ b ∈ Bool ] Trace n b
+
+  mkTree : Trace zero true ⊢ IndDyck
+  mkTree = ⊗-unit-r ∘g rec TraceTys alg (0 , true) where
+    Stk : ℕ → Grammar ℓ-zero
+    Stk = Nat.elim ε λ _ Stk⟨n⟩ → literal ] ⊗ IndDyck ⊗ Stk⟨n⟩
+    GenIndDyck : ℕ × Bool → Grammar ℓ-zero
+    GenIndDyck (n , false) = ⊤
+    GenIndDyck (n , true) = IndDyck ⊗ Stk n
+    alg : Algebra TraceTys GenIndDyck
+    alg (n , b) = LinΣ-elim (λ
+      { eof' → LinΣ-elim (λ { Eq.refl → LinΣ-elim λ { Eq.refl → (roll ∘g LinΣ-intro nil') ,⊗ id ∘g ⊗-unit-r⁻ } })
+      ; open' → Bool.elim {A = λ b → literal [ ⊗ GenIndDyck (suc n , b)  ⊢ GenIndDyck (n , b)}
+          (⟜4⊗ (⟜4-intro-ε (roll ∘g LinΣ-intro balanced')))
+          ⊤-intro b
+      ; close' → LinΣ-elim (λ { (n-1 , Eq.refl) → Bool.elim
+                                                   {A =
+                                                    λ b →
+                                                      Term (literal ] ⊗ GenIndDyck (n-1 , b)) (GenIndDyck (suc n-1 , b))}
+        (⟜0⊗ (roll ∘g LinΣ-intro nil'))
+        ⊤-intro
+        b } )
+      ; leftovers' → LinΣ-elim λ { (n-1 , Eq.refl) → LinΣ-elim λ { Eq.refl → ⊤-intro } }
+      ; unexpected' → LinΣ-elim λ { Eq.refl → ⊤-intro }
+      })
+
+  exhibitTrace' : IndDyck ⊢ Trace zero true
+  exhibitTrace' = ((⟜-app ∘g ⊸0⊗ (roll ∘g LinΣ-intro eof' ∘g LinΣ-intro Eq.refl ∘g LinΣ-intro Eq.refl)) ∘g LinΠ-app 0) ∘g rec DyckTy alg _ where
+    Goal : Unit → Grammar ℓ-zero
+    Goal _ = &[ n ∈ ℕ ] (Trace n true ⟜ Trace n true)
+    alg : Algebra DyckTy Goal
+    alg _ = LinΣ-elim (λ
+      { nil' → LinΠ-intro (λ n → ⟜-intro-ε id)
+      ; balanced' → LinΠ-intro λ n → ⟜-intro {k = Trace n true}
+        (roll ∘g LinΣ-intro open'
+        ∘g id ,⊗ ((⟜-app ∘g LinΠ-app (suc n) ,⊗ ((roll ∘g LinΣ-intro close' ∘g LinΣ-intro (_ , Eq.refl) ∘g id ,⊗ (⟜-app ∘g LinΠ-app n ,⊗ id)) ∘g ⊗-assoc⁻)) ∘g ⊗-assoc⁻)
+        ∘g ⊗-assoc⁻)
+      })
diff --git a/code/cubical/Grammar/Dependent/Base.agda b/code/cubical/Grammar/Dependent/Base.agda
index 74e4d4b..1d303d5 100644
--- a/code/cubical/Grammar/Dependent/Base.agda
+++ b/code/cubical/Grammar/Dependent/Base.agda
@@ -24,15 +24,23 @@ LinearΠ {A = A} f w = ∀ (a : A) → f a w
 LinearΣ : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
 LinearΣ {A = A} f w = Σ[ a ∈ A ] f a w
 
+Dep⊕-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
+Dep⊕-syntax = LinearΣ
+
 LinearΣ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
 LinearΣ-syntax = LinearΣ
 
+Dep&-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
+Dep&-syntax = LinearΠ
+
 LinearΠ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
 LinearΠ-syntax = LinearΠ
 
 -- TODO: this precedence isn't really right
 syntax LinearΣ-syntax {A = A} (λ x → B) = LinΣ[ x ∈ A ] B
+syntax Dep⊕-syntax {A = A} (λ x → B) = ⊕[ x ∈ A ] B
 syntax LinearΠ-syntax {A = A} (λ x → B) = LinΠ[ x ∈ A ] B
+syntax Dep&-syntax {A = A} (λ x → B) = &[ x ∈ A ] B
 
 module _ {A : Type ℓS} {g : Grammar ℓG}{h : A → Grammar ℓH} where
   LinΠ-intro : (∀ a → g ⊢ h a) → g ⊢ LinΠ[ a ∈ A ] h a
diff --git a/code/cubical/Grammar/Inductive.agda b/code/cubical/Grammar/Inductive.agda
new file mode 100644
index 0000000..f457e55
--- /dev/null
+++ b/code/cubical/Grammar/Inductive.agda
@@ -0,0 +1,151 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.Inductive (Alphabet : hSet ℓ-zero)where
+
+open import Cubical.Foundations.Structure
+
+open import Helper
+open import Grammar Alphabet
+open import Term Alphabet
+
+private
+  variable ℓG ℓG' ℓ ℓ' : Level
+
+module _ where
+  data Endofunctor ℓ : Type (ℓ-suc ℓ) where
+    k : Grammar ℓ → Endofunctor ℓ
+    Var : Endofunctor ℓ -- identity
+    &e ⊕e : ∀ (X : Type ℓ) → (X → Endofunctor ℓ) → Endofunctor ℓ
+    ⊗e : Endofunctor ℓ → Endofunctor ℓ → Endofunctor ℓ
+
+  ⟦_⟧ : Endofunctor ℓ → Grammar ℓ → Grammar ℓ
+  ⟦ k x ⟧ g = x
+  ⟦ Var ⟧ g = g
+  ⟦ &e X F_x ⟧ g = LinΠ[ x ∈ X ] (⟦ F_x x ⟧ g)
+  ⟦ ⊕e X F_x ⟧ g = LinΣ[ x ∈ X ] (⟦ F_x x ⟧ g)
+  ⟦ ⊗e F F' ⟧ g = ⟦ F ⟧ g ⊗' ⟦ F' ⟧ g
+
+  opaque
+    unfolding _⊗_ ⊗-intro
+    map : ∀ (F : Endofunctor ℓ) {g h} → g ⊢ h → ⟦ F ⟧ g ⊢ ⟦ F ⟧ h
+    map (k x) f    = id
+    map Var f      = f
+    map (&e X Fx) f = LinΠ-intro λ x → map (Fx x) f ∘g LinΠ-app x
+    map (⊕e X Fx) f = LinΣ-elim (λ x → LinΣ-intro x ∘g map (Fx x) f)
+    map (⊗e F G) f = map F f ,⊗ map G f
+
+    map-id : ∀ (F : Endofunctor ℓ) {g} → map F (id {g = g}) ≡ id
+    map-id (k h) i w x = x
+    map-id Var i w x = x
+    map-id (&e A F) i w x a = map-id (F a) i w (x a)
+    map-id (⊕e A F) i w (a , x) = a , (map-id (F a) i w x)
+    map-id (⊗e F F') i w (sp , x , x') = sp , map-id F i _ x , map-id F' i _ x'
+
+    map-∘ :  ∀ (F : Endofunctor ℓ) {g h k} (f : h ⊢ k)(f' : g ⊢ h)
+      → map F (f ∘g f') ≡ map F f ∘g map F f'
+    map-∘ (k g') f f' i w x = x
+    map-∘ Var f f' i w x = f w (f' w x)
+    map-∘ (&e A F) f f' i w  x   a  = map-∘ (F a) f f' i w (x a)
+    map-∘ (⊕e A F) f f' i w (a , x) = a , map-∘ (F a) f f' i w x
+    map-∘ (⊗e F F') f f' i w (sp , x , x') = sp , map-∘ F f f' i _ x , map-∘ F' f f' i _ x'
+
+  data μ (F : Endofunctor ℓ) : Grammar ℓ where
+    roll : ⟦ F ⟧ (μ F) ⊢ μ F
+
+  module _ (F : Endofunctor ℓ) where
+    Algebra : Grammar ℓ → Type _
+    Algebra X = ⟦ F ⟧ X ⊢ X
+
+    initialAlgebra : Algebra (μ F)
+    initialAlgebra = roll
+
+    Homomorphism : ∀ {g h} → Algebra g → Algebra h → Type _
+    Homomorphism {g = g}{h = h} ϕ ψ = Σ[ f ∈ g ⊢ h ]
+      f ∘g ϕ ≡ ψ ∘g map F f
+
+    idHomo : ∀ {g} → (ϕ : Algebra g) → Homomorphism ϕ ϕ
+    idHomo ϕ = id , λ i → ϕ ∘g map-id F (~ i)
+
+    compHomo : ∀ {g h k} (ϕ : Algebra g)(ψ : Algebra h)(χ : Algebra k)
+      → Homomorphism ψ χ → Homomorphism ϕ ψ
+      → Homomorphism ϕ χ
+    compHomo ϕ ψ χ α β = (α .fst ∘g β .fst) ,
+      ( (λ i → α .fst ∘g β .snd i)
+      ∙ (λ i → α .snd i ∘g map F (β .fst))
+      ∙ (λ i → χ ∘g map-∘ F (α .fst) (β .fst) (~ i)))
+
+  {-# TERMINATING #-}
+  rec : ∀ {F : Endofunctor ℓ}{X} → Algebra F X → μ F ⊢ X
+  rec {F = F} alg w (roll _ x) = alg w (map F (rec alg) w x)
+
+  μ-β : ∀ {F : Endofunctor ℓ}{X} → (alg : Algebra F X) → rec {F = F} alg ∘g roll ≡ alg ∘g map F (rec {F = F} alg)
+  μ-β alg = refl
+
+
+  module _ {F : Endofunctor ℓ}{X} (alg : Algebra F X) (ϕ : Homomorphism F (initialAlgebra F) alg) where
+    private
+      {-# TERMINATING #-}
+      μ-η' : ∀ w x → ϕ .fst w x ≡ rec alg w x
+      μ-η' w (roll _ x) = funExt⁻ (funExt⁻ (ϕ .snd) _) x
+        ∙ cong (alg _) (funExt⁻ (funExt⁻ (cong (map F) (funExt λ _ → funExt (μ-η' _))) w) x)
+
+    μ-η : ϕ .fst ≡ rec alg
+    μ-η = funExt λ w → funExt (μ-η' w)
+
+  μ-ind : ∀ {F : Endofunctor ℓ}{X} (alg : Algebra F X) (ϕ ϕ' : Homomorphism F (initialAlgebra F) alg)
+    → ϕ .fst ≡ ϕ' .fst
+  μ-ind α ϕ ϕ' = μ-η α ϕ ∙ sym (μ-η α ϕ')
+
+  μ-ind-id : ∀ {F : Endofunctor ℓ} (ϕ : Homomorphism F (initialAlgebra F) (initialAlgebra F))
+    → ϕ .fst ≡ id
+  μ-ind-id {F = F} ϕ = μ-ind (initialAlgebra F) ϕ (idHomo F (initialAlgebra F))
+
+open import Cubical.Data.Bool
+module _ (g : Grammar ℓ-zero) where
+  -- TODO define sugar for binary sum via Σ[ bool ]
+  *endo : Endofunctor ℓ-zero
+  *endo = ⊕e Bool (λ { false → k ε ; true → ⊗e (k g) Var})
+
+  * : Grammar ℓ-zero
+  * = μ *endo
+
+  opaque
+    unfolding _⊗_
+    open *r-Algebra
+    KLalg : *r-Algebra g
+    KLalg .the-ℓ = ℓ-zero
+    KLalg .G = *
+    KLalg .nil-case = roll ∘g LinΣ-intro false
+    KLalg .cons-case = roll ∘g LinΣ-intro true
+
+    KL*→* : KL* g ⊢ *
+    KL*→* = foldKL*r g KLalg
+
+  *alg : Algebra *endo (KL* g)
+  *alg w (false , x) = nil w x
+  *alg w (true , x) = cons w x
+
+  *→KL* : * ⊢ KL* g
+  *→KL* = rec *alg
+
+  opaque
+    unfolding *r-initial KL*→* KL*r-elim map
+    open import Grammar.Equivalence Alphabet
+    open StrongEquivalence
+    *≅KL* : StrongEquivalence * (KL* g)
+    *≅KL* .fun = *→KL*
+    *≅KL* .inv = KL*→*
+    *≅KL* .sec =
+      !*r-AlgebraHom g (*r-initial g)
+        (record {
+          f = *→KL* ∘g KL*→*
+        ; on-nil = refl
+        ; on-cons = refl })
+        (id*r-AlgebraHom g (*r-initial g))
+    *≅KL* .ret =
+      μ-ind-id
+        (KL*→* ∘g *→KL* ,
+        funExt (λ w → funExt λ {
+          (false , x) → refl
+        ; (true , x) → refl }))
diff --git a/code/cubical/Grammar/Inductive/Indexed.agda b/code/cubical/Grammar/Inductive/Indexed.agda
new file mode 100644
index 0000000..3eaf55e
--- /dev/null
+++ b/code/cubical/Grammar/Inductive/Indexed.agda
@@ -0,0 +1,117 @@
+{- An indexed inductive type is basically just a mutually inductive type -}
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.Inductive.Indexed (Alphabet : hSet ℓ-zero)where
+
+open import Cubical.Foundations.Structure
+
+open import Helper
+open import Grammar Alphabet
+open import Term Alphabet
+
+private
+  variable ℓG ℓG' ℓ ℓ' : Level
+
+module _ where
+  data Functor (A : Type ℓ) : Type (ℓ-suc ℓ) where
+    k : (g : Grammar ℓ) → Functor A
+    Var : (a : A) → Functor A -- reference one of the mutually inductive types being defined
+    &e ⊕e : ∀ (B : Type ℓ) → (F : B → Functor A) → Functor A
+    ⊗e : (F : Functor A) → (F' : Functor A) → Functor A
+
+  ⟦_⟧ : {A : Type ℓ} → Functor A → (A → Grammar ℓ) → Grammar ℓ
+  ⟦ k h ⟧ g = h
+  ⟦ Var a ⟧ g = g a
+  ⟦ &e B F ⟧ g = &[ b ∈ B ] ⟦ F b ⟧ g
+  ⟦ ⊕e B F ⟧ g = ⊕[ b ∈ B ] ⟦ F b ⟧ g
+  ⟦ ⊗e F F' ⟧ g = ⟦ F ⟧ g ⊗' ⟦ F' ⟧ g
+
+  module _ {A : Type ℓ} where
+    opaque
+      unfolding _⊗_ ⊗-intro
+      map : ∀ (F : Functor A) {g h : A → Grammar ℓ}
+        → (∀ a → g a ⊢ h a)
+        → ⟦ F ⟧ g ⊢ ⟦ F ⟧ h
+      map (k g) f = id
+      map (Var a) f = f a
+      map (&e B F) f = LinΠ-intro λ a → map (F a) f ∘g LinΠ-app a
+      map (⊕e B F) f = LinΣ-elim λ a → LinΣ-intro a ∘g map (F a) f
+      map (⊗e F F') f = map F f ,⊗ map F' f
+
+      map-id : ∀ (F : Functor A) {g : A → Grammar _} →
+        map F (λ a → id {g = g a}) ≡ id
+      map-id (k g) i = id
+      map-id (Var a) i = id
+      map-id (&e B F) i = LinΠ-intro (λ a → map-id (F a) i ∘g LinΠ-app a)
+      map-id (⊕e B F) i = LinΣ-elim (λ a → LinΣ-intro a ∘g map-id (F a) i)
+      map-id (⊗e F F') i = map-id F i ,⊗ map-id F' i
+
+      map-∘ :  ∀ (F : Functor A) {g h k : A → Grammar _} (f : ∀ a → h a  ⊢ k a)(f' : ∀ a → g a ⊢ h a)
+        → map F (λ a → f a ∘g f' a) ≡ map F f ∘g map F f'
+      map-∘ (k g) f f' i = id
+      map-∘ (Var a) f f' i = f a ∘g f' a
+      map-∘ (&e B F) f f' i = LinΠ-intro (λ a → map-∘ (F a) f f' i ∘g LinΠ-app a)
+      map-∘ (⊕e B F) f f' i = LinΣ-elim (λ a → LinΣ-intro a ∘g map-∘ (F a) f f' i)
+      map-∘ (⊗e F F') f f' i = map-∘ F f f' i ,⊗ map-∘ F' f f' i
+
+    data μ (F : A → Functor A) a : Grammar ℓ where
+      roll : ⟦ F a ⟧ (μ F) ⊢ μ F a
+
+  module _ {A : Type ℓ} (F : A → Functor A) where
+    Algebra : (A → Grammar ℓ) → Type _
+    Algebra g = ∀ a → ⟦ F a ⟧ g ⊢ g a
+
+    initialAlgebra : Algebra (μ F)
+    initialAlgebra = λ a → roll
+
+    Homomorphism : ∀ {g h} → Algebra g → Algebra h → Type _
+    Homomorphism {g = g}{h} α β =
+      Σ[ ϕ ∈ (∀ a → g a ⊢ h a) ]
+      (∀ a → ϕ a ∘g α a ≡ β a ∘g map (F a) ϕ)
+
+    idHomo : ∀ {g} → (α : Algebra g) → Homomorphism α α
+    idHomo α = (λ a → id) , λ a → cong (α a ∘g_) (sym (map-id (F a)))
+
+    compHomo : ∀ {g h k} (α : Algebra g)(β : Algebra h)(η : Algebra k)
+      → Homomorphism β η → Homomorphism α β → Homomorphism α η
+    compHomo α β η ϕ ψ .fst a = ϕ .fst a ∘g ψ .fst a
+    compHomo α β η ϕ ψ .snd a =
+      cong (ϕ .fst a ∘g_) (ψ .snd a)
+      ∙ cong (_∘g map (F a) (ψ .fst)) (ϕ .snd a)
+      ∙ cong (η a ∘g_) (sym (map-∘ (F a) (ϕ .fst) (ψ .fst)))
+
+    {-# TERMINATING #-}
+    recHomo : ∀ {g} → (α : Algebra g) → Homomorphism initialAlgebra α
+    recHomo α .fst a w (roll ._ x) =
+      α a w (map (F a) (recHomo α .fst) w x)
+    recHomo α .snd a = refl
+
+    rec : ∀ {g} → (α : Algebra g) → ∀ a → (μ F a) ⊢ g a
+    rec α = recHomo α .fst
+
+    module _ {g} (α : Algebra g) (ϕ : Homomorphism initialAlgebra α) where
+      private
+        {-# TERMINATING #-}
+        μ-η' : ∀ a w x → ϕ .fst a w x ≡ rec α a w x
+        μ-η' a w (roll _ x) =
+          (λ i → ϕ .snd a i w x)
+          ∙ λ i → α a w (map (F a) (λ a w x → μ-η' a w x i) w x)
+      μ-η : ϕ .fst ≡ rec α
+      μ-η = funExt (λ a → funExt λ w → funExt λ x → μ-η' a w x)
+
+    ind : ∀ {g} (α : Algebra g) (ϕ ϕ' : Homomorphism initialAlgebra α) → ϕ .fst ≡ ϕ' .fst
+    ind α ϕ ϕ' = μ-η α ϕ ∙ sym (μ-η α ϕ')
+
+    ind-id : ∀ (ϕ : Homomorphism initialAlgebra initialAlgebra) → ϕ .fst ≡ idHomo initialAlgebra .fst
+    ind-id ϕ = ind initialAlgebra ϕ (idHomo initialAlgebra)
+
+
+    unroll : ∀ a → μ F a ⊢ ⟦ F a ⟧ (μ F)
+    unroll a w (roll .w x) = x
+
+    -- Lambek's lemma for indexed inductives
+    unroll' : ∀ a → μ F a ⊢ ⟦ F a ⟧ (μ F)
+    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/LinearFunction.agda b/code/cubical/Grammar/LinearFunction.agda
index 82f8ef9..18e03db 100644
--- a/code/cubical/Grammar/LinearFunction.agda
+++ b/code/cubical/Grammar/LinearFunction.agda
@@ -188,8 +188,13 @@ opaque
   g1 ⊗ g2 ⊗ g3 ⊢ k → ε ⊢ k ⟜ g3 ⟜ g2 ⟜ g1
 ⟜3-intro-ε {k = k} f =
   ⟜-mapCod (⟜-curry {k = k})
-  ∘g ⟜-curry {k = k}
-  ∘g ⟜-intro-ε f
+  ∘g ⟜2-intro-ε f
+
+⟜4-intro-ε :
+  g1 ⊗ g2 ⊗ g3 ⊗ g4 ⊢ k → ε ⊢ k ⟜ g4 ⟜ g3 ⟜ g2 ⟜ g1
+⟜4-intro-ε {k = k} f =
+  ⟜-mapCod (⟜-mapCod (⟜-curry {k = k}))
+  ∘g ⟜3-intro-ε f
 
 ⟜-strength :
   g ⊗ (h ⟜ k) ⊢ (g ⊗ h) ⟜ k
@@ -215,3 +220,9 @@ opaque
 
 ⟜3⊗ : ε ⊢ k ⟜ g3 ⟜ g2 ⟜ g1 → g1 ⊗ g2 ⊗ g3 ⊗ l ⊢ k ⊗ l
 ⟜3⊗ f = ⟜-app-l ∘g ⟜2⊗ f
+
+⟜4⊗ : ε ⊢ k ⟜ g4 ⟜ g3 ⟜ g2 ⟜ g1 → g1 ⊗ g2 ⊗ g3 ⊗ g4 ⊗ l ⊢ k ⊗ l
+⟜4⊗ f = ⟜-app-l ∘g ⟜3⊗ f
+
+⊸0⊗ : ε ⊢ k → l ⊢ l ⊗ k
+⊸0⊗ f = id ,⊗ f ∘g ⊗-unit-r⁻