1lab
1lab copied to clipboard
F-algebras, F-colgebras, and F-dialgebras as pullbacks of `Comma`
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.