add kleisli triple #381
add kleisli triple #381
Conversation
| -- see https://ncatlab.org/nlab/show/extension+system (the naming differs) | ||
|
|
||
| open import Level | ||
| open import Categories.Category |
There was a problem hiding this comment.
Can you please use Categories.Category.Core (unless you really need more) and also using clauses and and for all open import below.
| open MR C | ||
|
|
||
| -- a kleisli triple is a relative monad with J = idF | ||
| Kleisli : Set (o ⊔ ℓ ⊔ e) |
There was a problem hiding this comment.
I'm wondering if the type should be called KleisliTriple as there are too many Kleisli things already? (The implication below can keep its name)
There was a problem hiding this comment.
As a slightly polemic point, nLab seems to promote the name "extension system" https://ncatlab.org/nlab/show/extension+system. I am more used to the name "Kleisli triple", but nLab may well change the trend. I do not really have any opinion on this.
There was a problem hiding this comment.
I would be fine with either KleisliTriple or ExtensionSystem.
There was a problem hiding this comment.
I chose KleisliTriple and KleisliCotriple for now.
| module η = NaturalTransformation η | ||
|
|
||
| assoc' : ∀ {X : Obj} → μ.η X ∘ F₁ (μ.η X) ≈ μ.η X ∘ μ.η (F₀ X) | ||
| assoc' = begin |
There was a problem hiding this comment.
This is the exact same proof as commute above -- factor out please.
There was a problem hiding this comment.
Done, I wasn't sure about the naming, so i just named it commute' and added a comment.
| μ = ntHelper {F = F ∘F F} {G = F} record | ||
| { η = λ X → extend id | ||
| ; commute = λ f → begin | ||
| extend id ∘ extend (unit ∘ extend (unit ∘ f)) ≈⟨ sym K.assoc ⟩ |
There was a problem hiding this comment.
This repeated use of sym K.assoc makes me think that RelativeMonad should be extended to have sym-assoc in its API (this is optional, but would be nice).
There was a problem hiding this comment.
Changed it for RelativeMonad and RelativeComonad and also fixed places where its used.
| identityʳ' : ∀ {X Y} {k : X ⇒ F₀ Y} → (μ.η Y ∘ F₁ k) ∘ η.η X ≈ k | ||
| identityʳ' {X} {Y} {k} = begin | ||
| ((μ.η Y ∘ F₁ k) ∘ η.η X) ≈⟨ pullʳ (sym (η.commute _)) ⟩ | ||
| (μ.η Y ∘ η.η (F₀ Y) ∘ k) ≈⟨ pullˡ M.identityʳ ⟩ |
There was a problem hiding this comment.
cancelˡ M.identityʳ should cut out 1 line.
|
Thanks for the feedback! I've also added |
Small proof that kleisli triples are equivalent to monads. I'm looking for some feedback and then I'd do the same for comonads.
I've defined the kleisli-triple as a typedef for
RMonad idFto avoid redundancy, but this might make things a little unclear.