diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index 837066e..80a883f 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -1,26 +1,37 @@ ```agda -module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where +module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where open Ambient ambient - open import Monad.Instance.K ambient - open import Monad.Instance.K.Strong ambient - open import Monad.Instance.K.Commutative ambient - open import Monad.Instance.K.EquationalLifting ambient + open import Monad.Instance.K.Strong ambient MK + open import Monad.Instance.K.Commutative ambient MK + open import Monad.Instance.K.EquationalLifting ambient MK + open import Category.Construction.UniformIterationAlgebras ambient + open import Algebra.UniformIterationAlgebra ambient + open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) + open MIK ambient + open MonadK MK open Terminal terminal using (⊤; !) open Initial using () renaming (! to ¡) + + open HomReasoning + open Equiv + open MR C ``` @@ -33,7 +44,71 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X -- TODO induction, see proposition 2.3 https://ncatlab.org/nlab/show/natural+numbers+object [_,_]#⟩ : ∀ {X A : Obj} → (⊤ ⇒ A) → X ⇒ A + X → X × N ⇒ A - [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) (([ π₂ , π₁ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ f ∘ π₁)) - -- TODO might be wrong, check it by testing kleene fixpoint + [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) + -- TODO might be wrong, check it by testing kleene fixpoint ʳ + + -- Notation + open kleisliK using (extend) + open monadK using (η; μ) + open strongK using (strengthen) + _↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → X ⇒ K.₀ X + _↓ f = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ + + _⇂_ : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → X ⇒ K.₀ Y + _⇂_ {X} {Y} {Z} f g = extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩ + + restrict-η : ∀ {X Y} (f : X ⇒ K.₀ Y) → f ↓ ≈ η.η _ ⇂ f + restrict-η {X} {Y} f = begin + K.₁ π₁ ∘ τ (X , Y) ∘ ⟨ idC , f ⟩ ≈˘⟨ cancelˡ monadK.identityˡ ⟩∘⟨refl ⟩∘⟨refl ○ assoc ⟩ + ((μ.η _ ∘ K.₁ (η.η _) ∘ K.₁ π₁) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈⟨ ((refl⟩∘⟨ (sym K.homomorphism)) ⟩∘⟨refl) ⟩∘⟨refl ⟩ + ((μ.η _ ∘ K.₁ (η.η _ ∘ π₁)) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈⟨ ((refl⟩∘⟨ (K.F-resp-≈ (sym π₁∘⁂))) ⟩∘⟨refl) ⟩∘⟨refl ⟩ + ((μ.η _ ∘ K.₁ (π₁ ∘ (η.η _ ⁂ idC))) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈˘⟨ pullˡ (pullˡ (pullʳ (sym K.homomorphism))) ⟩ + (μ.η _ ∘ K.₁ π₁) ∘ (K.₁ (η.η _ ⁂ idC) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈⟨ refl ⟩ + extend π₁ ∘ (K.₁ (η.η _ ⁂ idC) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ pullˡ (strengthen.commute _) ⟩ + extend π₁ ∘ τ (K.₀ X , Y) ∘ (η.η _ ⁂ K.₁ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂-cong₂ refl K.identity) ⟩∘⟨refl ⟩ + extend π₁ ∘ τ (K.₀ X , Y) ∘ (η.η _ ⁂ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ + extend π₁ ∘ τ (K.₀ X , Y) ∘ ⟨ η.η _ , f ⟩ ∎ + + restrict-law : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → f ⇂ g ≈ extend f ∘ g ↓ + restrict-law {X} {Y} {Z} f g = begin + extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ + extend π₁ ∘ τ (K.₀ Y , Z) ∘ (f ⁂ idC) ∘ ⟨ idC , g ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm-id f)) ⟩ + extend π₁ ∘ (K.₁ (f ⁂ idC) ∘ τ (X , Z)) ∘ ⟨ idC , g ⟩ ≈⟨ (refl⟩∘⟨ assoc) ○ pullˡ (pullʳ (sym K.homomorphism)) ⟩ + (μ.η _ ∘ K.₁ (π₁ ∘ (f ⁂ idC))) ∘ τ (X , Z) ∘ ⟨ idC , g ⟩ ≈⟨ (refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ○ K.homomorphism)) ⟩∘⟨refl ⟩ + (μ.η Y ∘ (K.₁ f ∘ K.₁ π₁)) ∘ τ (X , Z) ∘ ⟨ idC , g ⟩ ≈⟨ sym-assoc ⟩∘⟨refl ○ assoc ⟩ + extend f ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ∎ + + dom-η : ∀ {X Y} (f : X ⇒ K.₀ Y) → (η.η _ ∘ f) ↓ ≈ η.η _ + dom-η {X} {Y} f = begin + K.₁ π₁ ∘ τ _ ∘ ⟨ idC , η.η _ ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩ + K.₁ π₁ ∘ τ _ ∘ (idC ⁂ η.η _) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩ + K.₁ π₁ ∘ η.η _ ∘ ⟨ idC , f ⟩ ≈⟨ pullˡ (K₁η π₁) ⟩ + (η.η _ ∘ π₁) ∘ ⟨ idC , f ⟩ ≈⟨ cancelʳ project₁ ⟩ + η.η _ ∎ + + _⊑_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e + f ⊑ g = f ≈ g ⇂ f + + dom-⊑ : ∀ {X Y} (f : X ⇒ K.₀ Y) → (f ↓) ⊑ (η.η _) + dom-⊑ {X} {Y} f = begin + -- TODO try with RST laws + (f ↓) ≈⟨ refl ⟩ + K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + extend π₁ ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {! !} ⟩ -- multiple steps + extend π₁ ∘ K.₁ (idC ⁂ π₁) ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {! !} ⟩ + extend π₁ ∘ τ _ ∘ (idC ⁂ K.₁ π₁) ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {! !} ⟩ + extend π₁ ∘ τ _ ∘ ⟨ η.η X , K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {! !} ⟩ + ((η.η X) ⇂ (f ↓)) ∎ + + -- some helper definitions to make our life easier + private + _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f + _♯ˡ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ˡ {Y = X} (stable X) {X = A} (algebras Y) f + _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f + + kleene : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g + kleene = {! !} ``` diff --git a/src/Monad/Instance/K/Strong.lagda.md b/src/Monad/Instance/K/Strong.lagda.md index 5077bb7..e6050aa 100644 --- a/src/Monad/Instance/K/Strong.lagda.md +++ b/src/Monad/Instance/K/Strong.lagda.md @@ -265,4 +265,14 @@ The following diagram demonstrates this: { M = monadK ; strength = KStrength } + + τ-comm-id : ∀ {X Y Z} (f : X ⇒ Y) → τ (Y , Z) ∘ (f ⁂ idC) ≈ K.₁ (f ⁂ idC) ∘ τ (X , Z) + τ-comm-id {X} {Y} {Z} f = begin + τ (Y , Z) ∘ (f ⁂ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym K.identity)) ⟩ + τ (Y , Z) ∘ (f ⁂ K.₁ idC) ≈⟨ strengthen.commute (f , idC) ⟩ + K.₁ (f ⁂ idC) ∘ τ (X , Z) ∎ + where + open Strength KStrength using (strengthen) + + module strongK = StrongMonad KStrong ```