Skip to main content
incorporated Simon Henry’s comment
Source Link

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition for instance here, in the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass notesand Simon Henry note in comments, if we’re working in a type-theoretic or structural set-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in most type-theoretic approachesstructural foundations, abstract sets are taken to be (certain) types, not assumed to beautomatically subsets of anyan ambient universal class.)

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition for instance here, in the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass notes in comments, if we’re working in a type-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in most type-theoretic approaches, abstract sets are taken to be (certain) types, not assumed to be subsets of any ambient universal class.)

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition for instance here, in the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass and Simon Henry note in comments, if we’re working in a type-theoretic or structural set-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in structural foundations, abstract sets not automatically subsets of an ambient universal class.)

added reference to formalisation of comparison between defs of cats; and added remark re Blass’s comment
Source Link

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This approach is made precise in computer formalisations in proof assistants, where functions have implicit arguments.This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition — I’m slightly hurried nowfor instance here, but can dig up a link/reference laterin the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass notes in comments, if we’re working in a type-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in most type-theoretic approaches, abstract sets are taken to be (certain) types, not assumed to be subsets of any ambient universal class.)

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This approach is made precise in computer formalisations in proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself) and shown equivalent to the class-of-arrows definition — I’m slightly hurried now, but can dig up a link/reference later. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition for instance here, in the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass notes in comments, if we’re working in a type-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in most type-theoretic approaches, abstract sets are taken to be (certain) types, not assumed to be subsets of any ambient universal class.)

brought the groups analogy back to the original example of composition
Source Link

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This approach is made precise in computer formalisations in proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself) and shown equivalent to the class-of-arrows definition — I’m slightly hurried now, but can dig up a link/reference later. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do notnot think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with having the original hom-sets be sub-objectsbeing sub-objects of it rather than literal set-theoretic subsets.)

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation.

This approach is made precise in computer formalisations in proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself) and shown equivalent to the class-of-arrows definition — I’m slightly hurried now, but can dig up a link/reference later. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with having the original hom-sets be sub-objects of it rather than literal set-theoretic subsets.)

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This approach is made precise in computer formalisations in proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself) and shown equivalent to the class-of-arrows definition — I’m slightly hurried now, but can dig up a link/reference later. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

Source Link
Loading