src/Monad/Instance/K/Commutative.lagda.md

@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Category.Instance.AmbientCategory
 open import Monad.Commutative

src/Monad/Instance/K/EquationalLifting.lagda.md

@@ -1,89 +0,0 @@
-<!--
-```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-open import Level
-open import Category.Instance.AmbientCategory
-open import Data.Product using (_,_)
-open import Categories.FreeObjects.Free
-open import Categories.Category.Construction.Kleisli
-open import Categories.Category.Restriction
-import Monad.Instance.K as MIK
-```
--->
-
-```agda
-module Monad.Instance.K.EquationalLifting {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
-open Ambient ambient
-open MIK ambient
-open MonadK MK
-open import Monad.Instance.K.Strong ambient MK
-open import Monad.Instance.K.Commutative ambient MK
-open import Category.Construction.UniformIterationAlgebras ambient
-open import Algebra.UniformIterationAlgebra ambient
-open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
-
-open HomReasoning
-open Equiv
-open MR C
-open kleisliK using (extend)
-open monadK using (μ)
-
--- some helper definitions to make our life easier
-private
-  η = λ Z → FreeObject.η (freealgebras Z)
-  _♯ = λ {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
-```
-
-# **K** is an equational lifting monad
-
-```agda
-equationalLifting : ∀ {X} → τ (K.₀ X , X) ∘ Δ {K.₀ X} ≈ K.₁ ⟨ η X , idC ⟩
-equationalLifting = {!   !}
-```
-
-From this we can follow that the kleisli category of **K** is a *restriction category*.
-
-```agda
--- TODO this a trivial restriction structure, since η is identity in the kleisli category... 
-kleisli-restriction : Restriction (Kleisli monadK)
-kleisli-restriction = record
-  { _↓ = λ f → η _
-  ; pidʳ = kleisliK.identityʳ
-  ; ↓-comm = refl
-  ; ↓-denestʳ = begin 
-    η _ ≈˘⟨ cancelˡ monadK.identityʳ ⟩ 
-    μ.η _ ∘ η _ ∘ η _ ≈˘⟨ pullʳ (K₁η (η _)) ⟩
-    (μ.η _ ∘ K.₁ (η _)) ∘ η _ ∎
-  ; ↓-skew-comm = λ {A} {B} {C} {g} {f} → begin 
-    (μ.η _ ∘ K.₁ (η _)) ∘ f ≈⟨ elimˡ monadK.identityˡ ⟩ 
-    f ≈˘⟨ kleisliK.identityʳ ⟩ 
-    extend f ∘ η _ ∎
-  ; ↓-cong = λ _ → refl
-  }
-
-kleisli-restriction' : Restriction (Kleisli monadK)
-kleisli-restriction' = record
-  { _↓ = λ f → K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
-  ; pidʳ = λ {A} {B} {f} → begin 
-    (μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC {A} , f ⟩ ≈⟨ {!   !} ⟩ 
-    (μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ (idC ⁂ f) ∘ ⟨ idC , idC ⟩ ≈⟨ {!   !} ⟩ 
-    (μ.η B ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ (idC ⁂ f) ∘ ⟨ idC , idC ⟩ ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    (μ.η B ∘ K.₁ f) ∘ η A ≈⟨ {!   !} ⟩ 
-    f ∎
-  ; ↓-comm = λ {A} {B} {D} {f} {g} → begin 
-    (μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ pullˡ (pullʳ (sym K.homomorphism)) ⟩ 
-    (μ.η _ ∘ K.₁ ((K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩) ∘ π₁)) ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {!   !} ⟩ 
-    (K.₁ π₁ ∘ (μ.η _ ∘ K.₁ ((τ _ ∘ ⟨ idC , f ⟩) ∘ π₁))) ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {!   !} ⟩ 
-    (K.₁ π₁ ∘ (μ.η _ ∘ K.₁ (τ _) ∘ K.₁ ⟨ π₁ , f ∘ π₁ ⟩)) ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
-    (μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ∎
-  ; ↓-denestʳ = {!   !}
-  ; ↓-skew-comm = {!   !}
-  ; ↓-cong = λ eq → refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl eq
-  }
-```