Why doesn't the definition of a category require an explicit notion of moprhisms equality?












2














I am learning basics of the category theory (CT).



I do understand that CT is a modern powerful framework to describe various branches of mathematics in a unified way.



I do admit that category's definition tells a lot about the whole thing and focuses on the most important properties, shadowing unnecessary details. However, the more I go forward, the more it feels like it should explicitly require a notion of morphisms equality (like it does with morphism composition). It feels so because equality or inequality of morphisms arises everywhere, since the very beginning: any commutative diagram eventually reduces to an equality of two different paths and many other things involve equality as well. Even composition is defined grouding upon an (implicit) equality!



I'll try to give an example of my concern. Consider $mathbb{SET}$. Its objects are sets and morphisms are functions. Now, let's recall that functions are sets as well - to be more precise, a function $f : A mapsto B$ is a subset of a $A times B$ obeying certain properties, which I omit. Thus, one could argue that $f$ is both a morphism between objects $A, B in Obj(mathbb{SET})$ and an object defined as a set of pairs ${ (a_1 in A, b_1 in B), ..., (a_n in A, b_n in B) }$ and those are equal because both are essentially exactly the same thing.



I hope my concern is clear and I need some kind of "conceptual insight" from knowledgeable people to move forward. Please give me the right perspective.










share|cite|improve this question
























  • Re "grouding": Do you mean "grounding"?
    – Peter Mortensen
    2 hours ago










  • Functions are not sets. Functions can be modeled as sets (in more than one canonical way). It can be a good idea to do so when you are only talking about sets (as is the case when defining a set theory).
    – Eric Towers
    5 mins ago
















2














I am learning basics of the category theory (CT).



I do understand that CT is a modern powerful framework to describe various branches of mathematics in a unified way.



I do admit that category's definition tells a lot about the whole thing and focuses on the most important properties, shadowing unnecessary details. However, the more I go forward, the more it feels like it should explicitly require a notion of morphisms equality (like it does with morphism composition). It feels so because equality or inequality of morphisms arises everywhere, since the very beginning: any commutative diagram eventually reduces to an equality of two different paths and many other things involve equality as well. Even composition is defined grouding upon an (implicit) equality!



I'll try to give an example of my concern. Consider $mathbb{SET}$. Its objects are sets and morphisms are functions. Now, let's recall that functions are sets as well - to be more precise, a function $f : A mapsto B$ is a subset of a $A times B$ obeying certain properties, which I omit. Thus, one could argue that $f$ is both a morphism between objects $A, B in Obj(mathbb{SET})$ and an object defined as a set of pairs ${ (a_1 in A, b_1 in B), ..., (a_n in A, b_n in B) }$ and those are equal because both are essentially exactly the same thing.



I hope my concern is clear and I need some kind of "conceptual insight" from knowledgeable people to move forward. Please give me the right perspective.










share|cite|improve this question
























  • Re "grouding": Do you mean "grounding"?
    – Peter Mortensen
    2 hours ago










  • Functions are not sets. Functions can be modeled as sets (in more than one canonical way). It can be a good idea to do so when you are only talking about sets (as is the case when defining a set theory).
    – Eric Towers
    5 mins ago














2












2








2


1





I am learning basics of the category theory (CT).



I do understand that CT is a modern powerful framework to describe various branches of mathematics in a unified way.



I do admit that category's definition tells a lot about the whole thing and focuses on the most important properties, shadowing unnecessary details. However, the more I go forward, the more it feels like it should explicitly require a notion of morphisms equality (like it does with morphism composition). It feels so because equality or inequality of morphisms arises everywhere, since the very beginning: any commutative diagram eventually reduces to an equality of two different paths and many other things involve equality as well. Even composition is defined grouding upon an (implicit) equality!



I'll try to give an example of my concern. Consider $mathbb{SET}$. Its objects are sets and morphisms are functions. Now, let's recall that functions are sets as well - to be more precise, a function $f : A mapsto B$ is a subset of a $A times B$ obeying certain properties, which I omit. Thus, one could argue that $f$ is both a morphism between objects $A, B in Obj(mathbb{SET})$ and an object defined as a set of pairs ${ (a_1 in A, b_1 in B), ..., (a_n in A, b_n in B) }$ and those are equal because both are essentially exactly the same thing.



I hope my concern is clear and I need some kind of "conceptual insight" from knowledgeable people to move forward. Please give me the right perspective.










share|cite|improve this question















I am learning basics of the category theory (CT).



I do understand that CT is a modern powerful framework to describe various branches of mathematics in a unified way.



I do admit that category's definition tells a lot about the whole thing and focuses on the most important properties, shadowing unnecessary details. However, the more I go forward, the more it feels like it should explicitly require a notion of morphisms equality (like it does with morphism composition). It feels so because equality or inequality of morphisms arises everywhere, since the very beginning: any commutative diagram eventually reduces to an equality of two different paths and many other things involve equality as well. Even composition is defined grouding upon an (implicit) equality!



I'll try to give an example of my concern. Consider $mathbb{SET}$. Its objects are sets and morphisms are functions. Now, let's recall that functions are sets as well - to be more precise, a function $f : A mapsto B$ is a subset of a $A times B$ obeying certain properties, which I omit. Thus, one could argue that $f$ is both a morphism between objects $A, B in Obj(mathbb{SET})$ and an object defined as a set of pairs ${ (a_1 in A, b_1 in B), ..., (a_n in A, b_n in B) }$ and those are equal because both are essentially exactly the same thing.



I hope my concern is clear and I need some kind of "conceptual insight" from knowledgeable people to move forward. Please give me the right perspective.







soft-question category-theory definition






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited 48 mins ago









Peter Mortensen

545310




545310










asked 7 hours ago









Sereja Bogolubov

551111




551111












  • Re "grouding": Do you mean "grounding"?
    – Peter Mortensen
    2 hours ago










  • Functions are not sets. Functions can be modeled as sets (in more than one canonical way). It can be a good idea to do so when you are only talking about sets (as is the case when defining a set theory).
    – Eric Towers
    5 mins ago


















  • Re "grouding": Do you mean "grounding"?
    – Peter Mortensen
    2 hours ago










  • Functions are not sets. Functions can be modeled as sets (in more than one canonical way). It can be a good idea to do so when you are only talking about sets (as is the case when defining a set theory).
    – Eric Towers
    5 mins ago
















Re "grouding": Do you mean "grounding"?
– Peter Mortensen
2 hours ago




Re "grouding": Do you mean "grounding"?
– Peter Mortensen
2 hours ago












Functions are not sets. Functions can be modeled as sets (in more than one canonical way). It can be a good idea to do so when you are only talking about sets (as is the case when defining a set theory).
– Eric Towers
5 mins ago




Functions are not sets. Functions can be modeled as sets (in more than one canonical way). It can be a good idea to do so when you are only talking about sets (as is the case when defining a set theory).
– Eric Towers
5 mins ago










3 Answers
3






active

oldest

votes


















7














Morphism equality is indeed taken as primitive, but at an "even more primitive" level than composition.



Remember - ignoring set/class issues for the moment - composition consists of a partial function assigning to a pair of morphisms (on which it's defined) a third morphism, which we call their composition. So equality between morphisms is folded into the very nature of sets themselves (in this case, the sets of morphisms).



If you're familiar with model theory, equality is part of the logical language - on the same level as the quantifiers and Boolean connectives - while compositionof morphisms would be part of the signature (or language, or vocabulary, or ...), similarly to the symbol for the group operation in the context of groups.



Your second-to-last paragraph, though, is more special. The phenomenon you're describing there is actually something category theory explicitly doesn't want to pay attention to, at least most of the time, since one of the big points is that we can forget what the objects are and just look at how the morphisms behave. Certainly there's no object/morphism relation in general categories - for example, think about a group viewed as a one-object category.






share|cite|improve this answer





























    6














    Category theory is ordinarily formulated within the framework of axiomatic set theory, just like the rest of mathematics. Axiomatic set theory includes equality as a primitive notion. So there is no need to separately specify equality as part of a category--you already know what equality means from your background foundation of mathematics. There is nothing special about category theory in this respect; this is just like how when defining a group, you don't have to specify what it means for two elements of the group to be equal, for instance.



    Yes, the underlying notion of equality may include equalities that you don't want, such as a morphism being equal to an object. But this is not actually a problem at all--you will never talk about morphisms being equal to objects, so you don't care whether they are. Note in particular that an isomorphism between categories does not need to preserve such equalities.



    (That said, there is some interest in alternate foundations of mathematics that are more strongly "typed", so that you can't talk about equalities of things that shouldn't "make sense". See for instance https://ncatlab.org/nlab/show/structural+set+theory. Again, though, this is in no way specific to category theory, nor is it at all logically necessary for the development of mathematics.)






    share|cite|improve this answer































      2














      As the other answers state, for typical, set-theoretic foundations, a global notion of equality is always available. There is thus no need to explicitly provide a notion of equality, and it is always possible to ask whether two mathematical objects (i.e. sets) are equal. Functions, i.e. arrows of $mathbf{Set}$, are sets and so are also objects of $mathbf{Set}$. The function qua an object isn't "essentially exactly the same" as the function qua an arrow. They are exactly the same thing, no "essentially" about it.1



      However, this is not desirable for category theory. Ideally, you'd use a logical framework in which the principle of equivalence held. The principle of equivalence states that everything you state should be isomorphism invariant. Makkai developed FOLDS explicitly to provide such a logical framework. The slightly more usable Dependent FOL (DFOL) also accomplishes this goal as well. This is also typically accomplished by formalizations in dependent type theories such as the Calculus of (Inductive) Constructions. As I illustrate in this answer, formalizing the notion of category in DFOL would explicitly provide a (family of) notion(s) of equality for morphism. (And, notably, not provide a notion of equality for objects.)



      Within traditional set-theoretic foundations, if you wanted to be more explicit about notions of equality, you could work in a setoid-enriched version of category theory. You would provide a (family of) setoid(s) of arrows2 This would require composition to respect the setoid structure of its inputs. This would then impact the definition of things like functors.



      1 Technically, we would probably add the codomain (at least) to the notion of arrow for $mathbf{Set}$ since hom-sets are usually defined to be disjoint in set-theoretic foundations. The resulting arrow is still a set, though, so that doesn't really change the story.



      2 Indeed, a (set-theoretic) model of the DFOL theory I sketch in the other answer would have arrows be a family of setoids.






      share|cite|improve this answer





















        Your Answer





        StackExchange.ifUsing("editor", function () {
        return StackExchange.using("mathjaxEditing", function () {
        StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
        StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
        });
        });
        }, "mathjax-editing");

        StackExchange.ready(function() {
        var channelOptions = {
        tags: "".split(" "),
        id: "69"
        };
        initTagRenderer("".split(" "), "".split(" "), channelOptions);

        StackExchange.using("externalEditor", function() {
        // Have to fire editor after snippets, if snippets enabled
        if (StackExchange.settings.snippets.snippetsEnabled) {
        StackExchange.using("snippets", function() {
        createEditor();
        });
        }
        else {
        createEditor();
        }
        });

        function createEditor() {
        StackExchange.prepareEditor({
        heartbeatType: 'answer',
        autoActivateHeartbeat: false,
        convertImagesToLinks: true,
        noModals: true,
        showLowRepImageUploadWarning: true,
        reputationToPostImages: 10,
        bindNavPrevention: true,
        postfix: "",
        imageUploader: {
        brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
        contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
        allowUrls: true
        },
        noCode: true, onDemand: true,
        discardSelector: ".discard-answer"
        ,immediatelyShowMarkdownHelp:true
        });


        }
        });














        draft saved

        draft discarded


















        StackExchange.ready(
        function () {
        StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3054271%2fwhy-doesnt-the-definition-of-a-category-require-an-explicit-notion-of-moprhisms%23new-answer', 'question_page');
        }
        );

        Post as a guest















        Required, but never shown

























        3 Answers
        3






        active

        oldest

        votes








        3 Answers
        3






        active

        oldest

        votes









        active

        oldest

        votes






        active

        oldest

        votes









        7














        Morphism equality is indeed taken as primitive, but at an "even more primitive" level than composition.



        Remember - ignoring set/class issues for the moment - composition consists of a partial function assigning to a pair of morphisms (on which it's defined) a third morphism, which we call their composition. So equality between morphisms is folded into the very nature of sets themselves (in this case, the sets of morphisms).



        If you're familiar with model theory, equality is part of the logical language - on the same level as the quantifiers and Boolean connectives - while compositionof morphisms would be part of the signature (or language, or vocabulary, or ...), similarly to the symbol for the group operation in the context of groups.



        Your second-to-last paragraph, though, is more special. The phenomenon you're describing there is actually something category theory explicitly doesn't want to pay attention to, at least most of the time, since one of the big points is that we can forget what the objects are and just look at how the morphisms behave. Certainly there's no object/morphism relation in general categories - for example, think about a group viewed as a one-object category.






        share|cite|improve this answer


























          7














          Morphism equality is indeed taken as primitive, but at an "even more primitive" level than composition.



          Remember - ignoring set/class issues for the moment - composition consists of a partial function assigning to a pair of morphisms (on which it's defined) a third morphism, which we call their composition. So equality between morphisms is folded into the very nature of sets themselves (in this case, the sets of morphisms).



          If you're familiar with model theory, equality is part of the logical language - on the same level as the quantifiers and Boolean connectives - while compositionof morphisms would be part of the signature (or language, or vocabulary, or ...), similarly to the symbol for the group operation in the context of groups.



          Your second-to-last paragraph, though, is more special. The phenomenon you're describing there is actually something category theory explicitly doesn't want to pay attention to, at least most of the time, since one of the big points is that we can forget what the objects are and just look at how the morphisms behave. Certainly there's no object/morphism relation in general categories - for example, think about a group viewed as a one-object category.






          share|cite|improve this answer
























            7












            7








            7






            Morphism equality is indeed taken as primitive, but at an "even more primitive" level than composition.



            Remember - ignoring set/class issues for the moment - composition consists of a partial function assigning to a pair of morphisms (on which it's defined) a third morphism, which we call their composition. So equality between morphisms is folded into the very nature of sets themselves (in this case, the sets of morphisms).



            If you're familiar with model theory, equality is part of the logical language - on the same level as the quantifiers and Boolean connectives - while compositionof morphisms would be part of the signature (or language, or vocabulary, or ...), similarly to the symbol for the group operation in the context of groups.



            Your second-to-last paragraph, though, is more special. The phenomenon you're describing there is actually something category theory explicitly doesn't want to pay attention to, at least most of the time, since one of the big points is that we can forget what the objects are and just look at how the morphisms behave. Certainly there's no object/morphism relation in general categories - for example, think about a group viewed as a one-object category.






            share|cite|improve this answer












            Morphism equality is indeed taken as primitive, but at an "even more primitive" level than composition.



            Remember - ignoring set/class issues for the moment - composition consists of a partial function assigning to a pair of morphisms (on which it's defined) a third morphism, which we call their composition. So equality between morphisms is folded into the very nature of sets themselves (in this case, the sets of morphisms).



            If you're familiar with model theory, equality is part of the logical language - on the same level as the quantifiers and Boolean connectives - while compositionof morphisms would be part of the signature (or language, or vocabulary, or ...), similarly to the symbol for the group operation in the context of groups.



            Your second-to-last paragraph, though, is more special. The phenomenon you're describing there is actually something category theory explicitly doesn't want to pay attention to, at least most of the time, since one of the big points is that we can forget what the objects are and just look at how the morphisms behave. Certainly there's no object/morphism relation in general categories - for example, think about a group viewed as a one-object category.







            share|cite|improve this answer












            share|cite|improve this answer



            share|cite|improve this answer










            answered 7 hours ago









            Noah Schweber

            121k10147280




            121k10147280























                6














                Category theory is ordinarily formulated within the framework of axiomatic set theory, just like the rest of mathematics. Axiomatic set theory includes equality as a primitive notion. So there is no need to separately specify equality as part of a category--you already know what equality means from your background foundation of mathematics. There is nothing special about category theory in this respect; this is just like how when defining a group, you don't have to specify what it means for two elements of the group to be equal, for instance.



                Yes, the underlying notion of equality may include equalities that you don't want, such as a morphism being equal to an object. But this is not actually a problem at all--you will never talk about morphisms being equal to objects, so you don't care whether they are. Note in particular that an isomorphism between categories does not need to preserve such equalities.



                (That said, there is some interest in alternate foundations of mathematics that are more strongly "typed", so that you can't talk about equalities of things that shouldn't "make sense". See for instance https://ncatlab.org/nlab/show/structural+set+theory. Again, though, this is in no way specific to category theory, nor is it at all logically necessary for the development of mathematics.)






                share|cite|improve this answer




























                  6














                  Category theory is ordinarily formulated within the framework of axiomatic set theory, just like the rest of mathematics. Axiomatic set theory includes equality as a primitive notion. So there is no need to separately specify equality as part of a category--you already know what equality means from your background foundation of mathematics. There is nothing special about category theory in this respect; this is just like how when defining a group, you don't have to specify what it means for two elements of the group to be equal, for instance.



                  Yes, the underlying notion of equality may include equalities that you don't want, such as a morphism being equal to an object. But this is not actually a problem at all--you will never talk about morphisms being equal to objects, so you don't care whether they are. Note in particular that an isomorphism between categories does not need to preserve such equalities.



                  (That said, there is some interest in alternate foundations of mathematics that are more strongly "typed", so that you can't talk about equalities of things that shouldn't "make sense". See for instance https://ncatlab.org/nlab/show/structural+set+theory. Again, though, this is in no way specific to category theory, nor is it at all logically necessary for the development of mathematics.)






                  share|cite|improve this answer


























                    6












                    6








                    6






                    Category theory is ordinarily formulated within the framework of axiomatic set theory, just like the rest of mathematics. Axiomatic set theory includes equality as a primitive notion. So there is no need to separately specify equality as part of a category--you already know what equality means from your background foundation of mathematics. There is nothing special about category theory in this respect; this is just like how when defining a group, you don't have to specify what it means for two elements of the group to be equal, for instance.



                    Yes, the underlying notion of equality may include equalities that you don't want, such as a morphism being equal to an object. But this is not actually a problem at all--you will never talk about morphisms being equal to objects, so you don't care whether they are. Note in particular that an isomorphism between categories does not need to preserve such equalities.



                    (That said, there is some interest in alternate foundations of mathematics that are more strongly "typed", so that you can't talk about equalities of things that shouldn't "make sense". See for instance https://ncatlab.org/nlab/show/structural+set+theory. Again, though, this is in no way specific to category theory, nor is it at all logically necessary for the development of mathematics.)






                    share|cite|improve this answer














                    Category theory is ordinarily formulated within the framework of axiomatic set theory, just like the rest of mathematics. Axiomatic set theory includes equality as a primitive notion. So there is no need to separately specify equality as part of a category--you already know what equality means from your background foundation of mathematics. There is nothing special about category theory in this respect; this is just like how when defining a group, you don't have to specify what it means for two elements of the group to be equal, for instance.



                    Yes, the underlying notion of equality may include equalities that you don't want, such as a morphism being equal to an object. But this is not actually a problem at all--you will never talk about morphisms being equal to objects, so you don't care whether they are. Note in particular that an isomorphism between categories does not need to preserve such equalities.



                    (That said, there is some interest in alternate foundations of mathematics that are more strongly "typed", so that you can't talk about equalities of things that shouldn't "make sense". See for instance https://ncatlab.org/nlab/show/structural+set+theory. Again, though, this is in no way specific to category theory, nor is it at all logically necessary for the development of mathematics.)







                    share|cite|improve this answer














                    share|cite|improve this answer



                    share|cite|improve this answer








                    edited 7 hours ago

























                    answered 7 hours ago









                    Eric Wofsey

                    179k12204331




                    179k12204331























                        2














                        As the other answers state, for typical, set-theoretic foundations, a global notion of equality is always available. There is thus no need to explicitly provide a notion of equality, and it is always possible to ask whether two mathematical objects (i.e. sets) are equal. Functions, i.e. arrows of $mathbf{Set}$, are sets and so are also objects of $mathbf{Set}$. The function qua an object isn't "essentially exactly the same" as the function qua an arrow. They are exactly the same thing, no "essentially" about it.1



                        However, this is not desirable for category theory. Ideally, you'd use a logical framework in which the principle of equivalence held. The principle of equivalence states that everything you state should be isomorphism invariant. Makkai developed FOLDS explicitly to provide such a logical framework. The slightly more usable Dependent FOL (DFOL) also accomplishes this goal as well. This is also typically accomplished by formalizations in dependent type theories such as the Calculus of (Inductive) Constructions. As I illustrate in this answer, formalizing the notion of category in DFOL would explicitly provide a (family of) notion(s) of equality for morphism. (And, notably, not provide a notion of equality for objects.)



                        Within traditional set-theoretic foundations, if you wanted to be more explicit about notions of equality, you could work in a setoid-enriched version of category theory. You would provide a (family of) setoid(s) of arrows2 This would require composition to respect the setoid structure of its inputs. This would then impact the definition of things like functors.



                        1 Technically, we would probably add the codomain (at least) to the notion of arrow for $mathbf{Set}$ since hom-sets are usually defined to be disjoint in set-theoretic foundations. The resulting arrow is still a set, though, so that doesn't really change the story.



                        2 Indeed, a (set-theoretic) model of the DFOL theory I sketch in the other answer would have arrows be a family of setoids.






                        share|cite|improve this answer


























                          2














                          As the other answers state, for typical, set-theoretic foundations, a global notion of equality is always available. There is thus no need to explicitly provide a notion of equality, and it is always possible to ask whether two mathematical objects (i.e. sets) are equal. Functions, i.e. arrows of $mathbf{Set}$, are sets and so are also objects of $mathbf{Set}$. The function qua an object isn't "essentially exactly the same" as the function qua an arrow. They are exactly the same thing, no "essentially" about it.1



                          However, this is not desirable for category theory. Ideally, you'd use a logical framework in which the principle of equivalence held. The principle of equivalence states that everything you state should be isomorphism invariant. Makkai developed FOLDS explicitly to provide such a logical framework. The slightly more usable Dependent FOL (DFOL) also accomplishes this goal as well. This is also typically accomplished by formalizations in dependent type theories such as the Calculus of (Inductive) Constructions. As I illustrate in this answer, formalizing the notion of category in DFOL would explicitly provide a (family of) notion(s) of equality for morphism. (And, notably, not provide a notion of equality for objects.)



                          Within traditional set-theoretic foundations, if you wanted to be more explicit about notions of equality, you could work in a setoid-enriched version of category theory. You would provide a (family of) setoid(s) of arrows2 This would require composition to respect the setoid structure of its inputs. This would then impact the definition of things like functors.



                          1 Technically, we would probably add the codomain (at least) to the notion of arrow for $mathbf{Set}$ since hom-sets are usually defined to be disjoint in set-theoretic foundations. The resulting arrow is still a set, though, so that doesn't really change the story.



                          2 Indeed, a (set-theoretic) model of the DFOL theory I sketch in the other answer would have arrows be a family of setoids.






                          share|cite|improve this answer
























                            2












                            2








                            2






                            As the other answers state, for typical, set-theoretic foundations, a global notion of equality is always available. There is thus no need to explicitly provide a notion of equality, and it is always possible to ask whether two mathematical objects (i.e. sets) are equal. Functions, i.e. arrows of $mathbf{Set}$, are sets and so are also objects of $mathbf{Set}$. The function qua an object isn't "essentially exactly the same" as the function qua an arrow. They are exactly the same thing, no "essentially" about it.1



                            However, this is not desirable for category theory. Ideally, you'd use a logical framework in which the principle of equivalence held. The principle of equivalence states that everything you state should be isomorphism invariant. Makkai developed FOLDS explicitly to provide such a logical framework. The slightly more usable Dependent FOL (DFOL) also accomplishes this goal as well. This is also typically accomplished by formalizations in dependent type theories such as the Calculus of (Inductive) Constructions. As I illustrate in this answer, formalizing the notion of category in DFOL would explicitly provide a (family of) notion(s) of equality for morphism. (And, notably, not provide a notion of equality for objects.)



                            Within traditional set-theoretic foundations, if you wanted to be more explicit about notions of equality, you could work in a setoid-enriched version of category theory. You would provide a (family of) setoid(s) of arrows2 This would require composition to respect the setoid structure of its inputs. This would then impact the definition of things like functors.



                            1 Technically, we would probably add the codomain (at least) to the notion of arrow for $mathbf{Set}$ since hom-sets are usually defined to be disjoint in set-theoretic foundations. The resulting arrow is still a set, though, so that doesn't really change the story.



                            2 Indeed, a (set-theoretic) model of the DFOL theory I sketch in the other answer would have arrows be a family of setoids.






                            share|cite|improve this answer












                            As the other answers state, for typical, set-theoretic foundations, a global notion of equality is always available. There is thus no need to explicitly provide a notion of equality, and it is always possible to ask whether two mathematical objects (i.e. sets) are equal. Functions, i.e. arrows of $mathbf{Set}$, are sets and so are also objects of $mathbf{Set}$. The function qua an object isn't "essentially exactly the same" as the function qua an arrow. They are exactly the same thing, no "essentially" about it.1



                            However, this is not desirable for category theory. Ideally, you'd use a logical framework in which the principle of equivalence held. The principle of equivalence states that everything you state should be isomorphism invariant. Makkai developed FOLDS explicitly to provide such a logical framework. The slightly more usable Dependent FOL (DFOL) also accomplishes this goal as well. This is also typically accomplished by formalizations in dependent type theories such as the Calculus of (Inductive) Constructions. As I illustrate in this answer, formalizing the notion of category in DFOL would explicitly provide a (family of) notion(s) of equality for morphism. (And, notably, not provide a notion of equality for objects.)



                            Within traditional set-theoretic foundations, if you wanted to be more explicit about notions of equality, you could work in a setoid-enriched version of category theory. You would provide a (family of) setoid(s) of arrows2 This would require composition to respect the setoid structure of its inputs. This would then impact the definition of things like functors.



                            1 Technically, we would probably add the codomain (at least) to the notion of arrow for $mathbf{Set}$ since hom-sets are usually defined to be disjoint in set-theoretic foundations. The resulting arrow is still a set, though, so that doesn't really change the story.



                            2 Indeed, a (set-theoretic) model of the DFOL theory I sketch in the other answer would have arrows be a family of setoids.







                            share|cite|improve this answer












                            share|cite|improve this answer



                            share|cite|improve this answer










                            answered 4 hours ago









                            Derek Elkins

                            16.1k11337




                            16.1k11337






























                                draft saved

                                draft discarded




















































                                Thanks for contributing an answer to Mathematics Stack Exchange!


                                • Please be sure to answer the question. Provide details and share your research!

                                But avoid



                                • Asking for help, clarification, or responding to other answers.

                                • Making statements based on opinion; back them up with references or personal experience.


                                Use MathJax to format equations. MathJax reference.


                                To learn more, see our tips on writing great answers.





                                Some of your past answers have not been well-received, and you're in danger of being blocked from answering.


                                Please pay close attention to the following guidance:


                                • Please be sure to answer the question. Provide details and share your research!

                                But avoid



                                • Asking for help, clarification, or responding to other answers.

                                • Making statements based on opinion; back them up with references or personal experience.


                                To learn more, see our tips on writing great answers.




                                draft saved


                                draft discarded














                                StackExchange.ready(
                                function () {
                                StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3054271%2fwhy-doesnt-the-definition-of-a-category-require-an-explicit-notion-of-moprhisms%23new-answer', 'question_page');
                                }
                                );

                                Post as a guest















                                Required, but never shown





















































                                Required, but never shown














                                Required, but never shown












                                Required, but never shown







                                Required, but never shown

































                                Required, but never shown














                                Required, but never shown












                                Required, but never shown







                                Required, but never shown







                                Popular posts from this blog

                                flock() on closed filehandle LOCK_FILE at /usr/bin/apt-mirror

                                Mangá

                                Eduardo VII do Reino Unido