From 6725f5ccbfacac7d96df8e4b304477dabe1c4797 Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Tue, 25 Jun 2024 13:52:32 +0000 Subject: [PATCH] clean up comonad morphism --- src/Categories/Comonad/Morphism.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Categories/Comonad/Morphism.agda b/src/Categories/Comonad/Morphism.agda index a6291599..dc970524 100644 --- a/src/Categories/Comonad/Morphism.agda +++ b/src/Categories/Comonad/Morphism.agda @@ -112,8 +112,7 @@ module _ {S R T : Comonad C} where R.δ.η U ∘ σ .α.η U ∘ τ .α.η U ≈⟨ pullˡ (σ .comult-comp) ⟩ (σ .α.η (R.F.₀ U) ∘ T.F.₁ (σ .α.η U) ∘ T.δ.η U) ∘ τ .α.η U - -- there is no approx² that witnesses (a ∘ (b ∘ c)) ∘ d ≈ (a ∘ b) ∘ (c ∘ d) - ≈⟨ pushˡ C.sym-assoc ⟩ + ≈⟨ assoc²βγ ⟩ (σ .α.η (R.F.₀ U) ∘ T.F.₁ (σ .α.η U)) ∘ (T.δ.η U ∘ τ .α.η U) ≈⟨ refl⟩∘⟨ τ .comult-comp ⟩ (σ .α.η (R.F.₀ U) ∘ T.F.₁ (σ .α.η U)) ∘ (τ .α.η (T.F.₀ U) ∘ S.F.₁ (τ .α.η U) ∘ S.δ.η U)