You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I am in preparing presentations based on my previous work "Prototypes: Object-Orientation, Functionally" https://github.com/metareflection/poof and I'm looking for help to understand how best to formalize the optics involved in advanced OO constructs: nested or mutually recursive objects or classes, multimethods, method combinations, etc. — and maybe also to understand how the coinductive and potentially non-terminating aspects of the fixed-points involved in OO specifications can be reconciled with using them to describe inductive and definitely-terminating computations in dependent type theory.