Conversation
… renaming; use projections instead
…ning provided by Bicat
| @@ -0,0 +1,99 @@ | |||
| {-# OPTIONS --without-K --safe --lossy-unification #-} | |||
There was a problem hiding this comment.
is --lossy-unification (still) crucial?
| actionˡ : F ∘₁ T M₁ ⇒₂ F | ||
| actionʳ : T M₂ ∘₁ F ⇒₂ F | ||
|
|
||
| assoc : actionʳ ∘ᵥ (T M₂ ▷ actionˡ) ∘ᵥ associator.from ≈ actionˡ ∘ᵥ (actionʳ ◁ T M₁) |
There was a problem hiding this comment.
Since you use Extras you might as well use Shorthands too.
| actionʳ : T M₂ ∘₁ F ⇒₂ F | ||
|
|
||
| assoc : actionʳ ∘ᵥ (T M₂ ▷ actionˡ) ∘ᵥ associator.from ≈ actionˡ ∘ᵥ (actionʳ ◁ T M₁) | ||
| sym-assoc : actionˡ ∘ᵥ (actionʳ ◁ T M₁) ∘ᵥ associator.to ≈ actionʳ ∘ᵥ (T M₂ ▷ actionˡ) |
There was a problem hiding this comment.
Since you use this version that is "definitionally symmetric", it might be useful to have a BimoduleHelper that lets users elide the items that are derivable.
| where | ||
| open Monad M | ||
|
|
||
| record Bimodulehomomorphism {M₁ M₂ : Monad 𝒞} (B₁ B₂ : Bimodule M₁ M₂) : Set (ℓ ⊔ e) where |
There was a problem hiding this comment.
I know that for smaller things, the objects and morphisms are all defined in the same file, but I think that for Bimodule, it would make sense to split this into Bimodule/Homomorphism.agda. It could also help make typechecking faster.
| → Bimodulehomomorphism B₂ B₃ → Bimodulehomomorphism B₁ B₂ → Bimodulehomomorphism B₁ B₃ | ||
| bimodule-hom-∘ {M₁} {M₂} {B₁} {B₂} {B₃} g f = record | ||
| { α = α g ∘ᵥ α f | ||
| ; linearˡ = begin |
There was a problem hiding this comment.
Please move both of these proofs to the where clause. Having these inline will cause a lot of noise in downstream use, as Agda is too eager to eta-expand.
| { α = α g ∘ᵥ α f | ||
| ; linearˡ = begin | ||
| actionˡ B₃ ∘ᵥ (α g ∘ᵥ α f) ◁ T M₁ ≈⟨ refl⟩∘⟨ ⟺ ∘ᵥ-distr-◁ ⟩ | ||
| actionˡ B₃ ∘ᵥ (α g ◁ T M₁) ∘ᵥ (α f ◁ T M₁) ≈⟨ sym-assoc₂ ⟩ |
There was a problem hiding this comment.
for a future PR: this sure looks like bicategorical versions of push and pull. Should be abstracted out!
There was a problem hiding this comment.
What is the recommended way to get push and pull into scope?
There was a problem hiding this comment.
import Categories.Morphism.Reasoning as MR
open MR Cwhere C is the 1-category of interest. Is the 'vertical' category clearly visible here?
My comment here is that there should be a Category.Bicategory.Reasoning that serves the same purpose. Right now, there is a bunch of stuff in Category.Bicategory.Extras that probably belongs in such a (new) module.
There was a problem hiding this comment.
There is a private module MR' defined in Category.Bicategory.Extras. Do you want this but public?
There was a problem hiding this comment.
Something like that, yes.
…e of each associativity law and have the symmetric one derived
|
This is ready for re-review. |
2 participants
This pull request defines bimodules between monads and bimodulehomomorphisms (cf. Shulman - Framed Bicategories and Monoidal Fibrations, Ch. 11). This is part of a larger project constructing a bicategory of monads and bimodules.