[HN Gopher] Category Theory Illustrated - Types
___________________________________________________________________
Category Theory Illustrated - Types
Author : boris_m
Score : 87 points
Date : 2026-04-03 09:49 UTC (13 hours ago)
(HTM) web link (abuseofnotation.github.io)
(TXT) w3m dump (abuseofnotation.github.io)
| chromacity wrote:
| It's a great introduction, but I find the premise a bit funny. It
| starts with Russell's paradox, insinuates that solving it within
| set theory makes set theory complex (it doesn't, you basically
| just restrict what can be used to build a set), and then
| introduces a system that is _fundamentally more complex_.
| layer8 wrote:
| Regarding Russell's paradox, its dual is also interesting:
| Consider the set _D_ := { _s_ | _s_ [?] _s_ }, the set of sets
| that _do_ contain themselves. Does _D_ contain itself? It might
| or it might not, neither causes a contradiction. Tnis shows that
| you don't need an antinomy for a set comprehension to be ill-
| defined.
| xanderlewis wrote:
| Why is it ill-defined? As you said, there's no contradiction.
|
| Also, in the usual ZF set theory, it's empty.
| Koshkin wrote:
| ... and, as such, it doesn't contain itself!
| layer8 wrote:
| It's ill-defined in the sense that it doesn't uniquely define
| the set. There are at least two different sets that _D_ could
| be (one containing it and one not containing it), hence the
| expression doesn't denote a well-defined set. ( _)
|
| The axioms of ZF do not allow to form that expression, so the
| set doesn't exist in ZF.
|
| (_) This is from a universist view. In a pluralist view, one
| wouldn't say that the fact of the matter of whether _D_
| contains itself or not is independent from the naive set
| theory, and that there are set universes where it is the case
| and others where it isn't. But I would hold that naive set
| theory starts from a universist view.
| Koshkin wrote:
| > _a set can contain itself_
|
| Can it?
|
| > _a term can have only one type... Due to this law, types cannot
| contain themselves_
|
| Doesn't look like one follows from the other...
| bombcar wrote:
| The set of all sets that contain itself ;)
| Koshkin wrote:
| Except such set is empty and thus does _not_ contain itself.
| impact-basin wrote:
| I think you're taking this point a little too forcefully; this
| is meant to informally motivate Russell's paradox, in my
| reading - which is exactly the title of the section you're
| referencing.
|
| The point here is a little more subtle; category theory doesn't
| necessarily rely on sets; the definitions of categories that
| you often see (involving sets of objects and sets of morphisms)
| is more axiomatically forceful than the more general
| definition, which uses the notion of classes; category theory
| can use set theory, but does not depend on it.
|
| The point here is that type theory offers just such another way
| to design in an avoidance of Russell's paradox.
|
| You might also want to read about e.g. Grothendieck universes -
| they're quite relevant here.
| igravious wrote:
| _> > a set can contain itself_
|
| _> Can it?_
|
| Yes -- in set theory sets can contain themselves
|
| _> > a term can have only one type... Due to this law, types
| cannot contain themselves_
|
| _> Doesn 't look like one follows from the other..._
|
| types are not sets and sets are not types therefore it makes no
| sense to link these two statements/judgements in the way you
| are linking them
| igravious wrote:
| to justify my claim with an excerpt from the article:
|
| "" What is type theory "Every propositional
| function ph(x)--so it is contended--has, in addition to its
| range of truth, a range of significance, i.e. a range within
| which x must lie if ph(x) is to be a proposition at all,
| whether true or false. This is the first point in the theory
| of types; the second point is that ranges of significance
| form types, i.e. if x belongs to the range of significance of
| ph(x), then there is a class of objects, the type of x, all
| of which must also belong to the range of significance of
| ph(x)" -- Bertrand Russell - Principles of Mathematics
|
| In the last section, we almost fell in the trap of explaining
| types as something that are "like sets, but... " (e.g. they
| are like sets, but a term can only be a member of one type).
| However, while it may be technically true, any such
| explanation would not be at all appropriate, as, while types
| started as alternative to sets, they actually ended up being
| quite different. So, thinking in terms of sets won't get you
| far. Indeed, if we take the proverbial set theorist from the
| previous section, and ask them about types, their truthful
| response would have to be: "Have you seen a
| set? Well, it has nothing to do with it." [<=== important
| bit]
|
| So let's see how we define a type theory in its own right. ""
| mrkeen wrote:
| Oof. If sets and types aren't the same, then sets and
| barbers are _definitely_ not the same!
| denotational wrote:
| > Yes -- in set theory sets can contain themselves
|
| Which set theory? ZFC doesn't permit this.
|
| Non-well-founded set theories are so non-standard that I
| think it's wrong, or at least misleading, to claim that
| unqualified "set theory" permits this.
| mrkeen wrote:
| TFA is right. Parent comment is not really rebutting in any
| meaningful way. Your rebuttal makes less sense.
|
| >> "a term can have only one _type_... Due to this law,
| _types_ cannot contain themselves "
|
| > types are not sets and sets are not types therefore it
| makes no sense to link these two statements/judgements in the
| way you are linking them
| mrkeen wrote:
| The system works according to its defined rules.
|
| In one system, a set can contain itself, in another system it
| can't.
|
| So it doesn't really make sense to ask 'can it?'
|
| If you allow sets to contain themselves, you also have to talk
| about sets which do not contain themselves, which yields
| Russell's paradox.
|
| If you disallow sets (or types) from containing themselves then
| you can't construct Russell's paradox, which is why it follows.
___________________________________________________________________
(page generated 2026-04-03 23:01 UTC)