minor

agda/src/Monad/Instance/Delay.lagda.md

@@ -289,7 +289,7 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
       ; unit = now
       ; extend = extend'
       ; identityʳ = identityʳ'
-      ; identityˡ = identityˡ'
+      ; identityˡ = extend'-unique now idC (id-comm ○ (sym ([]-unique (identityˡ ○ sym unitlaw) id-comm-sym)) ⟩∘⟨refl)
       ; assoc = assoc'
       ; sym-assoc = sym assoc'
       ; extend-≈ = extend-≈'
@@ -328,20 +328,6 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
           out⁻¹ ∘ out ∘ f                                       ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
           f                                                     ∎
 
-        identityˡ' : ∀ {X} → extend' now ≈ idC
-        identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend' now ; commutes = begin 
-          out ∘ extend' now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩ 
-          ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁     ≈⟨ pullʳ inject₁ ⟩
-          (idC +₁ (u (! (coalgebras X) {A = alg now}))) 
-          ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out                   ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
-          (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
-          [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ 
-          , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out      ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
-          [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out  ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
-          [ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out                                ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
-          ([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out                             ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
-          (idC +₁ extend' now) ∘ out                                             ∎ })
-
         assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend' (extend' h ∘ g) ≈ extend' h ∘ extend' g
         assoc' {X} {Y} {Z} {g} {h} = extend'-unique (extend' h ∘ g) (extend' h ∘ extend' g) (begin 
           out ∘ extend' h ∘ extend' g                                       ≈⟨ pullˡ (extendlaw h) ⟩

agda/src/Monad/Instance/Delay/Strong.lagda.md

@@ -88,13 +88,7 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
         { η = τ
         ; commute = commute' })
       ; identityˡ = identityˡ' -- triangle
-      ; η-comm = begin -- η-τ
-          τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ 
-          τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ 
-          (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ distributeˡ⁻¹-i₁) ⟩ 
-          out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ 
-          out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          now ∎
+      ; η-comm = λ {A} {B} → τ-now (A , B)
       ; μ-η-comm = μ-η-comm' -- μ-τ
       ; strength-assoc = strength-assoc' -- square
       }