Stuck on mu-eta strength, started assoc

src/Monad/Instance/Delay.lagda.md

@@ -128,7 +128,6 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
       open Terminal
       alg : F-Coalgebra (Y +-)
       alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
-
       extend' : D₀ X ⇒ D₀ Y
       extend' = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
 
@@ -305,20 +304,24 @@ Next we will show that the delay monad is strong, by giving a natural transforma
         { strengthen = ntHelper (record 
           { η = τ
           ; commute = commute' })
-        ; identityˡ = identityˡ'
+        ; identityˡ = identityˡ' -- triangle
-        ; η-comm = begin 
+        ; η-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 ∎
-        ; μ-η-comm = begin 
+        ; μ-η-comm = μ-η-comm' -- μ-η
-          extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ pullˡ (sym k-assoc) ⟩ 
+        ; strength-assoc = λ {X} {Y} {Z} → begin 
-          extend (extend idC ∘ now ∘ τ _) ∘ τ _ ≈⟨ {!   !} ⟩ 
+          extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin 
+            out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩ 
             {!   !} ≈⟨ {!   !} ⟩ 
-          τ _ ∘ (idC ⁂ extend idC) ∎
+            {!   !} ≈⟨ {!   !} ⟩ 
-        ; strength-assoc = {!   !}
+            {!   !} ≈⟨ {!   !} ⟩ 
+            (idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ {!   !} ∎ })) ⟩ 
+          u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = {!   !} }}) ≈⟨ {!   !} ⟩
+          τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎ -- square
         }
         where
           open import Agda.Builtin.Sigma
@@ -349,18 +352,6 @@ 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ˡ⁻¹ ∎
 
-            τ-helper₂ : out ∘ extend (now ∘ π₂) ∘ τ ≈ out ∘ π₂
-            τ-helper₂ = begin 
-              out ∘ extend (now ∘ π₂) ∘ τ ≈⟨ pullˡ (extendlaw (now ∘ π₂)) ⟩ 
-              ([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
-              ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ ≈⟨ pullʳ τ-law ⟩
-              (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
-              (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ identityʳ refl) ⟩∘⟨refl ⟩
-              (π₂ +₁ extend (now ∘ π₂) ∘ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
-              out ∘ π₂ ∎ 
-
             τ-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 }))
 
@@ -403,7 +394,53 @@ 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) }}) ≈⟨ {!   !} ⟩ 
+            τ _ ∘ (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)
+{- ⁂ ⊤ ○ 
 Diagram for identityˡ':
 https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
 -}