6 Jan
2010
6 Jan
'10
9:30 p.m.
Peter Selinger wrote:
I don't know enough about FOLDS to have an intuition whether any non-evil (1) structure can be expressed in it. Does FOLDS, for example, allow constructions that are not equational? Like categories satisfying fg = 1 => gf = 1? I am pretty sure that's non-evil (1).
Yes, that should be fine in FOLDS. The "FOL" in FOLDS is First-Order Logic, which includes implication, quantification, etc. Actually, Makkai's formulation of FOLDS doesn't include any operations, only relations (with operations modeled by functional relations), but I think operations can be added easily (as they are in full DTT). Mike