4 ms·
But don't most dependent type theories have a restrictive notion of equality (e.g. without extensional equality of functions) making many things that we would l
by creata 6y ago
But don't most dependent type theories have a restrictive notion of equality (e.g. without extensional equality of functions) making many things that we would like to be monoids not fit that definition? Anyway, I agree with your general point: dependent types are extremely simple, and make so many things more elegant (type-safe printf is the common example) that I'm surprised they aren't more popular.
- siraben 6y agoHm yes. For instance the monoid of endofunctions on S would require one to prove that f . id = id . f = f. In vanilla dependent types this needs the extensionality axiom added, but in category theory it definitely is fine to speak of equality between morphisms with the same source and target.