📝Category Theory: Function object

Universal construction

ab is a function object    z,!h:z(ab)g=eval(h×id)a \Rightarrow b \text{ is a function object} \iff \forall z, \exists! h: z \to (a \Rightarrow b) \ni g = eval \circ (h \times id)

  • This relies on that a morphism between two products (h×id:(z×a)((ab)×a)h \times id: (z \times a) \to ((a \Rightarrow b) \times a)) can be constructed as a product of two morphisms (hh and idid), so that we know that it is a correct way to obtain (ab)×a(a \Rightarrow b) \times a from z×az \times a using h:z(ab)h: z \to (a \Rightarrow b)


Want to receive my 🖋 posts as I publish them?