open import Level
open import Categories.Category.Core
open import Categories.Functor.Coalgebra
open import Categories.Monad.Commutative
open import Monad.Instance.Delay
open import Categories.Category.Distributive
open import Monad.Helper
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
module Monad.Instance.Delay.Commutative {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (D : DelayM (Distributive.cocartesian distributive)) where
open Category C
open import Category.Distributive.Helper distributive
open Bundles
open HomReasoning
open Equiv
open MR C
open MP C
open M C
open DelayM D
open D-Kleisli
open D-Monad
open Later∘Extend
open import Monad.Instance.Delay.Strong distributive D public
open D-Strong
open import Monad.Instance.Delay.Guarded cocartesian D
module σ-mod where
open τ-mod
σ : ∀ {X Y} → D₀ X × Y ⇒ D₀ (X × Y)
σ = D₁ swap ∘ τ ∘ swap
abstract
σ-law : ∀ {X} {Y} → out ∘ σ {X} {Y} ≈ (id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)
σ-law = begin
out ∘ σ ≈⟨ pullˡ (D₁-commutes swap) ⟩
((swap +₁ D₁ swap) ∘ out) ∘ τ ∘ swap ≈⟨ pullˡ (pullʳ τ-commutes) ⟩
((swap +₁ D₁ swap) ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ swap ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘×₁))) ⟩
(swap +₁ D₁ swap) ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ swap ∘ (out ×₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩
(swap +₁ D₁ swap) ∘ (id +₁ τ) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (out ×₁ id) ≈⟨ pullˡ +₁∘+₁ ⟩
(swap ∘ id +₁ D₁ swap ∘ τ) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (out ×₁ id) ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩
(((swap ∘ id) ∘ swap +₁ (D₁ swap ∘ τ) ∘ swap) ∘ distributeʳ⁻¹) ∘ (out ×₁ id) ≈⟨ ((+₁-cong₂ (identityʳ ⟩∘⟨refl ○ swap∘swap) assoc) ⟩∘⟨refl) ⟩∘⟨refl ⟩
((id +₁ D₁ swap ∘ τ ∘ swap) ∘ distributeʳ⁻¹) ∘ (out ×₁ id) ≈⟨ assoc ⟩
(id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ∎
σ-helper : ∀ {X Y} → (σ {X} {Y}) ∘ (out⁻¹ ×₁ id) ≈ out⁻¹ ∘ (id +₁ σ) ∘ distributeʳ⁻¹
σ-helper = begin
σ ∘ (out⁻¹ ×₁ id) ≈⟨ introˡ out⁻¹∘out ⟩
(out⁻¹ ∘ out) ∘ σ ∘ (out⁻¹ ×₁ id) ≈⟨ pullʳ (pullˡ σ-law) ⟩
out⁻¹ ∘ ((id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ (out⁻¹ ×₁ id) ≈⟨ refl⟩∘⟨ (pullʳ (cancelʳ (×₁∘×₁ ○ ×₁-cong₂ out∘out⁻¹ identity² ○ ⟨⟩-unique id-comm id-comm))) ⟩
out⁻¹ ∘ (id +₁ σ) ∘ distributeʳ⁻¹ ∎
σ-now : ∀ {X} {Y} → σ {X} {Y} ∘ (now ×₁ id) ≈ now
σ-now = begin
(D₁ swap ∘ τ ∘ swap) ∘ (now ×₁ id) ≈⟨ pullʳ (pullʳ swap∘×₁) ⟩
D₁ swap ∘ τ ∘ (id ×₁ now) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ τ-now ⟩
D₁ swap ∘ now ∘ swap ≈⟨ extendʳ (sym (D.η.commute swap)) ⟩
now ∘ swap ∘ swap ≈⟨ elimʳ swap∘swap ⟩
now ∎
later∘σ : ∀ {X} {Y} → σ {X} {Y} ∘ (later ×₁ id) ≈ later ∘ σ
later∘σ = begin
(D₁ swap ∘ τ ∘ swap) ∘ (later ×₁ id) ≈⟨ pullʳ (pullʳ swap∘×₁) ⟩
D₁ swap ∘ τ ∘ (id ×₁ later) ∘ swap ≈⟨ refl⟩∘⟨ (extendʳ τ-later) ⟩
D₁ swap ∘ later ∘ τ ∘ swap ≈⟨ extendʳ (sym (later-extend-comm (now ∘ swap))) ⟩
later ∘ D₁ swap ∘ τ ∘ swap ∎
σ-unique : ∀ {X Y} → (s : D₀ X × Y ⇒ D₀ (X × Y)) → (out ∘ s ≈ (id +₁ s) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)) → s ≈ σ
σ-unique s s-commutes = begin
s ≈˘⟨ elimʳ swap∘swap ⟩
s ∘ swap ∘ swap ≈˘⟨ cancelˡ ((sym D.F.homomorphism) ○ D.F.F-resp-≈ swap∘swap ○ D.F.identity) ⟩
D₁ swap ∘ D₁ swap ∘ s ∘ swap ∘ swap ≈⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ sym (τ-unique (D₁ swap ∘ s ∘ swap) helper))) ⟩
D₁ swap ∘ τ ∘ swap ∎
where
helper : out ∘ D₁ swap ∘ s ∘ swap ≈ (id +₁ D₁ swap ∘ s ∘ swap) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
helper = begin
out ∘ D₁ swap ∘ s ∘ swap ≈⟨ extendʳ (D₁-commutes swap) ⟩
(swap +₁ D₁ swap) ∘ out ∘ s ∘ swap ≈⟨ refl⟩∘⟨ (extendʳ s-commutes) ⟩
(swap +₁ D₁ swap) ∘ (id +₁ s) ∘ (distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ swap ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ⟩
(swap +₁ D₁ swap ∘ s) ∘ (distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ swap ≈⟨ refl⟩∘⟨ (pullʳ (sym swap∘×₁)) ⟩
(swap +₁ D₁ swap ∘ s) ∘ distributeʳ⁻¹ ∘ swap ∘ (id ×₁ out) ≈⟨ refl⟩∘⟨ (extendʳ distributeʳ⁻¹∘swap) ⟩
(swap +₁ D₁ swap ∘ s) ∘ (swap +₁ swap) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ swap∘swap assoc) ⟩
(id +₁ D₁ swap ∘ s ∘ swap) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎
σ-natural : ∀ {U V W X : Obj} (f : U ⇒ V) (g : W ⇒ X) → σ ∘ (extend (now ∘ f) ×₁ g) ≈ extend (now ∘ (f ×₁ g)) ∘ σ
σ-natural f g = begin
σ ∘ (D₁ f ×₁ g) ≈⟨ pullʳ (pullʳ swap∘×₁) ⟩
D₁ swap ∘ τ ∘ (g ×₁ extend (now ∘ f)) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (τ-natural g f)) ⟩
D₁ swap ∘ (D₁ (g ×₁ f) ∘ τ) ∘ swap ≈⟨ pullˡ (pullˡ (sym D.F.homomorphism)) ⟩
(D₁ (swap ∘ (g ×₁ f)) ∘ τ) ∘ swap ≈⟨ ((D.F.F-resp-≈ swap∘×₁) ⟩∘⟨refl) ⟩∘⟨refl ⟩
(D₁ ((f ×₁ g) ∘ swap) ∘ τ) ∘ swap ≈⟨ pushˡ D.F.homomorphism ⟩∘⟨refl ⟩
(D₁ (f ×₁ g) ∘ D₁ swap ∘ τ) ∘ swap ≈⟨ assoc²βε ⟩
D₁ (f ×₁ g) ∘ σ ∎
open τ-mod
open σ-mod
στ-comm : ∀ {X} {Y} → extend σ ∘ τ {D₀ X} {Y} ≈ out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out)
στ-comm = out-mono (extend σ ∘ τ) (out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out)) (begin
out ∘ extend σ ∘ τ ≈⟨ pullˡ (extend-commutes σ) ⟩
([ out ∘ σ , i₂ ∘ extend σ ] ∘ out) ∘ τ ≈⟨ pullʳ τ-commutes ⟩
[ out ∘ σ , i₂ ∘ extend σ ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ pullˡ []∘+₁ ⟩
[ (out ∘ σ) ∘ id , (i₂ ∘ extend σ) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ ([]-cong₂ (identityʳ ○ σ-law) assoc) ⟩∘⟨refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ (sym out⁻¹∘out) refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ∘ out ×₁ out) ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ×₁ (id +₁ id)) ∘ (out ×₁ out) ≈⟨ refl⟩∘⟨ pullˡ (sym (distributeˡ⁻¹-natural out⁻¹ id id)) ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) , i₂ ∘ extend σ ∘ τ ] ∘ (((out⁻¹ ×₁ id) +₁ (out⁻¹ ×₁ id)) ∘ distributeˡ⁻¹) ∘ (out ×₁ out) ≈⟨ pullˡ (pullˡ []∘+₁) ⟩
([ ((id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id)) ∘ (out⁻¹ ×₁ id) , (i₂ ∘ extend σ ∘ τ) ∘ (out⁻¹ ×₁ id) ] ∘ distributeˡ⁻¹) ∘ (out ×₁ out) ≈⟨ assoc ○ ([]-cong₂ (pullʳ (cancelʳ (×₁∘×₁ ○ ×₁-cong₂ out∘out⁻¹ identity² ○ ⟨⟩-unique id-comm id-comm))) (refl⟩∘⟨ (×₁-cong₂ refl (sym D.F.identity)) ○ (pullʳ (pullʳ (τ-natural out⁻¹ id))))) ⟩∘⟨refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend σ ∘ D₁ (out⁻¹ ×₁ id) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ (pullˡ (sym DK.assoc)) ○ refl⟩∘⟨ ((extend-≈ (pullˡ DK.identityʳ)) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend (σ ∘ (out⁻¹ ×₁ id)) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ((extend-≈ σ-helper) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend (out⁻¹ ∘ (id +₁ σ) ∘ distributeʳ⁻¹) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈˘⟨ ([]-cong₂ refl (refl⟩∘⟨ ((sym DK.assoc ○ extend-≈ (pullˡ DK.identityʳ) ○ extend-≈ assoc) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ (extend (out⁻¹ ∘ (id +₁ σ)) ∘ D₁ distributeʳ⁻¹) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ pullʳ helper₁)) ⟩∘⟨refl ⟩
[ (id +₁ σ) ∘ distributeʳ⁻¹ , i₂ ∘ extend (out⁻¹ ∘ (id +₁ σ)) ∘ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ refl assoc²βε) ⟩
[ (id +₁ σ) , i₂ ∘ extend (out⁻¹ ∘ (id +₁ σ)) ∘ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ∘[])) ⟩∘⟨refl ⟩
[ (id +₁ σ) , i₂ ∘ [ extend (out⁻¹ ∘ (id +₁ σ)) ∘ D₁ i₁ ∘ τ , extend (out⁻¹ ∘ (id +₁ σ)) ∘ D₁ i₂ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (pullˡ ((sym DK.assoc) ○ extend-≈ (pullˡ DK.identityʳ))) (pullˡ ((sym DK.assoc) ○ extend-≈ (pullˡ DK.identityʳ)))))) ⟩∘⟨refl ⟩
[ (id +₁ σ) , i₂ ∘ [ extend ((out⁻¹ ∘ (id +₁ σ)) ∘ i₁) ∘ τ , extend ((out⁻¹ ∘ (id +₁ σ)) ∘ i₂) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ ((extend-≈ (pullʳ +₁∘i₁)) ⟩∘⟨refl) ((extend-≈ (pullʳ +₁∘i₂)) ⟩∘⟨refl)))) ⟩∘⟨refl ⟩
[ (id +₁ σ) , i₂ ∘ [ extend (out⁻¹ ∘ i₁ ∘ id) ∘ τ , extend (out⁻¹ ∘ i₂ ∘ σ) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (elimˡ ((extend-≈ (refl⟩∘⟨ identityʳ)) ○ DK.identityˡ)) ((extend-≈ sym-assoc) ⟩∘⟨refl)))) ⟩∘⟨refl ⟩
[ (id +₁ σ) , i₂ ∘ [ τ , extend (later ∘ σ) ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl ((sym (later∘extend σ)) ⟩∘⟨refl ○ assoc)))) ⟩∘⟨refl ⟩
[ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈˘⟨ cancelˡ out∘out⁻¹ ⟩
out ∘ out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ∎)
where
helper₁ : (D₁ distributeʳ⁻¹) ∘ τ ≈ [ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹
helper₁ = Iso⇒Epi (IsIso.iso isIsoʳ) ((D₁ distributeʳ⁻¹) ∘ τ) ([ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹) (begin
((D₁ distributeʳ⁻¹) ∘ τ) ∘ distributeʳ ≈⟨ ∘[] ○ []-cong₂ (refl⟩∘⟨ (×₁-cong₂ refl (sym D.F.identity))) (refl⟩∘⟨ (×₁-cong₂ refl (sym D.F.identity))) ⟩
[ ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₁ ×₁ D₁ id) , ((D₁ distributeʳ⁻¹) ∘ τ) ∘ (i₂ ×₁ D₁ id) ] ≈⟨ []-cong₂ (pullʳ (τ-natural i₁ id)) (pullʳ (τ-natural i₂ id)) ⟩
[ (D₁ distributeʳ⁻¹) ∘ D₁ (i₁ ×₁ id) ∘ τ , (D₁ distributeʳ⁻¹) ∘ D₁ (i₂ ×₁ id) ∘ τ ] ≈⟨ []-cong₂ (pullˡ (sym D.F.homomorphism)) (pullˡ (sym D.F.homomorphism)) ⟩
[ D₁ (distributeʳ⁻¹ ∘ (i₁ ×₁ id)) ∘ τ , D₁ (distributeʳ⁻¹ ∘ (i₂ ×₁ id)) ∘ τ ] ≈⟨ []-cong₂ (D.F.F-resp-≈ distributeʳ⁻¹-i₁ ⟩∘⟨refl) ((D.F.F-resp-≈ distributeʳ⁻¹-i₂) ⟩∘⟨refl) ⟩
[ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩
([ D₁ i₁ ∘ τ , D₁ i₂ ∘ τ ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
commutativeMonad : Commutative braided strongMonad
commutativeMonad = record { commutes = begin
(extend id ∘ D₁ σ) ∘ τ ≈⟨ (Kleisli⇒Monad⇒Kleisli kleisli _) ⟩∘⟨refl ⟩
extend σ ∘ τ ≈⟨ commutes' ⟩
extend τ ∘ σ ≈˘⟨ (Kleisli⇒Monad⇒Kleisli kleisli _) ⟩∘⟨refl ⟩
(extend id ∘ D₁ τ) ∘ σ ∎ }
where
commutes' : ∀ {X Y} → extend σ ∘ τ ≈ extend τ ∘ σ
commutes' {X} {Y} = guarded-unique g (extend σ ∘ τ) (extend τ ∘ σ) guarded (fixpoint-eq στ-comm) (fixpoint-eq fixpoint₂)
where
w = (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ×₁ out)
g = out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w
guarded : IsGuarded g
guarded = record
{ guard = [ id +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w
; guard-eq = begin
(i₁ +₁ id) ∘ [ id +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈⟨ pullˡ (∘[] ○ []-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) (pullˡ (+₁∘i₂ ○ identityʳ))) ⟩
[ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ cancelˡ out∘out⁻¹ ⟩
out ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ∎
}
fixpoint₂ : extend τ ∘ σ ≈ out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ w
fixpoint₂ = out-mono (extend τ ∘ σ) (out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ w) (begin
out ∘ extend τ ∘ σ ≈⟨ pullˡ (extend-commutes τ) ⟩
([ out ∘ τ , i₂ ∘ extend τ ] ∘ out) ∘ σ ≈⟨ pullʳ σ-law ⟩
[ out ∘ τ , i₂ ∘ extend τ ] ∘ (id +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ (identityʳ ○ τ-commutes) assoc) ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ extend τ ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ id) ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) out⁻¹∘out)) ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ extend τ ∘ σ ] ∘ distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ out⁻¹) ∘ (out ×₁ out) ≈⟨ refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural out⁻¹ id id))) ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ extend τ ∘ σ ] ∘ (((id ×₁ out⁻¹) +₁ (id ×₁ out⁻¹)) ∘ distributeʳ⁻¹) ∘ (out ×₁ out) ≈⟨ pullˡ (pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (cancelʳ (×₁∘×₁ ○ ×₁-cong₂ identity² out∘out⁻¹ ○ ⟨⟩-unique id-comm id-comm))) (refl⟩∘⟨ (×₁-cong₂ (sym D.F.identity) refl)))) ○ assoc ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ , (i₂ ∘ extend τ ∘ σ) ∘ (D₁ id ×₁ out⁻¹) ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (pullʳ (pullʳ (σ-natural id out⁻¹)))) ⟩∘⟨refl ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend τ ∘ D₁ (id ×₁ out⁻¹) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ (pullˡ ((sym DK.assoc) ○ extend-≈ (pullˡ DK.identityʳ))))) ⟩∘⟨refl ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend (τ ∘ (id ×₁ out⁻¹)) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ((extend-≈ τ-out⁻¹) ⟩∘⟨refl))) ⟩∘⟨refl ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend (out⁻¹ ∘ (id +₁ τ) ∘ distributeˡ⁻¹) ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈˘⟨ ([]-cong₂ refl (refl⟩∘⟨ pullˡ ((sym DK.assoc) ○ (extend-≈ (pullˡ DK.identityʳ) ○ extend-≈ assoc)))) ⟩∘⟨refl ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ , i₂ ∘ extend (out⁻¹ ∘ (id +₁ τ)) ∘ D₁ distributeˡ⁻¹ ∘ σ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl ((refl⟩∘⟨ (refl⟩∘⟨ helper₂)) ○ sym assoc²βε)) ⟩∘⟨refl ⟩
[ (id +₁ τ) ∘ distributeˡ⁻¹ , (i₂ ∘ extend (out⁻¹ ∘ (id +₁ τ)) ∘ [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ]) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
([ (id +₁ τ) , i₂ ∘ extend (out⁻¹ ∘ (id +₁ τ)) ∘ [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹)) ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ assoc ○ ([]-cong₂ refl (refl⟩∘⟨ ∘[])) ⟩∘⟨refl ⟩
[ (id +₁ τ) , i₂ ∘ [ extend (out⁻¹ ∘ (id +₁ τ)) ∘ D₁ i₁ ∘ σ , extend (out⁻¹ ∘ (id +₁ τ)) ∘ D₁ i₂ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ ([]-cong₂ refl (refl⟩∘⟨ ([]-cong₂ (pullˡ (sym DK.assoc ○ extend-≈ (pullˡ DK.identityʳ))) (pullˡ (sym DK.assoc ○ extend-≈ (pullˡ DK.identityʳ)))))) ⟩∘⟨refl ⟩
[ (id +₁ τ) , i₂ ∘ [ extend ((out⁻¹ ∘ (id +₁ τ)) ∘ i₁) ∘ σ , extend ((out⁻¹ ∘ (id +₁ τ)) ∘ i₂) ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ []-cong₂ refl (refl⟩∘⟨ []-cong₂ (extend-≈ (pullʳ inject₁) ⟩∘⟨refl) (extend-≈ (pullʳ inject₂) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
[ (id +₁ τ) , i₂ ∘ [ extend (out⁻¹ ∘ i₁ ∘ id) ∘ σ , extend (out⁻¹ ∘ i₂ ∘ τ) ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ []-cong₂ refl (refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ (refl⟩∘⟨ identityʳ) ○ DK.identityˡ)) (extend-≈ sym-assoc ⟩∘⟨refl ○ sym (pullˡ (later∘extend τ)))) ⟩∘⟨refl ⟩
[ (id +₁ τ) , i₂ ∘ [ σ , later ∘ extend τ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ≈⟨ helper₃ ⟩
[ id +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ w ≈˘⟨ cancelˡ out∘out⁻¹ ⟩
out ∘ out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ w ∎)
where
helper₂ : (D₁ distributeˡ⁻¹) ∘ σ ≈ [ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ∘ distributeˡ⁻¹
helper₂ = Iso⇒Epi (IsIso.iso isIsoˡ) ((D₁ distributeˡ⁻¹) ∘ σ) ([ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ∘ distributeˡ⁻¹) (begin
((D₁ distributeˡ⁻¹) ∘ σ) ∘ distributeˡ ≈⟨ ∘[] ○ []-cong₂ (refl⟩∘⟨ ×₁-cong₂ (sym D.F.identity) refl) (refl⟩∘⟨ ×₁-cong₂ (sym D.F.identity) refl) ⟩
[ ((D₁ distributeˡ⁻¹) ∘ σ) ∘ (D₁ id ×₁ i₁) , ((D₁ distributeˡ⁻¹) ∘ σ) ∘ (D₁ id ×₁ i₂) ] ≈⟨ []-cong₂ (pullʳ (σ-natural id i₁)) (pullʳ (σ-natural id i₂)) ⟩
[ (D₁ distributeˡ⁻¹) ∘ D₁ (id ×₁ i₁) ∘ σ , (D₁ distributeˡ⁻¹) ∘ D₁ (id ×₁ i₂) ∘ σ ] ≈⟨ []-cong₂ (pullˡ (sym D.F.homomorphism)) (pullˡ (sym D.F.homomorphism)) ⟩
[ D₁ (distributeˡ⁻¹ ∘ (id ×₁ i₁)) ∘ σ , D₁ (distributeˡ⁻¹ ∘ (id ×₁ i₂)) ∘ σ ] ≈⟨ []-cong₂ (D.F.F-resp-≈ distributeˡ⁻¹-i₁ ⟩∘⟨refl) (D.F.F-resp-≈ distributeˡ⁻¹-i₂ ⟩∘⟨refl) ⟩
[ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
([ D₁ i₁ ∘ σ , D₁ i₂ ∘ σ ] ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
helper₃ : [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out {X} ×₁ out {Y}) ≈ [ id +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ w
helper₃ = begin
[ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out {X} ×₁ out {Y}) ≈⟨ refl⟩∘⟨ helper ⟩
[ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ [ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w ≈⟨ pullˡ ∘[] ⟩
[ [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ [ i₁ ∘ i₁ , i₂ ∘ i₁ ]
, [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w ≈⟨ ([]-cong₂ ∘[] ∘[]) ⟩∘⟨refl ⟩
[ [ [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ i₁ ∘ i₁ , [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ i₂ ∘ i₁ ]
, [ [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ (i₁ ∘ i₂)
, [ id +₁ τ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ] ∘ (i₂ ∘ i₂) ] ] ∘ w ≈⟨ ([]-cong₂ ([]-cong₂ (pullˡ inject₁) (pullˡ inject₂ ○ assoc)) ([]-cong₂ (pullˡ inject₁) (pullˡ inject₂ ○ assoc))) ⟩∘⟨refl ⟩
[ [ (id +₁ τ) ∘ i₁ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ∘ i₁ ] , [ (id +₁ τ) ∘ i₂ , i₂ ∘ [ D₁ swap ∘ τ ∘ swap , later ∘ extend τ ∘ σ ] ∘ i₂ ] ] ∘ w ≈⟨ ([]-cong₂ ([]-cong₂ (+₁∘i₁ ○ identityʳ) (refl⟩∘⟨ inject₁)) ([]-cong₂ +₁∘i₂ (refl⟩∘⟨ inject₂))) ⟩∘⟨refl ⟩
[ [ i₁ , i₂ ∘ σ ] , [ i₂ ∘ τ , i₂ ∘ later ∘ extend τ ∘ σ ] ] ∘ w ≈˘⟨ ([]-cong₂ ([]-cong₂ identityʳ refl) ∘[]) ⟩∘⟨refl ⟩
[ id +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ w ∎
where
helper : (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out {X} ×₁ out {Y}) ≈ [ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w
helper = sym (begin
[ [ i₁ ∘ i₁ , i₂ ∘ i₁ ] , [ (i₁ ∘ i₂) , (i₂ ∘ i₂) ] ] ∘ w ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ ((+₁-cong₂ (sym distributeˡ⁻¹-i₁) (sym distributeˡ⁻¹-i₁)) ⟩∘⟨refl) ((+₁-cong₂ (sym distributeˡ⁻¹-i₂) (sym distributeˡ⁻¹-i₂)) ⟩∘⟨refl)) ⟩
[ (distributeˡ⁻¹ ∘ (id ×₁ i₁) +₁ distributeˡ⁻¹ ∘ (id ×₁ i₁)) ∘ distributeʳ⁻¹
, (distributeˡ⁻¹ ∘ (id ×₁ i₂) +₁ distributeˡ⁻¹ ∘ (id ×₁ i₂)) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈˘⟨ ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁)) ⟩∘⟨refl ⟩
[ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ ((id ×₁ i₁) +₁ (id ×₁ i₁)) ∘ distributeʳ⁻¹
, (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ ((id ×₁ i₂) +₁ (id ×₁ i₂)) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈˘⟨ pullˡ ∘[] ⟩
(distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ [ ((id ×₁ i₁) +₁ (id ×₁ i₁)) ∘ distributeʳ⁻¹ , ((id ×₁ i₂) +₁ (id ×₁ i₂)) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ refl⟩∘⟨ []-cong₂ (distributeʳ⁻¹-natural i₁ id id) (distributeʳ⁻¹-natural i₂ id id) ⟩∘⟨refl ⟩
(distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ [ distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ i₁) , distributeʳ⁻¹ ∘ ((id +₁ id) ×₁ i₂) ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈˘⟨ refl⟩∘⟨ pullˡ ∘[] ⟩
(distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ [ ((id +₁ id) ×₁ i₁) , ((id +₁ id) ×₁ i₂) ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ([]-cong₂ (×₁-cong₂ ([]-unique id-comm-sym id-comm-sym) refl) (×₁-cong₂ ([]-unique id-comm-sym id-comm-sym) refl)) ⟩∘⟨refl ⟩
(distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ [ (id ×₁ i₁) , (id ×₁ i₂) ] ∘ distributeˡ⁻¹ ∘ (out ×₁ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩
(distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (out ×₁ out) ∎)
fixpoint-eq : ∀ {f : D₀ X × D₀ Y ⇒ D₀ (X × Y)} → f ≈ out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ f ] ] ∘ w → f ≈ extend [ now , f ] ∘ g
fixpoint-eq {f} fix = begin
f ≈⟨ fix ⟩
out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , later ∘ f ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl (pullʳ inject₂))) ⟩∘⟨refl ⟩
out⁻¹ ∘ [ id +₁ σ , i₂ ∘ [ τ , (later ∘ [ now , f ]) ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (sym ∘[] ○ refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ inject₁ ○ DK.identityˡ)) (pullˡ DK.identityʳ)) ⟩∘⟨refl ⟩
out⁻¹ ∘ [ id +₁ σ , [ i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ τ , i₂ ∘ extend (later ∘ [ now , f ]) ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (([]-cong₂ ([]-cong₂ (sym identityʳ) (∘-resp-≈ʳ (elimˡ (extend-≈ inject₁ ○ DK.identityˡ)))) ([]-cong₂ (pullʳ (pullˡ (DK.sym-assoc ○ extend-≈ (pullˡ DK.identityʳ)))) (pullʳ (pullˡ (extend∘later [ now , f ]))))) ⟩∘⟨refl) ⟩
out⁻¹ ∘ [ [ i₁ , i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ σ ] , [ (i₂ ∘ extend [ now , f ]) ∘ D₁ i₁ ∘ τ , (i₂ ∘ extend [ now , f ]) ∘ later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ inject₁ (pullʳ (pullˡ ((sym DK.assoc) ○ extend-≈ (pullˡ DK.identityʳ))))) ∘[] ⟩∘⟨refl ⟩
out⁻¹ ∘ [ [ [ i₁ , out ∘ f ] ∘ i₁ , (i₂ ∘ extend [ now , f ]) ∘ D₁ i₁ ∘ σ ] , (i₂ ∘ extend [ now , f ]) ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (([]-cong₂ []∘+₁ (pullˡ inject₂)) ⟩∘⟨refl) ⟩
out⁻¹ ∘ [ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ (i₁ +₁ D₁ i₁ ∘ σ) , [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ (pullˡ ∘[]) ⟩
out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈⟨ out-mono (out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w) (extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w) helper ⟩
extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ∎
where
helper = begin
out ∘ out⁻¹ ∘ [ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈⟨ cancelˡ out∘out⁻¹ ⟩
[ [ i₁ , out ∘ f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ ([]-cong₂ (∘[] ○ []-cong₂ unitlaw refl) refl) ⟩∘⟨refl ⟩
[ out ∘ [ now , f ] , i₂ ∘ extend [ now , f ] ] ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ pullʳ (cancelˡ out∘out⁻¹) ⟩
([ out ∘ [ now , f ] , i₂ ∘ extend [ now , f ] ] ∘ out) ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ pullˡ (extend-commutes [ now , f ]) ⟩
out ∘ extend [ now , f ] ∘ out⁻¹ ∘ [ i₁ +₁ D₁ i₁ ∘ σ , i₂ ∘ [ D₁ i₁ ∘ τ , later ∘ now ∘ i₂ ] ] ∘ w ∎