mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
No commits in common. "c7f9ccf05af8f4a2998237c31c1fd19487c66f6d" and "3e4ecb3dfb2f18d665d155c0d4f5c9449426e057" have entirely different histories.
c7f9ccf05a
...
3e4ecb3dfb
3 changed files with 40 additions and 127 deletions
|
|
@ -1,6 +1,5 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
open import Level
|
||||
open import Categories.Functor renaming (id to idF)
|
||||
open import Categories.Functor.Algebra
|
||||
|
|
@ -134,9 +133,10 @@ Here we give a different Characterization and show that it is equal.
|
|||
by-uni = begin
|
||||
([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩
|
||||
[ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ idC) ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩
|
||||
[ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘i₁ ○ identityʳ)) (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ +₁∘i₁) (pullˡ +₁∘i₂ ○ pullʳ (+₁∘i₂ ○ identityʳ))) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩
|
||||
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩
|
||||
-- TODO all these steps work
|
||||
[ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈⟨ {! !} ⟩
|
||||
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈⟨ {! !} ⟩
|
||||
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈⟨ {! !} ⟩
|
||||
(idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
|
||||
|
||||
-- TODO Proposition 41
|
||||
|
|
@ -147,24 +147,22 @@ Here we give a different Characterization and show that it is equal.
|
|||
[ (idC +₁ i₁) ∘ g , f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ i₁) ∘ g , (idC +₁ idC) ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩
|
||||
[ ([ idC , idC ] +₁ idC) ∘ ((i₁ +₁ i₁) ∘ g) , ([ idC , idC ] +₁ idC) ∘ ((i₂ +₁ idC) ∘ f) ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩
|
||||
(([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] idC) ⟩∘⟨refl) ⟩
|
||||
([ i₁ ∘ idC , [ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] ] # ∘ i₂) ∘ i₂ ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩
|
||||
(([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ {! !} ⟩ -- lemma 40
|
||||
[ i₁ , ([ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ]) ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩
|
||||
[ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
|
||||
[ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
|
||||
[ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
|
||||
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X} ≈⟨ sym (#-Uniformity (sym by-uni₂)) ⟩
|
||||
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ {! !} ⟩
|
||||
-- [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni₂))) ⟩
|
||||
-- {! !} ≈⟨ {! !} ⟩
|
||||
-- [ {! !} , [ [ i₁ , (idC +₁ i₂ ∘ i₁ ∘ i₂) ∘ g ] , i₂ ∘ i₂ ∘ h ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ (#-Uniformity by-uni₃ ⟩∘⟨refl) ○ assoc ⟩
|
||||
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
(([ {! !} , {! !} ] ∘ f) #) ≈⟨ #-Uniformity (sym by-uni₃) ⟩
|
||||
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) (pullˡ ∘[]))) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩
|
||||
([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩
|
||||
([ idC , g # ] +₁ h ) # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩
|
||||
[ i₁ ∘ [ idC , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩
|
||||
[ i₁ ∘ [ idC , g # ] , [ [ idC , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ idC) ∘ h ] # ∘ i₂ ≈⟨ sym (#-Stutter ((i₂ +₁ idC) ∘ h) [ idC , g # ]) ⟩
|
||||
(([ [ idC , g # ] , [ idC , g # ] ] +₁ idC) ∘ (i₂ +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩
|
||||
((([ idC , g # ] +₁ idC)) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩
|
||||
([ (i₁ ∘ [ idC , g # ]) ∘ i₁ , [ idC , g # ] ∘ i₂ +₁ idC ∘ idC ] ∘ f) # ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩
|
||||
([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
([ i₁ , g # +₁ idC ] ∘ f) # ∎
|
||||
where
|
||||
g = (idC +₁ [ idC , idC ]) ∘ f
|
||||
|
|
@ -176,27 +174,22 @@ Here we give a different Characterization and show that it is equal.
|
|||
[ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩
|
||||
[ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩
|
||||
g ∘ [ idC , idC ] ∎
|
||||
by-uni₂ : [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ∘ i₂ ≈ (idC +₁ i₂ ∘ i₂) ∘ {! !}
|
||||
by-uni₂ : [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ≈ (idC +₁ i₂) ∘ {! !}
|
||||
by-uni₂ = begin
|
||||
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ∘ i₂ ≈⟨ (pullˡ inject₂) ○ inject₂ ⟩
|
||||
i₂ ∘ f ≈⟨ {! !} ⟩
|
||||
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ≈⟨ inject₂ ⟩
|
||||
[ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
(idC +₁ i₂) ∘ [ ((idC +₁ i₁) ∘ g) , {! h !} ] ∎
|
||||
by-uni₃ : (idC +₁ i₂) ∘ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ≈ {! !} ∘ i₂
|
||||
by-uni₃ = begin
|
||||
(idC +₁ i₂) ∘ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ≈⟨ ∘[] ⟩
|
||||
[ (idC +₁ i₂) ∘ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , (idC +₁ i₂) ∘ i₂ ∘ h ] ≈⟨ []-cong₂ ∘[] (pullˡ +₁∘i₂) ⟩
|
||||
[ [ (idC +₁ i₂) ∘ i₁ , (idC +₁ i₂) ∘ (idC +₁ i₁ ∘ i₂) ∘ g ] , (i₂ ∘ i₂) ∘ h ] ≈⟨ []-cong₂ ([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) assoc ⟩
|
||||
[ [ i₁ , (idC +₁ i₂ ∘ i₁ ∘ i₂) ∘ g ] , i₂ ∘ i₂ ∘ h ] ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ∎
|
||||
by-uni₃ : [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₂ ≈ (idC +₁ i₂) ∘ {! !}
|
||||
by-uni₃ = begin
|
||||
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₂ ≈⟨ inject₂ ⟩
|
||||
i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f ≈⟨ pullˡ ∘[] ⟩
|
||||
[ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
(idC +₁ i₂) ∘ [ i₁ , {! i₂ !} ] ∘ f ∎
|
||||
by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
|
||||
by-fix = sym (begin
|
||||
[ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩
|
||||
[ idC , [ idC , g # ] ∘ g ] ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩
|
||||
[ idC , [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ] ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩
|
||||
[ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (idC +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩
|
||||
([ i₁ , (idC +₁ i₂) ∘ g ] #) ∎)
|
||||
|
||||
-- every elgot-algebra comes with a divergence constant
|
||||
!ₑ : ⊥ ⇒ A
|
||||
|
|
|
|||
|
|
@ -210,36 +210,13 @@ KCommutative = record { commutes = commutes' }
|
|||
(idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
|
||||
comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
|
||||
comm₈ {U} g = begin
|
||||
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ στ ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ {! !} ⟩ -- lemma 42
|
||||
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ sym τσ ⟩
|
||||
((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
|
||||
where
|
||||
τσ : ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ≈ extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
|
||||
τσ = begin
|
||||
(((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
|
||||
στ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈ extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
|
||||
στ = begin
|
||||
((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩
|
||||
((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
|
||||
(((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
|
||||
(((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) comm) ⟩
|
||||
extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
|
||||
extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
|
||||
extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
|
||||
extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ⁂ idC) ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
|
||||
extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
|
||||
extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ idC) ∘ g) # , idC))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ K.₁ idC)) ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
|
||||
extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
|
||||
(((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
|
||||
where
|
||||
by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
|
||||
by-uni = begin
|
||||
|
|
@ -248,10 +225,4 @@ KCommutative = record { commutes = commutes' }
|
|||
(ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩
|
||||
(((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩
|
||||
(idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
|
||||
comm : (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ≈ (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
|
||||
comm = sym (begin
|
||||
(τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩
|
||||
(τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η (K.₀ Y)) idC)) ⟩
|
||||
(τ _ +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)
|
||||
```
|
||||
|
|
|
|||
|
|
@ -1,51 +0,0 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory
|
||||
open import Categories.Category
|
||||
open import Categories.Category.Instance.Setoids
|
||||
open import Categories.Monad
|
||||
open import Categories.Category.Monoidal.Instance.Setoids
|
||||
open import Categories.Category.Cocartesian
|
||||
open import Categories.Object.Terminal
|
||||
open import Function.Equality as SΠ renaming (id to ⟶-id)
|
||||
import Categories.Morphism.Reasoning as MR
|
||||
open import Relation.Binary
|
||||
open import Agda.Builtin.Unit using (tt)
|
||||
|
||||
```
|
||||
-->
|
||||
|
||||
```agda
|
||||
module Monad.Instance.K.Instance.Maybe {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient using ()
|
||||
```
|
||||
|
||||
# The Maybe Monad as instance of K
|
||||
Assuming the axiom of choice, the maybe monad is an instance of K in the category of setoids.
|
||||
|
||||
```agda
|
||||
module _ {c ℓ' : Level} where
|
||||
open Cocartesian (Setoids-Cocartesian {c} {c ⊔ ℓ'})
|
||||
open Terminal (terminal {c} {c ⊔ ℓ'})
|
||||
open MR (Setoids c (c ⊔ ℓ'))
|
||||
open Category (Setoids c (c ⊔ ℓ'))
|
||||
open Equiv
|
||||
|
||||
maybe : Monad (Setoids c (c ⊔ ℓ'))
|
||||
maybe = record
|
||||
{ F = record
|
||||
{ F₀ = λ X → X + ⊤
|
||||
; F₁ = λ {A} {B} f → f +₁ ⟶-id
|
||||
; identity = {! !}
|
||||
; homomorphism = {! !}
|
||||
; F-resp-≈ = λ {A} {B} {f} {g} f≈g → +₁-cong₂ f≈g ?
|
||||
}
|
||||
; η = {! !}
|
||||
; μ = {! !}
|
||||
; assoc = {! !}
|
||||
; sym-assoc = {! !}
|
||||
; identityˡ = {! !}
|
||||
; identityʳ = {! !}
|
||||
}
|
||||
```
|
||||
Loading…
Reference in a new issue