From 6bb5bd519e3bd5624d77eeff790783f575c2dbaa Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 1 Nov 2023 20:06:20 +0100
Subject: [PATCH] introduce equational lifting

---
 src/Monad/Instance/K/Commutative.lagda.md     |  1 +
 .../Instance/K/EquationalLifting.lagda.md     | 89 +++++++++++++++++++
 2 files changed, 90 insertions(+)
 create mode 100644 src/Monad/Instance/K/EquationalLifting.lagda.md

diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md
index 8d48f54..93ed533 100644
--- a/src/Monad/Instance/K/Commutative.lagda.md
+++ b/src/Monad/Instance/K/Commutative.lagda.md
@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Category.Instance.AmbientCategory
 open import Monad.Commutative
diff --git a/src/Monad/Instance/K/EquationalLifting.lagda.md b/src/Monad/Instance/K/EquationalLifting.lagda.md
new file mode 100644
index 0000000..8e385d9
--- /dev/null
+++ b/src/Monad/Instance/K/EquationalLifting.lagda.md
@@ -0,0 +1,89 @@
+<!--
+```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
+  }
+```