Conversation
Notes: Defintion is "manual", i.e. not via lifting. To allow this we needed to factor out some definitions. For Algebras (for Coalgebras equivalently): F-Algebra -> F-Algebra-on F-Algebra-Morphism -> is-F-Algebra-Morphism Further notes: • We did _not_ define "just" (T,F)-Bialgebras as without a distributive law μ to relate them there is not much structure. • For us μ is just a nat trans (T∘F)⇒(F∘T), so not the notion of a distributive law in a monadic context.
A Functor F : C → C can be lifted to F' : Alg(T) → Alg(T) given T and a distributive law μ for T∘F.
Have lots of intermediate terms foo_i, bar_i here. This is akin to Coq code riddled with `Check`s.
|
We don't currently have any modules with a non-ascii character in the name. Is it OK to add one in this case? |
|
Good point. I think that's asking for trouble, we shouldn't have file names with unicode in them. Internal modules is fine, but not "file-modules". |
Metavariable resolution needs to be fixed for `F-resp-≈` in proof. Proofs currently still contain scaffolding. Contains `coLambek`.
* ∘ defined as ∘ in coF-Algebras
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Sorry to be so picky (and slow). This is a very nice piece of work! Might as well really polish it up.
Added anonymous module which meant having to indent all previous code – not ideal, but oh well. First step in Bialg(μ,F,T)≅Coalgs(LiftAlgs(F))≅Algs(LiftCoalgs(T))
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
This is looking really good. Is it "ready"?
Almost! I'm currently implementing a final interesting lemma, that initial objects in T-Algs induce initial objs in μ-F-T-Bialgebras (dually, final F-Coalgs are also final in μ-F-T-Bialgebras). I also replied to some of your review comments with questions |
|
(link to personal Trello board deleted - it was misconfigured, and wasn't supposed to post on here) |
this because we need to open a different `Category` module for the final proof
This before adding `lift(Initial|Terminal)`
Needed to redo the definition of `LiftCoalgebras`, to use conversion functions to transport only the _proofs_ from `LiftAlgebras`
Also x-ref documentation comment across modules
|
I added some last nice things to round off this MR (see commit descriptions). After review everything should be ready to merge! |
|
Thanks - at POPL right now, so might not get to do the review until I'm back home. We'll see. |
yes, I saw on Mastodon. No rush! |
3 participants
I've defined bialgebras for functors. I needed to factor out some definitions in
AlgebraandCoalgebra, but the changes don't break any existing code. For more details see the commit message of f8a6027