What is a subset?

[marcbezem]

In 2.13, a subset is defined as Σ (x:A) P(x), for a set A and P: A->Prop. In 2.18, the P is called subset. In 2.13, a P: T -> Prop is called (by me) a predicate on T. I seem to be the only one using the terminology "predicate". I like it, but we could decide otherwise.

A disadvantage of calling P a subset is that one needs an additional definition of an element of a subset.

The choice of terminology has some consequences for how one presents, given a mono f : Hom(G,H), the underlying set of G as a subset of the underlying set of H.

[UlrikBuchholtz]

Well, a subset is the pair of the Σ-type and the inclusion. I added a footnote for now (in e983fca), but feel free to rephrase the definition. Lemma 2.22.4(a) (lem:Prop-Set-pointed-families) provides the equivalence between subsets and predicates.

[bidundas]

This is beyond my jurisdiction, I know. However, I still offer my opinion.

The question is ”what should the type of subsets of the set A be?”

1. the type of injections into A
2. the set of families of propositions on A

To the categorical me, ”the set of subsets of A" is a very special skeleton of the ”groupoid of injections into A” which is isomorphic to "the set of characteristic functions A->{0,1}”.
Hence, I’d say that 2 is closer to my feeling for a subset than 1, whereas 2 is the bigger groupoid of injections (which happens to have a set as a skeleton).

Bjorn

PS I agonized over this for subgroups, and landed on this solution (”monomorphism into" vs ”subgroup of” - the latter being pointed transitive G-sets.). I accumulated a lot of reasons for this, so please don’t force me to change it.

On May 23, 2020, at 19:32, Marc Bezem notifications@github.com wrote:

In 2.13, a subset is defined as Σ (x:A) P(x), for a set A and P: A->Prop. In 2.18, the P is called subset. In 2.13, a P: T -> Prop is called (by me) a predicate on T. I seem to be the only one using the terminology "predicate". I like it, but we could decide otherwise.

A disadvantage of calling P a subset is that one needs an additional definition of an element of a subset.

The choice of terminology has some consequences for how one presents, given a mono f : Hom(G,H), the underlying set of G as a subset of the underlying set of H.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[UlrikBuchholtz]

Well, the groupoid of types with an injection into A is a set, and is already equivalent/isomorphic to the set of characteristic functions A→Prop.

(Here, I'll pretend I don't know what a skeleton is.)

[bidundas]

Pretending that you don’t know what a skeleton is can ruin these things...

The argument is that when choosing between equivalent types modelling a categorical notion one would prefer the one modelling an isomorphic category, not an equivalent one.

Bjorn

On May 23, 2020, at 20:00, Ulrik Buchholtz notifications@github.com wrote:

Well, the groupoid of types with an injection into A is a set, and is already equivalent/isomorphic to the set of characteristic functions A→Prop.

(Here, I'll pretend I don't know what a skeleton is.)

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe.

[DanGrayson]

Have you interchanged 1 & 2 below?

A subset needs to have elements, so it needs to be a type. I also very much like the type of injections into A, but by providing a coercion we can arrange for an injection into A to have elements. Demanding that a subset always be constructed from a predicate seems to be too much, for classically, one normally constructs the characteristic function from the subset.

On Sat, May 23, 2020 at 12:51 PM Bjorn Ian Dundas notifications@github.com wrote:

This is beyond my jurisdiction, I know. However, I still offer my opinion.

The question is ”what should the type of subsets of the set A be?”

1. the type of injections into A
2. the set of families of propositions on A

To the categorical me, ”the set of subsets of A" is a very special skeleton of the ”groupoid of injections into A” which is isomorphic to "the set of characteristic functions A->{0,1}”. Hence, I’d say that 2 is closer to my feeling for a subset than 1, whereas 2 is the bigger groupoid of injections (which happens to have a set as a skeleton).

Bjorn

PS I agonized over this for subgroups, and landed on this solution (”monomorphism into" vs ”subgroup of” - the latter being pointed transitive G-sets.). I accumulated a lot of reasons for this, so please don’t force me to change it.

On May 23, 2020, at 19:32, Marc Bezem notifications@github.com wrote:

In 2.13, a subset is defined as Σ (x:A) P(x), for a set A and P: A->Prop. In 2.18, the P is called subset. In 2.13, a P: T -> Prop is called (by me) a predicate on T. I seem to be the only one using the terminology "predicate". I like it, but we could decide otherwise.

A disadvantage of calling P a subset is that one needs an additional definition of an element of a subset.

The choice of terminology has some consequences for how one presents, given a mono f : Hom(G,H), the underlying set of G as a subset of the underlying set of H.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/UniMath/SymmetryBook/issues/73#issuecomment-633105291, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFK6RHPZOQ6C243IRW7T43RTAEL5ANCNFSM4NIQ7B2Q .

[UlrikBuchholtz]

Pretending that you don’t know what a skeleton is can ruin these things... The argument is that when choosing between equivalent types modelling a categorical notion one would prefer the one modelling an isomorphic category, not an equivalent one.

Well, here the point is rather that our framework doesn't even know what a skeletal set is: every set is a homotopy set, and we have no notion of a strict set. (In a two-level type theory, one could introduce this, but it's not a mathematical notion.)

[bidundas]

I

On May 23, 2020, at 20:38, Ulrik Buchholtz notifications@github.com wrote:

Pretending that you don’t know what a skeleton is can ruin these things... The argument is that when choosing between equivalent types modelling a categorical notion one would prefer the one modelling an isomorphic category, not an equivalent one.

Well, here the point is rather that our framework doesn't even know what a skeletal set is: every set is a homotopy set, and we have no notion of a strict set. (In a two-level type theory, one could introduce this, but it's not a mathematical notion.)

This is not about mathematics, this is about words. Even in a univalent universe we do tend to have different names for differently constructed types, also when they are equivalent.

I've promised myself not to fight these fights - I seem to forget - sorry.

Bjorn

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe.

[UlrikBuchholtz]

This is not about mathematics, this is about words. Even in a univalent universe we do tend to have different names for differently constructed types, also when they are equivalent.

Very much agreed on the latter point.

So are we then agreed that a “subset” of A is a type together with an injection into A, while a “predicate” on A is a function from A to Prop? (Or a function from A to the universe that factors through Prop; these are also not definitionally the same.)

This can be explicated around the current Def. 2.13.1 (def:subtype), with a forward reference to Sec. 2.22, where the equivalence is established.

[DanGrayson]

I like those choices.

On Sat, May 23, 2020, 2:42 PM Ulrik Buchholtz notifications@github.com wrote:

This is not about mathematics, this is about words. Even in a univalent universe we do tend to have different names for differently constructed types, also when they are equivalent.

Very much agreed on the latter point.

So are we then agreed that a “subset” of A is a type together with an injection into A, while a “predicate” on A is a function from A to Prop? (Or a function from A to the universe that factors through Prop; these are also not definitionally the same.)

This can be explicated around the current Def. 2.13.1 (def:subtype), with a forward reference to Sec. 2.22, where the equivalence is established.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/UniMath/SymmetryBook/issues/73#issuecomment-633125485, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFK6RB7M67QZSZ4B3KRBATRTARITANCNFSM4NIQ7B2Q .

[marcbezem]

I agree, including the forward reference to 2.22.

[UlrikBuchholtz]

OK, I will implement this as described above.

[UlrikBuchholtz]

The definition of injection should be moved to this section too.

[UlrikBuchholtz]

This is now implemented in 94e489e. However, it now necessitates some rewriting in Sec. 2.23 (sec:typefam), so I'm leaving the issue open for this.

[UlrikBuchholtz]

I see this issue is still open, which is apropos of today's discussion. Currently, we say after Cor. 2.19.7 that { t : T | P(t) } is a subset. This is in particular a subtype, hence should be considered foremost as an element of Sub_T, as in Def. 2.19.5, with a coercion to sets/types. Could this be explained more clearly? I find the \setof notation very useful, because we often don't have to give a name to the predicate P. (Perhaps we should more often!?) (We also discussed allowing this notation for general subtypes…)

BTW, we should define \subseteq in Ch. 2! I don't know how much we want to make of this—there's lots to say, but the definition would be a minimum.

[DanGrayson]

I see this issue is still open.

Let's use the \setof notation not just for sets, as Ulrik proposes. (If no one disagrees, I'll also clarify the sentence.)

I noticed this:

The phrase "ordinary sets" might be misunderstood, especially since we don't want to assume traditional set theory as a prerequisite for this book. Maybe by something like this: "In a certain sense, a predicate on T can be recovered from the collection of elements of T for which the predicate is true, and focusing on that collection can be more intuitive. We develop this idea as follows."

A universe is introduced here without comment:

The alert student will wonder whether the notion of "subtype" really depends on that. What should we say about that? Do we really want to get into propositional resizing?

Perhaps we should put "yes" and "no" in a different font:

[marcbezem]

Re Def. 2.19.5, I think the "default" U would be the U in which the type T lives.

[UlrikBuchholtz]

Re “In ordinary sets”, I like your re-phrasing, Dan, also without the “In a certain sense”.

Re Def. 2.19.5, it's simple if we assume propositional resizing, so we can mention (in the margin), that if we have that then T's universe suffices, otherwise we might have to consider larger universes V, also corresponding to the universes of propositions when we consider a subtype of T as a predicate P : T -> Prop_V.

I think, for clarity, we should introduce Sub_T^U in Def. 2.19.5 and then write that we'll often write just Sub_T, leaving the choice of universe ambiguous.

[UlrikBuchholtz]

Re fonts/names of elements of Bool: Hm, maybe blackboard bold y and n? (However, this clashes a bit with our current convention, which I'm still a little uneasy about, of using blackboard bold n to denote the standard n-element set when n is a variable of type Nat.)

I'm a bit(!) loathe to introduce new fonts. If we want to keep yes and no, maybe small caps would be good:

[DanGrayson]

" our current convention, which I'm still a little uneasy about, of using blackboard bold n to denote the standard n-element set"

I agree -- let's not use font changes on variable names to signify mathematical operations.