mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Work on commutativity
This commit is contained in:
parent
82cd7c9aa6
commit
34c5a62d09
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 74 additions and 45 deletions
|
|
@ -140,8 +140,8 @@ extend-preserve {X} {Y} {Z} f h = begin
|
|||
private
|
||||
comm-helper : ∀ {X Y Z U} (f : X ⇒ K.₀ Y + X) (g : Z ⇒ K.₀ U + Z) → extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ≈ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #)
|
||||
comm-helper {X} {Y} {Z} {U} f g = begin
|
||||
extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈⟨ τσ ⟩
|
||||
extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w # ≈⟨ {! !} ⟩
|
||||
extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈⟨ τσ ⟩
|
||||
extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w # ≈⟨ {! !} ⟩
|
||||
extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ f) # ⁂ ((η _ +₁ idC) ∘ g) #) ∎
|
||||
where
|
||||
f' = (η _ +₁ idC) ∘ f
|
||||
|
|
@ -149,55 +149,82 @@ private
|
|||
w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')
|
||||
w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #
|
||||
w-law₁ = sym (begin
|
||||
extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ step₁ ⟩
|
||||
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ {! !} ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹) ] ∘ distributeʳ⁻¹ ∘ {! !} ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ {! !}) ⟩
|
||||
-- TODO whatever is going wrong here?????
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹) ] ∘ ({! idC ⁂ idC !} +₁ {! !}) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ {! elimʳ !} {! !})) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ π₁ , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (π₁ ⁂ idC) ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distribute₁ π₁ idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , (f' # ∘ π₁ +₁ idC) ∘ ((π₁ ⁂ idC) +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₁∘⁂) identityˡ))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ ∘ π₁ +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , (((f' # ∘ π₁) +₁ idC) ∘ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩
|
||||
([ i₁ , (f' # ∘ π₁) +₁ idC ] ∘ h) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩
|
||||
([ i₁ , ((idC +₁ ∇) ∘ h) # +₁ idC ] ∘ h) # ≈˘⟨ {! !} ⟩ -- proposition 41
|
||||
((idC +₁ ∇) ∘ h)# ≈⟨ #-Uniformity (algebras _) by-uni ⟩
|
||||
(f' #) ∘ π₁ ∎)
|
||||
extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ step₁ ⟩
|
||||
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ sym step₂ ⟩
|
||||
(f' #) ∘ π₁ ∎)
|
||||
where
|
||||
h = (π₁ +₁ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)
|
||||
step₁ : extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))#
|
||||
step₁ = begin
|
||||
extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ extend-preserve [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] w ⟩
|
||||
((extend [ f' # ∘ π₁ , η _ ∘ π₁ ] +₁ idC) ∘ w) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩
|
||||
([ (i₁ ∘ extend [ f' # ∘ π₁ , η _ ∘ π₁ ]) ∘ K.₁ i₁ ∘ τ _ , ((extend (η (K.₀ Y) ∘ π₁) ∘ σ _ +₁ idC)) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK [ f' # ∘ π₁ , η _ ∘ π₁ ] i₁ ○ kleisliK.extend-≈ inject₁))) ((+₁-cong₂ ((refl⟩∘⟨ monadK.F.homomorphism) ⟩∘⟨refl ○ (cancelˡ kleisliK.identityˡ) ⟩∘⟨refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (η (K.₀ U)) idC)) ○ assoc)) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ (idC ⁂ η _ +₁ idC ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ ∘ (idC ⁂ η _) , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (τ-η _) ○ kleisliK.identityʳ)) ((+₁-cong₂ {! !} refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ -- K.₁ π₁ law for σ
|
||||
([ i₁ ∘ f' # ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ ((#-Fixpoint (algebras _)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ (sym π₁∘⁂))) refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ ∘ (f' ⁂ idC) , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc)) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ ((f' ⁂ idC) +₁ (f' ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distribute₁ f' idC idC))) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ (distributeˡ⁻¹ ∘ (f' ⁂ (idC +₁ idC))) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))))) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ sym distribute₂') refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' refl)) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ pullˡ distribute₄) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (∘[] ○ []-cong₂ []∘+₁ []∘+₁))) ⟩
|
||||
(([ [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₁) , (((π₁ +₁ idC)) ∘ i₁) ] , [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₂) , (((π₁ +₁ idC)) ∘ i₂) ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (assoc ○ ([]-cong₂ ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₁) +₁∘i₁) ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₂) +₁∘i₂)) ⟩∘⟨refl) ⟩
|
||||
([ [ (i₁ ∘ idC ∘ π₁) , i₁ ∘ π₁ ] , [ i₁ ∘ f' # ∘ π₁ , i₂ ∘ idC ] ] ∘ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ ([]-cong₂ (refl⟩∘⟨ identityˡ) refl ○ sym ∘[]) refl) ⟩∘⟨ assoc) ⟩
|
||||
([ i₁ ∘ [ π₁ , π₁ ] , f' # ∘ π₁ +₁ idC ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc refl)) ⟩
|
||||
([ i₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ distribute₃) refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ∎
|
||||
by-uni : (idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈ f' ∘ π₁
|
||||
by-uni = begin
|
||||
(idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩
|
||||
(idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩
|
||||
(π₁ +₁ π₁ ∘ [ (idC ∘ π₁) , (idC ∘ (π₁ ⁂ idC)) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ∘[] ○ ([]-cong₂ (refl⟩∘⟨ identityˡ) ((refl⟩∘⟨ identityˡ) ○ π₁∘⁂)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
|
||||
(π₁ +₁ [ π₁ ∘ π₁ , π₁ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distribute₃))) ⟩∘⟨refl ⟩
|
||||
(π₁ +₁ (π₁ ∘ π₁) ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (cancelʳ project₁)) ⟩∘⟨refl ⟩
|
||||
(π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ pullˡ distribute₂' ⟩
|
||||
π₁ ∘ (f' ⁂ idC) ≈⟨ π₁∘⁂ ⟩
|
||||
f' ∘ π₁ ∎
|
||||
(π₁ +₁ [ π₁ ∘ π₁ , π₁ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distribute₃))) ⟩∘⟨refl ⟩
|
||||
(π₁ +₁ (π₁ ∘ π₁) ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (cancelʳ project₁)) ⟩∘⟨refl ⟩
|
||||
(π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ pullˡ distribute₂' ⟩
|
||||
π₁ ∘ (f' ⁂ idC) ≈⟨ π₁∘⁂ ⟩
|
||||
f' ∘ π₁ ∎
|
||||
step₂ : (f' #) ∘ π₁ ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))#
|
||||
step₂ = begin
|
||||
(f' #) ∘ π₁ ≈˘⟨ #-Uniformity (algebras _) by-uni ⟩
|
||||
((idC +₁ ∇) ∘ h)# ≈⟨ {! !} ⟩ -- proposition 41
|
||||
([ i₁ , ((idC +₁ ∇) ∘ h) # +₁ idC ] ∘ h) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩
|
||||
([ i₁ , (f' # ∘ π₁) +₁ idC ] ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩
|
||||
([ (i₁ ∘ π₁) , (((f' # ∘ π₁) +₁ idC) ∘ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ ∘ π₁ +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₁∘⁂) identityˡ))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , (f' # ∘ π₁ +₁ idC) ∘ ((π₁ ⁂ idC) +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distribute₁ π₁ idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (π₁ ⁂ idC) ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)))) ⟩∘⟨refl) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ π₁ , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (π₁∘⁂ ○ identityˡ)) (assoc ○ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ refl))) ⟩
|
||||
([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹) ] ∘ (idC ⁂ g +₁ idC ⁂ g) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distribute₁' g idC idC) ○ assoc)) ⟩
|
||||
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ g) ∘ (f' ⁂ idC))# ≈˘⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) identityʳ)) ⟩
|
||||
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ∎
|
||||
step₁ : extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))#
|
||||
step₁ = begin
|
||||
extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ extend-preserve [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] w ⟩
|
||||
((extend [ f' # ∘ π₁ , η _ ∘ π₁ ] +₁ idC) ∘ w) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩
|
||||
([ (i₁ ∘ extend [ f' # ∘ π₁ , η _ ∘ π₁ ]) ∘ K.₁ i₁ ∘ τ _ , ((extend (η (K.₀ Y) ∘ π₁) ∘ σ _ +₁ idC)) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK [ f' # ∘ π₁ , η _ ∘ π₁ ] i₁ ○ kleisliK.extend-≈ inject₁))) ((+₁-cong₂ ((refl⟩∘⟨ monadK.F.homomorphism) ⟩∘⟨refl ○ (cancelˡ kleisliK.identityˡ) ⟩∘⟨refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (η (K.₀ U)) idC)) ○ assoc)) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ (idC ⁂ η _ +₁ idC ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩
|
||||
([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ ∘ (idC ⁂ η _) , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (τ-η _) ○ kleisliK.identityʳ)) ((+₁-cong₂ {! !} refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ -- K.₁ π₁ law for σ
|
||||
([ i₁ ∘ f' # ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ ((#-Fixpoint (algebras _)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ (sym π₁∘⁂))) refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ ∘ (f' ⁂ idC) , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc)) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ ((f' ⁂ idC) +₁ (f' ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distribute₁ f' idC idC))) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ (distributeˡ⁻¹ ∘ (f' ⁂ (idC +₁ idC))) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))))) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ sym distribute₂') refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' refl)) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ pullˡ distribute₄) ⟩
|
||||
([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (∘[] ○ []-cong₂ []∘+₁ []∘+₁))) ⟩
|
||||
(([ [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₁) , (((π₁ +₁ idC)) ∘ i₁) ] , [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₂) , (((π₁ +₁ idC)) ∘ i₂) ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (assoc ○ ([]-cong₂ ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₁) +₁∘i₁) ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₂) +₁∘i₂)) ⟩∘⟨refl) ⟩
|
||||
([ [ (i₁ ∘ idC ∘ π₁) , i₁ ∘ π₁ ] , [ i₁ ∘ f' # ∘ π₁ , i₂ ∘ idC ] ] ∘ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ ([]-cong₂ (refl⟩∘⟨ identityˡ) refl ○ sym ∘[]) refl) ⟩∘⟨ assoc) ⟩
|
||||
([ i₁ ∘ [ π₁ , π₁ ] , f' # ∘ π₁ +₁ idC ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc refl)) ⟩
|
||||
([ i₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ distribute₃) refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ∎
|
||||
w-law₂ : g' # ∘ π₂ ≈ extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w #
|
||||
w-law₂ = {! !}
|
||||
w-law₂ = sym (begin
|
||||
extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈⟨ step₁ ⟩
|
||||
([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g'))# ≈⟨ {! !} ⟩
|
||||
g' # ∘ π₂ ∎)
|
||||
where
|
||||
step₁ : extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈ ([ i₁ ∘ π₂ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f ⁂ g'))#
|
||||
step₁ = begin
|
||||
extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # ≈⟨ extend-preserve _ w ⟩
|
||||
((extend [ η _ ∘ π₂ , g' # ∘ π₂ ] +₁ idC) ∘ w) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ η (K.₀ U) ∘ π₂ , (g' #) ∘ π₂ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩
|
||||
([ (i₁ ∘ extend [ η _ ∘ π₂ , g' # ∘ π₂ ]) ∘ K.₁ i₁ ∘ τ _ , (extend ((g' #) ∘ π₂) ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK _ i₁ ○ kleisliK.extend-≈ inject₁ ○ Monad⇒Kleisli⇒Monad monadK π₂))) refl) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η _ +₁ idC) ⁂ idC) ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ Y)) idC)) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ σ _ +₁ idC) ∘ ((η _ ⁂ idC) +₁ (idC ⁂ idC)) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ σ-η) (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (extend (g' # ∘ π₂) ∘ η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ {! !} ⟩
|
||||
([ i₁ ∘ K.₁ π₂ ∘ τ _ , (g' # ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ∎
|
||||
τσ : extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈ extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w #
|
||||
τσ = {! !} -- begin
|
||||
-- extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ w-law₁ w-law₂ ⟩
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory
|
||||
open import Categories.Category
|
||||
|
|
|
|||
Loading…
Reference in a new issue