diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index 2e75792..c1f26ce 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -83,4 +83,23 @@ module Category.Instance.AmbientCategory where open MR C open HomReasoning open Equiv + + iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso) + iso-epi-from iso = λ f g eq → begin + f ≈⟨ introʳ (_≅_.isoʳ iso) ⟩ + (f ∘ M'._≅_.from iso ∘ M'._≅_.to iso) ≈⟨ pullˡ eq ⟩ + ((g ∘ M'._≅_.from iso) ∘ M'._≅_.to iso) ≈⟨ cancelʳ (_≅_.isoʳ iso) ⟩ + g ∎ + where + open HomReasoning + open MR C + iso-epi-to : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.to iso) + iso-epi-to iso = λ f g eq → begin + f ≈⟨ introʳ (_≅_.isoˡ iso) ⟩ + (f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩ + ((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩ + g ∎ + where + open HomReasoning + open MR C ``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 2c2cf78..6019898 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -22,6 +22,8 @@ module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where open Ambient ambient ``` +-- TODO SERGEYS LÖSUNG: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ== + ## Definition The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523) @@ -72,7 +74,6 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver unitlaw : out ∘ now ≈ i₁ unitlaw = cancelˡ (_≅_.isoʳ out-≅) - ``` Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`: @@ -100,7 +101,6 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y ι : X × N ⇒ DX ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }}) - ``` ## Delay is a monad @@ -294,7 +294,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma open import Categories.Category.Monoidal.Core open Monoidal monoidal open import Categories.Monad.Relative using () renaming (Monad to RMonad) - open RMonad kleisli using (extend) renaming (assoc to k-assoc) + open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ) open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_) open Monad monad using () renaming (η to η'; μ to μ') module η = NaturalTransformation η' @@ -306,12 +306,12 @@ Next we will show that the delay monad is strong, by giving a natural transforma ; 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ʳ dstr-law₁) ⟩ - out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ - out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - now ∎ + τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ + τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩ + (out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩ + out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ + out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ + now ∎ ; μ-η-comm = μ-η-comm' -- μ-τ ; strength-assoc = strength-assoc' -- square } @@ -346,6 +346,15 @@ Next we will show that the delay monad is strong, by giving a natural transforma out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎ + τ-now : τ ∘ (idC ⁂ now) ≈ now + τ-now = begin + τ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ (⁂-cong₂ identity² refl)) ⟩ + τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ τ-helper ⟩ + (out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩ + out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩ + out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ + now ∎ + τ-unique : (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (idC +₁ t) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) → t ≈ τ τ-unique t t-commutes = sym (!-unique (record { f = t ; commutes = t-commutes })) @@ -388,52 +397,70 @@ Next we will show that the delay monad is strong, by giving a natural transforma π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩ [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩ (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎) + μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC) μ-η-comm' {X} {Y} = begin extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin - out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw idC) ⟩ - ([ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ τ (X , Y)))) ⟩ - [ out ∘ idC , i₂ ∘ extend idC ] ∘ ([ out ∘ now ∘ τ _ , i₂ ∘ extend (now ∘ τ _) ] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law _)) ⟩ - [ out ∘ idC , i₂ ∘ extend idC ] ∘ [ out ∘ now ∘ τ _ , i₂ ∘ extend (now ∘ τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (sym []∘+₁) ⟩∘⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩ - ([ out , i₂ ] ∘ (idC +₁ extend idC)) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - -- TODO only works if (now +₁ now) ∘ out ≈ out ∘ now - {! !} ≈⟨ {! !} ⟩ - [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (now +₁ idC) ∘ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (now +₁ idC)) ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - [ out ∘ (τ _ ∘ (idC ⁂ now)) , i₂ ] ∘ (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - [ out ∘ now , i₂ ] ∘ (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {! !} ⟩ - (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ∎ })) ⟩ - u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) }}) ≈⟨ {! !} ⟩ + out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩ + out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩ + [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩ + ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩ + (idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩ + (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩ + u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin + out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩ + ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩ + ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩ + (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ τ _ ∘ (idC ⁂ extend idC) ∎ where - β : ∀ {A} → D₀ A + D₀ (D₀ A) ⇒ A + D₀ (D₀ A) - β {A} = [ ((idC +₁ now) ∘ out) , i₂ ] - β⁻¹ : ∀ {A} → A + D₀ (D₀ A) ⇒ D₀ A + D₀ (D₀ A) - β⁻¹ {A} = [ (i₁ ∘ now) , i₂ ] - β∘β⁻¹ : ∀ {A} → β {A} ∘ β⁻¹ ≈ idC - β∘β⁻¹ = begin - [ ((idC +₁ now) ∘ out) , i₂ ] ∘ [ (i₁ ∘ now) , i₂ ] ≈⟨ ∘[] ⟩ - [ [ ((idC +₁ now) ∘ out) , i₂ ] ∘ (i₁ ∘ now) , [ ((idC +₁ now) ∘ out) , i₂ ] ∘ i₂ ] ≈⟨ []-cong₂ (pullˡ inject₁) inject₂ ⟩ - [ ((idC +₁ now) ∘ out) ∘ now , i₂ ] ≈⟨ []-cong₂ (pullʳ unitlaw) refl ⟩ - [ (idC +₁ now) ∘ i₁ , i₂ ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) refl ⟩ - [ i₁ , i₂ ] ≈⟨ +-η ⟩ - idC ∎ - -- diag₁ : ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈ out ∘ τ _ - -- diag₁ = begin - -- ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {! !} ⟩ - -- (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {! !} ⟩ - -- (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ((idC ⁂ (now +₁ idC))) ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {! !} ⟩ - -- (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ] ∘ out) ≈⟨ {! !} ⟩ - -- (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {! !} ⟩ - -- (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ out ∘ now , i₂ ] ∘ out) ≈⟨ {! !} ⟩ - -- (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ out) ≈⟨ sym (τ-law (X , A (Terminal.⊤ (coalgebras Y)))) ⟩ - -- out ∘ τ _ ∎ - diag₂ = τ-law - diag₃ = out-law {Y = D₀ (X × Y)} (extend idC) + square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) + square = begin + out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ + ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩ + [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ + tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ + tri = begin + [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ + [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ + [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ + [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ + (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎ + id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _) + id*∘Dτ = begin + extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ + extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ + extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩ + extend (τ _) ∎ + tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ + tri₂' = begin + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₁) , (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⁂-cong₂ identity² inject₁) (⁂-cong₂ identity² inject₂) ⟩ + (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩ + (idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩ + [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩ + [ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩ + [ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩ + [ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩ + (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩ + (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎ + tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ + tri₂ = iso-epi-from + (record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ }) + ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ])) + ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) + (assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl) + strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ strength-assoc' {X} {Y} {Z} = begin extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin @@ -487,11 +514,10 @@ Next we will show that the delay monad is strong, by giving a natural transforma (distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩ distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎) -{- ⁂ ⊤ ○ -Diagram for identityˡ': -https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ== --} --- ⊤ +-- {- ⁂ ⊤ ○ +-- Diagram for identityˡ': +-- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ== +-- -} commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) → τ P₂ ∘ ((fst fg) ⁂ extend (now ∘ (snd fg))) ≈ extend (now ∘ ((fst fg) ⁂ (snd fg))) ∘ τ P₁ commute' {(U , V)} {(W , X)} (f , g) = begin @@ -521,7 +547,7 @@ https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgK open Terminal (coalgebras (W × X)) alg' : F-Coalgebra ((W × X) +-) alg' = record { A = U × D₀ V ; α = ((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) } --- ⁂ ○ ˡ ʳ + strongMonad : StrongMonad monoidal strongMonad = record { M = monad ; strength = strength } ```