Minh 12:41 PM Hi Alex! Could i ask you a very newbie category theory question?

Alex 12:42 PM Of course!

Minh 12:43 PM I’m a bit confused about how proofs are supposed to be written, for example the proof that identity is neutral and composition is associative:

12:43 i don’t see any clearer way of writing a proof than it has already been defined in the text

Alex 12:44 PM oh I guess they mean the calculation forall a. (f o id)(a) = f (id(a)) = f(a) hence f o id = f

Minh 12:45 PM ahhh okay, thanks! :slightly_smiling_face: also, when asking that sort of question, do you interpret that question in general or with respect to a specific category (in this case Set)?

Alex 12:47 PM well in this particular case I think they’re asking you to prove that Set satisfies the axioms 12:47 Very badly written.

Minh 12:48 PM i suppose i should expect the calculation to differ for different categories then Alex 10 minutes ago Yes of course. Unless they’re categories of sets + structure and structure-preserving functions (e.g. graphs and graph homomorphisms)

Alex 10 minutes ago There you just need to additionally prove that the composition of functions preserves the structure

Alex 9 minutes ago E.g. that two graph homomorphisms (which are just functions from nodes to nodes) compose to a graph homomorphism :+1: 1

Minh 5 minutes ago i think i understand this. do you mean that proving categories of sets + structure and structure preserving functions, is not that much different from what i’ve just shown you, as opposed to other categories?

Alex 3 minutes ago Yes exactly. I mean that the proof is exactly this: Proof. As for Set, but we additionally prove that the identity function is structure-preserving, and that the composition of structure-preserving functions is also structure-preserving. … [] (edited)

Alex 3 minutes ago But it can be very different for other kinds of categories

Minh 2 minutes ago i see! thanks :slightly_smiling_face:

Alex 12:48 PM For reference, it is my opinion that the only authoritative book which is accessible to computer scientists is in fact Awodey :+1: 1

Minh 2:20 PM This implies that there exists morphisms f : A -> B and g : B -> A where their compositions are not identities. But how can we tell that, if all the information we have to consider are the objects A & B and the type of the morphism? (assuming the notion of isomorphism isn’t dependent on the content of A, B, or what f and g “do” as functions)

Alex 2:21 PM There are indeed many many categories where there are morphisms f : A ->B and g : B -> A where f o g =/= id 2:22 take e.g. any nonempty set S a point x : {} -> S of the set the unique function f : S -> {} 2:22 where {*} is the one-element set, aka the terminal object 1 of the category Set 2:22 we have f o x = id_{*}, but definitely not x o f = id_S

Side conversation start

Alex Today at 2:22 PM we have f o x = id_{*}, but definitely not x o f = id_S

Minh 33 minutes ago okay i can’t believe i confused myself again. I don’t know if it’s wrong to make these functions concrete, but if f took the set {1, 2, 3} to a point {1}, and x concretely took the point {1} to the set {1, 2, 3}, would these not be isomorphic?

Alex 27 minutes ago let f : {1, 2, 3} -> {1} and x : {1} -> {1, 2, 3} as you describe

Alex 27 minutes ago calculate f o x and x o f and see

Minh 25 minutes ago i must be calculating them wrong, because i’m not seeing

Alex 25 minutes ago so what function is f o x?

Minh 25 minutes ago {1} -> {1] ?

Alex 25 minutes ago that’s its type

Alex 24 minutes ago but concretely it is defined by (f o x)(a) = f(x(a)) = f(1) = 1

Alex 24 minutes ago so the function f o x : {1} -> {1} is the function that maps 1 to 1

Alex 23 minutes ago it couldn’t do anything else in fact: a function from any domain into {1} must map everything in its domain into {1}, so it must map everything to the single element 1 \in {1} (this is the beginnings of category theory)

Alex 23 minutes ago now compute x o f

Minh 22 minutes ago so the function x o f is (x o f)(a) = x (f (a)) = x(1) = 1, 2, 3

Alex 20 minutes ago hang on :joy: 1

Alex 20 minutes ago a function returns for everything in its domain something in its codomain

Alex 20 minutes ago so what is the function x?

Minh 19 minutes ago i think this is where i’m misunderstanding it

Alex 19 minutes ago x : {1} -> {1, 2, 3} x(a) = 1

Alex 19 minutes ago aka x = { 1 |-> 1 }

Alex 19 minutes ago while f = { 1 |-> 1, 2 |-> 1, 3 |-> 1 }

Minh 18 minutes ago i’m imagining a haskell defined function, where you can literally state “x {1} = {1, 2, 3}”

Alex 18 minutes ago this is not a Haskell function, this is a set-theoretic function

Alex 18 minutes ago like on your 1st year sets, relations, discrete maths type of thing

Minh 18 minutes ago (did not do that)

Minh 18 minutes ago a function returns for everything in its domain something in its codomain this is new information to me

Minh 17 minutes ago so given this, i don’t understand how there can exist a morphism from the empty set (the initial object) to any set

Alex 17 minutes ago it is most definitely not

Alex 17 minutes ago you surely know that a Haskell function returns something in its output type for everything in its input type

Minh 16 minutes ago ahhhh i realise im thinking about it in the wrong way

Minh 15 minutes ago i wasn’t thinking about it in terms of possible inputs and outputs, i was thinking “give me the set {1} and ill return you the set {1, 2, 3}”

Alex 15 minutes ago no no no, {1} and {1, 2, 3} are the domain and codomain of the function

Alex 15 minutes ago x : {1} -> {1, 2, 3} means that x is a function from the type {1} to the type {1, 2, 3}

Alex 14 minutes ago it’s almost the same as x :: () -> Either () (Either () ())

Minh 13 minutes ago right i see! so re: i don’t understand how there can exist a morphism from the empty set (the initial object) to any set is this trivial because we don’t actually have a domain for the function, so our codomain can be anything?

Alex 13 minutes ago it is trivial but not for quite that reason

Alex 13 minutes ago recall: function maps everything in domain to something in codomain (edited)

Alex 13 minutes ago take any set S, say S = {0, 1, 2, 3…}

Alex 12 minutes ago a function f : \emptyset -> S maps everything in its domain to everything in its codomain

Alex 12 minutes ago what is in its domain? nothing

Alex 12 minutes ago so that’s a function

Alex 12 minutes ago it just maps [nothing] to…. well there’s nothing that needs to be mapped

Alex 11 minutes ago f(a) = … just kidding I don’t need to write this because there’s literally no possible a \in \emptyset …

Minh 11 minutes ago i understand! thank you! does the idea of visualising domain and codomain generalise over different categories, or is this specific to Set because of functions

Alex 11 minutes ago it’s absolutely central to category theory

Alex 11 minutes ago one way to understand category theory is as an “algebra of functions”

Alex 10 minutes ago where the only possible moves are composition and identity

Alex 10 minutes ago but it’s worth understanding what functions are in set theory

Minh 10 minutes ago right, so even in other categories, the types of objects will represent a domain/codomain?

Alex 9 minutes ago every category has morphisms and objects, and every morphism has a domain and a codomain object (edited)

Alex 9 minutes ago these are the very words used in the definition of a category

Alex 8 minutes ago but it’s worth differentiating between Haskell and set theory for now

Alex 8 minutes ago in Haskell a function is just a usual function definition

Alex 7 minutes ago in set theory, a function is a 3-tuple (A, B, f) where A and B are sets f is a relation from A to B, i.e. a subset of the set of all possible pairs A x B = { (a, b) | a \in A and b \in B} such that f is total and single-valued, i.e. for every x \in A there exists exactly one b \in B such that (a, b) \in f (edited)

Alex 7 minutes ago we call A the domain and B the codomain

Alex 6 minutes ago two functions (A, B, f) and (A', B', f') are equal if they are component-wise equal, i.e. if A = A', B = B', and f = f' as subsets of A x B

Minh 6 minutes ago so is it more correct to think of objects A and B as domains and codomains, rather than as particular values of their types?

Alex 6 minutes ago I don’t think the latter has any standing. the terms domain and codomain arise exactly from this

they have since been abstracted in category theory, but this is their origin

Alex 16 minutes ago you should now retry x o f versus f o x

Minh 13 minutes ago Right, so let f : {1, 2, 3} -> {1} and x : {1} -> {1, 2, 3} x o f is (x o f)(a) = x (f (a)) = x(1) = something of either value 1, 2, or 3? (edited)

Minh 12 minutes ago im thinking that x has to map {1} to a single fixed chosen value in the codomain {1, 2, 3} (edited)

Alex 7 minutes ago exactly, it must

Alex 7 minutes ago nothing else is a function

Alex 7 minutes ago so one thing you could pick here is the inclusion….

Alex 7 minutes ago {1} is a subset of {1, 2, 3}

Alex 6 minutes ago so there is an obvious function x : {1} -> {1, 2, 3} that includes the subset {1} into the set {1, 2, 3} (edited)

Alex 6 minutes ago it is the function x(a) = a

Alex 6 minutes ago concretely, x = { (1, 1) }

Minh 2 minutes ago is there any meaning in picking this inclusion?

Alex 2 minutes ago not really, no matter which function {1} -> {1, 2, 3} you pick (there are exactly three such functions), it won’t be an isomorphism

Minh 7 minutes ago i think i’ve just about convinced myself of this, thank you!

Alex 6 minutes ago very good!

Alex 6 minutes ago so which of the two equalities fails?

Minh 5 minutes ago x o f = id_S, because it’s not possible for x to consistently return the same value that was passed to f?

Alex 3 minutes ago exactly :heart: 1

Alex 3 minutes ago more concretely, two functions f, g are equal if and only if f(x) = g(x) for all x in their domain

Alex 3 minutes ago (also they must have the same domain and codomain)

Alex 3 minutes ago this is known as “function extensionality”

Alex 2 minutes ago (it comes for free in set theory, because sets just work that way) :+1: 1

Alex 2 minutes ago if x is the inclusion you have (x o f)(2) = 1 =/= 2 = id_S(2)

Alex 2 minutes ago so the two functions differ at input 2, done

Minh 3 minutes ago just to double-check, if an object represented a domain of a particular morphism, does this mean that two objects representing the same domain but instantiated to different values in that domain, would still be considered the same object? (i’m not sure whether its a good idea to ever consider an object taking a particular value) (edited)

Alex 2 minutes ago Objects are not instantiated to values, they’re merely sitting there

Alex 1 minute ago Objects are usually particular sets, graphs, groups, topological spaces, … :+1: 1

Alex < 1 minute ago Forget any intuition from CS, it’s useless and irrelevant

Alex < 1 minute ago Category theory is in algebra-land :+1: 1

Side conversation end

Minh 2:24 PM right i see, we can’t reproduce the set S from the terminal object because of lack of information - doesn’t this imply that an isomorphism should depend on what f and g do as functions?

Alex 2:25 PM there might be many isomorphisms between two objects A and B, so yes it’s very strongly dependent 2:25 think of how many ways there are to prove that Nat is isomorphic to Nat x Nat 2:25 each one is a different pair of functions

Minh 2:26 PM would you also say that the notion of isomorphism depends on the content of the objects A and B?

Alex 2:26 PM how could it not?

Minh 2:27 PM got you thanks,

Minh 2:27 PM Eddie Jones [2:15 PM] Right yeah so the language of category theory isn’t really about the contents of objects in fact objects don’t always have a notion of “contents” it is just about morphisms and objects but this language talks about specific categories such as Set where objects and morphisms have a specific meaning [2:15 PM] So the notion of isomorphism isn’t dependent on the content of A, B, or what f and g “do” as functions really [2:16 PM] But the counter example just illustrates that there exists an f and g in Set that have the right type but aren’t isomorphic Minh [2:25 PM] alex says the notion of an isomorphism is dependent on what f and g do as functions apparently Eddie Jones [2:26 PM] yeah you can’t know that f and g are isomorphic until you know what they do [2:27 PM] but isomorphic is defined for an arbitrary category which means the definition doesn’t even rely on the fact they are functions

Alex 2:28 PM oh I see, classic Eddie 2:29 he is right though that saying “f : A -> B is an isomorphism” is a completely formal statement in the theory of categories New 2:29 it means: \exists g : B -> A. f o g = id ^ g o f = id 2:29 but checking that something is an actual isomorphism in a specific category does require intimate knowledge of A, B, and f :+1: 1

Minh 12:49 PM Hi! Could you help explain what this one object means? From what Eddie has told me, objects and morphisms can be literally anything without any context as long as they have the right laws, so the object doesn’t really have to represent anything - it’s just abstract. Does this mean that the ideas of objects as domains/codomains no longer apply in this context?

“Another category we can be build from natural numbers has only one object and its morphisms are the natural numbers. The identity morphism is 0 and composition is given by addition. The laws follow from the fact that 0 is neutral (n +0= n =0+ n) and (+) associative (l + m) + n = l + (m + n). Here we exploit the algebraic properties of +, namely that it is a monoid; hence categories with one object correspond to monoids. "

Alex 12:49 PM well, you know what a monoid is, right?

Minh 12:50 PM yes sir (in a Haskell context)

Alex 12:50 PM it’s the same in algebra, it’s a set (cf. type) with an associative binary operation and a unit element 12:50 so given two elements x, y \in M of a monoid, you can always combine them to form x \cdot y \in M 12:51 so far so good?

Minh 12:51 PM yep (which is i why i first thought of the object being the domain of Nats)

Alex 12:51 PM ok so here’s the brain twister 12:51 a category is a typed monoid 12:51 you can’t just form x \cdot y whenever you please 12:52 every “element” of the category (= morphism) has a “source” and a “target” 12:52 and you can only “multiply” two elements if the source of one and the target of the other match 12:53 so you can only have x \cdot y whenever x and y “match” in some sense 12:53 so if x : A -> B and y : B -> C you can form y \cdot x : A -> C

Minh 12:54 PM right

Alex 12:54 PM you can think of the elements of this typed monoid as “going” from places to places 12:54 x : A -> B is a process, maybe, that takes you from A to B in some particular way 12:55 a monoid is just a place where everything takes you from the same place to the same place 12:55 so you have just a single “type” * 12:55 and every x is x : * -> * 12:55 and thus you can compose any x, y : * -> * because their source and targets just match

Minh 12:58 PM ah i see, this makes sense! 12:59 right, so could i think of the object being representative of a single type (under which addition with natural numbers results in that same type)?

Alex 12:59 PM exactly 12:59 picture the category Set 12:59 a function f : S -> T is a “way” of going from S to T 1:00 given any x \in S, it will give you f(x) \in T 1:00 there might be many ways f, g, h, … : S -> T of going from S to T in Set 1:00 but here’s a subcategory, which is in fact a monoid 1:00 take the set Nat of natural numbers New 1:00 the functions f : Nat -> Nat form a monoid 1:01 each f : Nat -> Nat is a way of going from Nat back to Nat, the monoid operation is exactly function composition, there is an identity elem namely the identity function 1:05 the association object ~ type is very strong in general 1:06 in rare cases object ~ state, but that’s not common

Minh 1:06 PM so is it okay to both be able to concretise the monoidal object as a concrete type, e.g. Nat, as well as visualise it as any type for which (+ Nat) will work e.g. Double?

Alex 1:06 PM perhaps lose the intuition even further and yield to abstraction 1:07 given any monoid (M, \cdot, e) there is a category with a single object, call it *, and morphisms m : * -> * being the elements of the monoid 1:07 you can do anything you like and call anything however you like, and postulate as much as you need 1:08 the single object in the above construction could be called * or, could be Nat, or Double… doesn’t matter, it’s just an object

Minh 1:08 PM i see!

Alex 1:09 PM the fact m : * -> * is the important thing 1:09 which tells you that m takes you from a place back to the same place :+1: 1