1lab icon indicating copy to clipboard operation
1lab copied to clipboard

F-algebras, F-colgebras, and F-dialgebras as pullbacks of `Comma`

Open TOTBWF opened this issue 4 months ago • 0 comments

Right now, we define F-Algebras : Displayed C ℓ ℓ by hand. However, we could also define it as Change-of-base Cat⟨ Id , Id ⟩ (Comma F Id), which would get us a lot of things for free. A similar trick should work for F-coalgebras and F-dialgebras.

TOTBWF avatar Aug 22 '25 16:08 TOTBWF