diff --git a/src/Category/Construction/PreElgotMonads.lagda.md b/src/Category/Construction/PreElgotMonads.lagda.md
index 06e380b..008bc74 100644
--- a/src/Category/Construction/PreElgotMonads.lagda.md
+++ b/src/Category/Construction/PreElgotMonads.lagda.md
@@ -41,20 +41,20 @@ module _ (P S : PreElgotMonad) where
       α-μ : ∀ {X}
         → α.η X ∘ TP.μ.η X ≈ TS.μ.η X ∘ TS.F.₁ (α.η X) ∘ α.η (TP.F.₀ X)
 
-PreElgotMonads : Category {!!} {!!} {!!}
+PreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
 PreElgotMonads = record
                    { Obj = PreElgotMonad
                    ; _⇒_ = PreElgotMonad-Morphism
                    ; _≈_ = λ f g → (PreElgotMonad-Morphism.α f) ≃ (PreElgotMonad-Morphism.α g)
                    ; id = id'
-                   ; _∘_ = {!!}
-                   ; assoc = {!!}
-                   ; sym-assoc = {!!}
-                   ; identityˡ = {!!}
-                   ; identityʳ = {!!}
-                   ; identity² = {!!}
-                   ; equiv = {!!}
-                   ; ∘-resp-≈ = {!!}
+                   ; _∘_ = _∘'_
+                   ; assoc = assoc
+                   ; sym-assoc = sym-assoc
+                   ; identityˡ = identityˡ
+                   ; identityʳ = identityʳ
+                   ; identity² = identity²
+                   ; equiv = λ {A} {B} → record { refl = refl ; sym = λ f → sym f ; trans = λ f g → trans f g }
+                   ; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
                    }
                    where
                      id' : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism A A
@@ -76,21 +76,24 @@ PreElgotMonads = record
                      _∘'_ {X} {Y} {Z} f g = record
                         { α = αf ∘ᵥ αg
                         ; α-η = λ {A} → begin
-                          (αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ {!!} ⟩
-                          {!!} ≈⟨ {!!} ⟩
-                          {!!} ≈⟨ {!!} ⟩
-                          {!!} ≈⟨ {!!} ⟩
-                          {!!} ≈⟨ {!!} ⟩
-                          {!!} ≈⟨ {!!} ⟩
+                          (αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ pullʳ (α-η g) ⟩
+                          αf.η A ∘ TY.η.η A ≈⟨ α-η f ⟩
                           TZ.η.η A ∎
-                        ; α-μ = {!!}
+                        ; α-μ = λ {A} → begin
+                           (αf.η A ∘ αg.η A) ∘ TX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩
+                          αf.η A ∘ TY.μ.η A ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩
+                          (TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ αf.η (TY.F.₀ A)) ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
+                          TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ (TZ.F.₁ (αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism TZ.F))) ⟩
+                          TZ.μ.η A ∘ (TZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩
+                          TZ.μ.η A ∘ TZ.F.₁ ((αf.η A ∘ αg.η A)) ∘  αf.η (TX.F.₀ A) ∘ αg.η (TX.F.₀ A) ∎
                         }
                         where
                           module TX = Monad (PreElgotMonad.T X)
                           module TY = Monad (PreElgotMonad.T Y)
                           module TZ = Monad (PreElgotMonad.T Z)
 
+                          open PreElgotMonad-Morphism using (α-η; α-μ)
+
                           open PreElgotMonad-Morphism f using () renaming (α to αf)
                           open PreElgotMonad-Morphism g using () renaming (α to αg)
-
 ```