- cyclic proofs are not scary — decidable in mu-calculus
- mu on the left and nu on the right — dualization
- makes me wonder what is the interpretation of recursive types
- inductive types, recursive types, interpreted co-inductively
- question: do negative recursive types correspond to algebra?
- monads on effects? algebra on datatypes?