diff --git a/src/FAlgebra.agda b/src/FAlgebra.agda
index a5b3a83..ff8c519 100644
--- a/src/FAlgebra.agda
+++ b/src/FAlgebra.agda
@@ -5,6 +5,9 @@ module FAlgebra where
 open import GeneralizedPolynomial
   using (Polynomial; ⟦_⟧; ⟦_⟧₀; ⟦_⟧₁; K_; ∅; _,_)
 open import Relation.Binary.PropositionalEquality
+open import Data.Product using (_,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Nat using (suc)
 
 open Polynomial
 open GeneralizedPolynomial.LeastFixpoint
@@ -12,11 +15,16 @@ open GeneralizedPolynomial.LeastFixpoint
 Algebra : Polynomial 1 → Set → Set
 Algebra F A = ⟦ F ⟧₁ A → A
 
--- lemma : (F : Polynomial) → ⟦ F ⟧₁ ⟦ μ F ⟧ₒ ≡ ⟦ F ⟧₁ (∅, μ F)
-
 cata : {F : Polynomial 1} {A : Set} → Algebra F A → ⟦ μ F ⟧₀ → A
-cata {F} ϕ μ⟨ x ⟩ = ϕ (mapCata F F ϕ x)
+cata {F} ϕₒ μ⟨ x ⟩ = ϕₒ (mapCata F F ϕₒ x)
   where
     mapCata : {X : Set} → (F G : Polynomial 1) → Algebra G X → ⟦ F ⟧ (∅ , (μ G)) → ⟦ F ⟧₁ X
-    mapCata {X} F G ϕ x = {!!}
+    mapCata {X} (I 0)       G ϕ μ⟨ x ⟩    = ϕ (mapCata G G ϕ x)
+    mapCata {X} (L ⊕ᵣ R)    G ϕ (inj₁ xₗ) = inj₁ (mapCata L G ϕ xₗ)
+    mapCata {X} (L ⊕ᵣ R)    G ϕ (inj₂ xᵣ) = inj₂ (mapCata R G ϕ xᵣ)
+    mapCata {X} (L ⊗ᵣ R)    G ϕ (xₗ , xᵣ) = mapCata L G ϕ xₗ , mapCata R G ϕ xᵣ
+    mapCata {X} (μ F)       G ϕ μ⟨ x ⟩    = μ⟨ ? ⟩
+    mapCata {X} (ν F)       G ϕ x         = {!!}
+    mapCata {X} (wk_ {0} P) G ϕ x         = x
+    mapCata {X} (wk_ {1} P) G ϕ x         = mapCata P G ϕ x
 
diff --git a/src/GeneralizedPolynomial.agda b/src/GeneralizedPolynomial.agda
index c9b27a8..810b822 100644
--- a/src/GeneralizedPolynomial.agda
+++ b/src/GeneralizedPolynomial.agda
@@ -5,11 +5,11 @@ module GeneralizedPolynomial where
 open import Data.Sum using (_⊎_)
 open import Data.Product using (_×_; ∃-syntax; _,_)
 open import Relation.Binary.PropositionalEquality
-    using (refl; ≢-sym)
+    using (refl; ≢-sym; _≡_)
 open import Data.Nat
   using (ℕ; suc; _<_; _≤_; _⊔_; s≤s; z≤n; _≟_; _≤?_; _<?_)
 open import Data.Nat.Properties
-  using (≤-reflexive; ≤-trans; ≤-step; n≤1+n; ≤∧≢⇒<; ≤-pred)
+  using (≤-reflexive; ≤-trans; ≤-step; n≤1+n; ≤∧≢⇒<; ≤-pred; <⇒≤)
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable
   using (True; toWitness; fromWitness)
@@ -24,22 +24,32 @@ private module ℕExtra where
   m≤n⊔m {0}     {m}     = ≤-reflexive refl
   m≤n⊔m {suc n} {0}     = z≤n
   m≤n⊔m {suc n} {suc m} = s≤s m≤n⊔m
-
-
 open ℕExtra
 
+infixl 6 _⊕ᵣ_
+infixl 7 _⊗ᵣ_
 infixl 6 _⊕_
 infixl 7 _⊗_
 infixr 8 μ_
 infixr 8 ν_
 
 data Polynomial : ℕ → Set₁ where
-    I_  : {n : ℕ} → (m : ℕ) → {True (m <? n)} → Polynomial n
-    K_  : Set → Polynomial 0
-    _⊗_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
-    _⊕_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
-    μ_  : {n : ℕ} → Polynomial (suc n) → Polynomial n
-    ν_  : {n : ℕ} → Polynomial (suc n) → Polynomial n
+    I_   : {n : ℕ} → (m : ℕ) → {True (m <? n)} → Polynomial n
+    K_   : Set → Polynomial 0
+    μ_   : {n : ℕ} → Polynomial (suc n) → Polynomial n
+    ν_   : {n : ℕ} → Polynomial (suc n) → Polynomial n
+
+    -- Shouldn't be used explicitly by users of the lib
+    _⊕ᵣ_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
+    _⊗ᵣ_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
+    wk_  : {n m : ℕ} → Polynomial n → {True (n ≤? m)} → Polynomial m
+
+-- Versions that infer weakening
+_⊗_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
+L ⊗ R = (wk_ L {fromWitness n≤n⊔m}) ⊗ᵣ (wk_ R {fromWitness m≤n⊔m})
+
+_⊕_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
+L ⊕ R = (wk_ L {fromWitness n≤n⊔m}) ⊕ᵣ (wk_ R {fromWitness m≤n⊔m})
 
 data Context : ℕ → Set₁ where
   ∅      : Context 0
@@ -59,24 +69,33 @@ lookup (ctx , _) (suc m) {s≤s p} with lookup ctx m {p}
 -- A = I 0 ⊕ I 1
 -- B = I 0
 -- A ⊗ B
-weaken : ∀ {n m : ℕ} → (m ≤ n) → Context n → Context m
-weaken {0}     {0} z≤z ∅ = ∅
-weaken {suc n} {m} m≤n ctx@(rest , _) with suc n ≟ m
+weaken-context : ∀ {n m : ℕ} → (m ≤ n) → Context n → Context m
+weaken-context {0}     {0} z≤z ∅ = ∅
+weaken-context {suc n} {m} m≤n ctx@(rest , _) with suc n ≟ m
 ... | yes refl = ctx
-... | no  n≢m  = weaken (≤-pred (≤∧≢⇒< m≤n (≢-sym n≢m))) rest
+... | no  n≢m  = weaken-context (≤-pred (≤∧≢⇒< m≤n (≢-sym n≢m))) rest
 
 open import Data.Nat.Induction
 
 mutual
-  {-# TERMINATING #-}
+  eval-impl : _
+  eval-impl 0       rec (K x)           ctx = x
+  eval-impl (suc n) rec (I_ m {m<n})    ctx with lookup ctx m {toWitness m<n}
+  ... | p , X , p<n                         = rec p p<n X
+                                                  (weaken-context (≤-trans (≤-pred p<n)
+                                                                  (n≤1+n _)) ctx)
+  eval-impl n rec (wk_ {f} {m} P {f≤m}) ctx with f ≟ m
+  ... | yes refl                            = eval-impl _ rec P ctx
+  ... | no  f≢m                             = rec f (≤∧≢⇒< (toWitness f≤m) f≢m) P
+                                                           (weaken-context (toWitness f≤m) ctx)
+  eval-impl n rec (μ P)                 ctx = LeastFixpoint P ctx
+  eval-impl n rec (ν P)                 ctx = GreatestFixpoint P ctx
+  eval-impl n rec (L ⊕ᵣ R)              ctx = eval-impl _ rec L ctx ⊎ eval-impl _ rec R ctx
+  eval-impl n rec (L ⊗ᵣ R)              ctx = eval-impl _ rec L ctx × eval-impl _ rec R ctx
+
+
   eval : {n : ℕ} → Polynomial n → Context n → Set
-  eval ((I m) {m<n}) ctx with lookup ctx m {toWitness m<n}
-  ... | p , X , s≤s p<n  = eval X (weaken (≤-trans p<n (n≤1+n _)) ctx)
-  eval (K x)         ctx = x
-  eval (L ⊗ R)       ctx = eval L (weaken n≤n⊔m ctx) × eval R (weaken m≤n⊔m ctx)
-  eval (L ⊕ R)       ctx = eval L (weaken n≤n⊔m ctx) ⊎ eval R (weaken m≤n⊔m ctx)
-  eval (μ P)         ctx = LeastFixpoint P ctx
-  eval (ν P)         ctx = GreatestFixpoint P ctx
+  eval {n} = <-rec _ eval-impl n
 
   data LeastFixpoint {n : ℕ} (P : Polynomial (suc n)) (ctx : Context n) : Set where
     μ⟨_⟩ : eval P (_,_ ctx {fromWitness (≤-reflexive refl)} (μ P)) → LeastFixpoint P ctx
@@ -85,11 +104,13 @@ mutual
     coinductive
     field rest : eval P (_,_ ctx {fromWitness (≤-reflexive refl)} (ν P))
 
-⟦_⟧ : ∀ {n m : ℕ} → {n≤m : True (n ≤? m)} → Polynomial n → Context m → Set
-⟦_⟧ {_} {_} {n≤m} F ctx = eval F (weaken (toWitness n≤m) ctx)
+
+⟦_⟧ : {n m : ℕ} → {n≤m : True (n ≤? m)} → Polynomial n → Context m → Set
+⟦_⟧ {_} {_} {n≤m} F ctx = eval F (weaken-context (toWitness n≤m) ctx)
 
 ⟦_⟧₁ : Polynomial 1 → Set → Set
 ⟦ P ⟧₁ X = ⟦ P ⟧ (∅ , K X)
 
 ⟦_⟧₀ : Polynomial 0 → Set
 ⟦ P ⟧₀ = ⟦ P ⟧ ∅
+