From 5bdc57f064d126e4c608f9bf795390477313dc53 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 6 Nov 2023 15:26:18 +0100 Subject: [PATCH] Finished small proof --- .../Instance/AmbientCategory.lagda.md | 10 +++++ src/Monad/Instance/K/PreElgot.lagda.md | 37 +++++++++++++------ 2 files changed, 36 insertions(+), 11 deletions(-) diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index fc50d95..3c35e27 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -200,4 +200,14 @@ module Category.Instance.AmbientCategory where μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩ F.₁ f ∎ where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ) + + extend∘F₁ : ∀ (M : Monad C) {X Y Z} (f : Y ⇒ Monad.F.₀ M Z) (g : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) f ∘ Monad.F.₁ M g ≈ RMonad.extend (Monad⇒Kleisli C M) (f ∘ g) + extend∘F₁ M f g = begin + extend f ∘ F.₁ g ≈⟨ (refl⟩∘⟨ sym (F₁⇒extend M g)) ⟩ + extend f ∘ extend (unit ∘ g) ≈⟨ k-sym-assoc ⟩ + extend (extend f ∘ unit ∘ g) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ + extend (f ∘ g) ∎ + where + open Monad M using (F) + open RMonad (Monad⇒Kleisli C M) using (extend; unit; extend-≈) renaming (sym-assoc to k-sym-assoc; identityʳ to k-identityʳ) ``` \ No newline at end of file diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index 80a883f..17356a9 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -45,7 +45,6 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X [_,_]#⟩ : ∀ {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 ʳ -- Notation open kleisliK using (extend) @@ -91,15 +90,28 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X 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 ⟩ ⟩ ≈⟨ {! !} ⟩ + K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ≈⟨ (sym (F₁⇒extend monadK π₁)) ⟩∘⟨refl ⟩ + extend (η.η X ∘ π₁) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ (kleisliK.extend-≈ (pullˡ project₁)) ⟩∘⟨refl ⟩ + extend (π₁ ∘ ⟨ η.η X , idC ⟩ ∘ π₁) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ (kleisliK.extend-≈ (pullʳ π₁∘⁂)) ⟩∘⟨refl ⟩ + extend ((π₁ ∘ π₁) ∘ (⟨ η.η X , idC ⟩ ⁂ idC)) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ pullˡ (extend∘F₁ monadK (π₁ ∘ π₁) (⟨ η.η X , idC ⟩ ⁂ idC)) ⟩ + extend (π₁ ∘ π₁) ∘ K.₁ ((⟨ η.η X , idC ⟩ ⁂ idC)) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ pullʳ (pullˡ (τ-comm-id ⟨ η.η X , idC ⟩) ○ assoc) ⟩ + (extend (π₁ ∘ π₁) ∘ τ _) ∘ (⟨ η.η X , idC ⟩ ⁂ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ + (extend (π₁ ∘ π₁) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ ((kleisliK.extend-≈ project₁) ⟩∘⟨refl) ⟩∘⟨refl ⟩ + (extend (π₁ ∘ assocˡ) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ (kleisliK.extend-≈ (pullˡ kleisliK.identityʳ)) ⟩∘⟨refl ⟩∘⟨refl ⟩ + (extend (extend π₁ ∘ η.η _ ∘ assocˡ) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ pullˡ (pullˡ kleisliK.sym-assoc) ⟩ + extend π₁ ∘ (extend (η.η _ ∘ assocˡ) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈⟨ refl⟩∘⟨ ((F₁⇒extend monadK assocˡ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + extend π₁ ∘ (K.₁ assocˡ ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ (elimʳ project₁) refl) refl ⟩ + extend π₁ ∘ (K.₁ assocˡ ∘ τ _) ∘ ⟨ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , idC ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ sym strongK.strength-assoc)) ⟩ + extend π₁ ∘ τ _ ∘ (idC ⁂ τ _) ∘ assocˡ ∘ ⟨ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , idC ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ assocʳ∘⟨⟩ ⟩ + extend π₁ ∘ τ _ ∘ (idC ⁂ τ _) ∘ (assocˡ ∘ assocʳ) ∘ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ assocˡ∘assocʳ ⟩ + extend π₁ ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityˡ refl)) ⟩ + extend π₁ ∘ τ _ ∘ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (elimʳ project₁) refl ⟩ + extend π₁ ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ (sym (kleisliK.extend-≈ (π₁∘⁂ ○ identityˡ))) ⟩∘⟨refl ⟩ -- multiple steps + extend (π₁ ∘ (idC ⁂ π₁)) ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈˘⟨ pullˡ (extend∘F₁ monadK π₁ (idC ⁂ π₁)) ⟩ + extend π₁ ∘ K.₁ (idC ⁂ π₁) ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (sym (strengthen.commute (idC , π₁))) ○ assoc) ⟩ + extend π₁ ∘ τ _ ∘ (idC ⁂ K.₁ π₁) ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ + extend π₁ ∘ τ _ ∘ ⟨ η.η X , K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl ⟩ ((η.η X) ⇂ (f ↓)) ∎ -- some helper definitions to make our life easier @@ -108,7 +120,10 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X _♯ˡ = λ {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 = {! !} + kleene₁ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁) + kleene₁ = {! !} + + kleene₂ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g + kleene₂ = {! !} ```