From b6da0a42426ba3616aa33d1144bef839c9b5ff94 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 5 Oct 2023 14:31:12 +0200 Subject: [PATCH] =?UTF-8?q?=E2=9C=A8=20Finished=201=3D>2=20of=20theorem=20?= =?UTF-8?q?35?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Monad/Instance/Delay/Quotienting.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md index e194936..ff4fb81 100644 --- a/src/Monad/Instance/Delay/Quotienting.lagda.md +++ b/src/Monad/Instance/Delay/Quotienting.lagda.md @@ -203,7 +203,7 @@ We will now show that the following conditions are equivalent: cond-4 = {! !} 1⇒2 : cond-1 → cond-2 - 1⇒2 c-1 X = s-alg-on , {! !} + 1⇒2 c-1 X = s-alg-on , (begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎) where open Coequalizer (coeqs X) renaming (universal to coeq-universal) open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)