category-theory.org

Category Theory

Category Theory:

• Foundational framework of mathematics: the foundations of category theory itself have to be clarified yet
• An abstract algebra of abstract functions
• It’s the arrows what counts.

\bigskip

Category - informal description:

• A collection of arrows and morphism that can be composed if they are adjacent.
• A structure packing structures of the same type (same category) and structure preserving mappings between them.
• Directed Multigraph with Algebra of paths. Each finite path is associated with an unique arrow.

Nr. of path segments	Path type
0	Identity
1	Morphism
2	Composition
3	Associativity law of composition

• Is context rich and content poor
• Is mathematical context where construction is possible.
  • Functors: Constructors
  • Natural Transformations: Comparison of constructions
• Example in programming:
  • Objects are types
  • Morphisms are functions between types

\bigskip

Category - formal definition:

• A quadruple $\cat{C}: (\Ob, \Mor, \comp, \id)$
• $\Ob(\cat{C})$ : Class of objects: $A$, $B$, $C$, $…$ e.g. Types / Propositions / Algebras / Logic Formulas
  An object exists in and depends upon an ambient category. \ An object is characterized by its morphisms going in and out of it. \ Objects are always characterized up to isomorphism (in the best cases, up to a unique isomorphism). E.g. there is no such thing as the natural numbers. \ However, the concept of natural numbers exists.
• $\Mor(\cat{C})$ : Morphisms (arrows): $f$, $g$, $h$, $…$ e.g. Computation / Proofs / ??? /
  Implication between Logic formulas
• $\comp$ : Morphism composition - associative (binary) operation: $$(f \comp g) \comp h = f \comp (g \comp h)$$ $$\Hom(A,B) \cprod \Hom(B,C) → \Hom(A,C): g \comp f$$ is a partially binary operation on Mor(CAT::) $$(g \comp f)(x) = g(f(x))$$
• $\id$ : an identity morphism on every object $A: \id_A$

Types of categories

Locally Small Category LSC:
A category where each Hom-set is a small set, i.e. a set and not a proper class. \ LSC “doesn’t have too many morphisms” \ $∀ A,B ∈ \Ob(\cat{C}): \Hom_\cat{C}(A, B)$ is a small set. \ (TODO arrow weight = price of calculation; preference for compositions)

\bigskip

Small Category SC:
A locally small category such that also the objects form a small set, i.e. a set and not a proper class, i.e. both the objects and morphisms form small sets.

\bigskip

“$X \iso Y$ (Things are equal) up to isomorphism” - meaning:
Things are isomorphic, i.e. $X$ can be mapped to $Y$ in a way that we see that $X$ and $Y$ are

• structurally the same, i.e.
• only formally different, i.e.
• working via analogy, i.e.
• $X$ is just a renamed version of $Y$

Such mapping is called isomorphism.

\bigskip

Commuting diagram / The diagram commutes - meaning:
No matter which way you go around you get the same thing.

\bigskip

Cartesian Closed Category CCC - useful in programming

• Cartesian: for any two objects $A$, $B$ of a category $\mathcal{C}$ there exists an ordered pair in $\mathcal{C}$ called product, noted as $A \cprod B$.
• Closed: for any two objects $A$, $B$ there exists a morphisms $A → B$ in $\mathcal{C}$ called exponential, notes as $B^A$.
• 0-th power of an obj: has terminal obj $\termObj$ (for all objects there exists a unique morphism $A → \termObj$)
• multiplying by terminal obj $\termObj$ gives back the original obj
• initial obj $\initObj$ - dual to terminal obj $\termObj$; Top and Bottom objects i.e. any one-element set (= singleton) is terminal DTTO for poset 1 is such an object that any other object is below it
• ? monoidal structure on objects ?

\bigskip

Locally Closed Cartesian Category LCCC:
For every obj $X$ sliced category is a CCC

Sliced Category C/c Category over an Object, i.e. an over-category. Slicing the original category along a specific object

\bigskip

Bi-Cartesian Closed Category BCCC: Algebra of Types can be made here

• has coproduct for every pair of objects
• has initial obj $\initObj$

\bigskip

Universal Mapping Property UMP:

• Universal - for all
• Consists of Initial and Terminal mapping (morphism)
• Universal Construction - 3 steps (? the triangle ?):

\begin{equation*} \begin{tikzcd} X \arrow[r, “u”] \arrow[rd] & F(A) \arrow[d, “F(h)”, dashed] & A \arrow[d, “h”, dashed]
& F(A’) & A’ \end{tikzcd} \end{equation*}

The double triangle of Product:

\begin{equation*}

\begin{tikzcd} & X \arrow[ld, “p_A”’] \arrow[rd, “p_B”] \arrow[d, “u”, dashed] &

A & A × B \arrow[r, “π_B”] \arrow[l, “π_A”’] & B \end{tikzcd}

\end{equation*}

Features of a category

Associative composability
$(x \comp y) \comp z = x \comp (y \comp z)$

\bigskip

Identity on objects

\bigskip

Function On sets / between sets

Pure: must be memoizable (lookup table)

Total: defined for all arguments

Partial: defined only for some arguments

Directionality: a function is an arrow “from → to”, i.e. functions are not symmetric; potentially an n-to-1 relation.

Inverse: not guaranteed to exist

$f: X → Y$ where $X$ is a Domain and $Y$ is a Codomain of $f$

Image: A proper subset of a Codomain

Container: function itself can be regarded as a container, e.g. identity function

Evaluation: it returns a value (when evaluated) i.e. data are represented as values; i.e functions and data are the same

Function type: is an exponential which is a data type; (Exponential is like an iterated product)

\bigskip

Morphisms and Mappings

Mapping or morphism of $X$ to/on $Y$: $X → Y$:

Latin	Greek / morphisms	Meaning	Functor
surjective	epic / epi \surj	all $Ys$ are used	Full
injective	monic / mono \inj	distinct $Xs →$ distinct $Ys$	Faithful
bijective	epi and mono \bij	exact pairing between $X, Y$	Full & Faithful
strict		$X \surj Y$ but not $Y \inj X$
			Faithful, not Full

Also:

Morphism	Size relation	Meaning	Reading
Surjection	$\abs{X} \geq \abs{Y}$	onto	$X$ at least as big as $Y$ or bigger
Injection	$\abs{X} \leq \abs{Y}$	one-to-one correspondence	$X$ at least as small as $Y$ or smaller
Bijection	$\abs{X} = \abs{Y}$	mutually unambiguous	$X$ has the same size as $Y$
Strict	$\abs{X} < \abs{Y}$	? double usage of some $Ys$ ?	$X$ strictly smaller than $Y$

• Isomorphism: https://en.wikipedia.org/wiki/Isomorphism
  isomorphic ~ “only formally different”
• Automorphism: https://en.wikipedia.org/wiki/Automorphism
• Endomorphism: https://en.wikipedia.org/wiki/Endomorphism
  Orthogonal projection of points onto a line is an example of an endomorphism that is not an automorphism.

Homomorphism - structure-preserving mapping (between two algebraic objects).
Morphishm implication structure:

\begin{equation*} \begin{tikzcd} Automorphism \arrow[d, Rightarrow] \arrow[rr, Rightarrow] & & Isomorphism \arrow[d, Rightarrow]
Endomorphism \arrow[rr, Rightarrow] & & (Homo)morphism \end{tikzcd} \end{equation*}

Epimorphism and monomorphism are dual to each other
Individual monoids themselves give category \ Monoids with homomorphisms give category

\bigskip

Pushout - type of a colimit:
$f: X \surj Y$ is epimorphism, i.e. surjective, i.e. all $Ys$ are used.

\bigskip

Pullback - type of a limit:
$f: X \inj Y$ is monomorphism, i.e. injective, i.e. $X$ is at least as big as $Y$. Also: Pullback of a functor $\Fun{G}$ along a functor $\Fun{F}$ is a composite functor, i.e. functor composition $\Fun{G} \comp \Fun{F}$.

\bigskip

Subobject of an object If $f: X \inj Y$ is monomorphism, i.e. an injection, i.e. different $Xs →$ different $Ys$ - don’t smush multiple elements into one, i.e. parallel arrows, then it is isomorphic (only formally different) from $Y$.

I have a set of different monomorphisms to $Y$:
$$\Set{S} = \{f_1: A → Y, f_2: B → Y\}$$ \ then $f_1 ≡ f_2$ are equivalent if there is an isomorphism $h: A → B$ such that $f_2 = h \comp f_1$ then $\Set{S}$ is isomorphic to some subset of $Y$. i.e. a set of equivalent morphisms mapping distinct $As$ and $Bs$ to $Y$.

Functors

Functor:

• Preserves structure between two categories
• Is a homomorphism by definition, i.e. it preserves structure between two categories
• In programming: total mapping of types; (total = all objects from the source are mapped)
• Constant functor: collapses all objects into one obj and all morphisms into an identity
• Intuitive understanding: (endo) functor is a container - i.e. list contains values (Comonad is a container that already comes prefilled with many values and with an access point to one particular value. E.g. hidden params (for hidden param propagation it’s better to use comonad than monad), history, neighborhood etc.)
• Endofunctor $[\cat{C},\cat{C}]$: is a functor that maps a category to itself Sahil, 15:41 ACTE4, 12.01.2021: From Ancient Greek ἔνδον (éndon, “inner, internal”). \href{https://youtu.be/FyoQjkwsy7o?t=2259}{Endofunctors & Endoscopy}
• Lifting: (= applying functor) transforms a function into a corresponding function within another (usually more general) setting

\begin{equation*} \begin{tikzcd} Fa \arrow[r, “Ff”] & Fb
a \arrow[r, “f”] \arrow[u] & b \arrow[u] \end{tikzcd} \end{equation*}

• Covariant functor: Same directions in src and dst category

G f : (a -> b) -> (G a -> G b)

• Contravariant functor: Reverse direction in src or dst category

G f : (a -> b) -> (G b -> G a)

respectively

G f : (b -> a) -> (G a -> G b)

i.e. $G f : \cat{C^\op} → \cat{D}$ respectively $Gf : \cat{C} → \cat{D^\op}$

• Bifunctor: e.g a Product - it takes two objects and produces third obj, but it also takes two morphisms and produces 3rd morphism which is a product of these
• List: $List(α) = Nil | Const α (List α)$ - most intuitive(?) two morphisms $C \cprod D → E$ functor example. It’s also a type constructor: takes a type $α$ and creates a list of $α$.
• Functoriality: A morphism is functorial, if it fulfills definition of a functor
• Profunctor: Lenses are profunctors. (In Clojure: get-in, update-in, assoc-in functions)

Sum $\csum$ and Product $\cprod are algebraic data types (Algebra on Types):
List(α) = Nil | Const α (List α) ~ L(α) = 1 + α \cprod L(α) => .. => L(α) = 1 / (1 - α) = 1 + α + α \cprod α + α \cprod α \cprod α + …

Inlining and refactoring are the opposite.

\bigskip

Fibre: points mapped to the same (index) value invertibility: function to fibre

NaT Natural Transformations

• a way of/for comparing functors
• maps Morphism(s) to commuting diagram(s) (naturality squares). i.e. comorphism: replacing a square of (complex) relations with a single morphism
• picks a morphish between two Objects; Picking 1 morphishm from a Homset
• Components of NaT
• Composing ftor acting on an obj with a ftor acting on a Morphishm: $α b \comp Ff$
• Every polymorphic functions is a NaT: it is defined for every single type

i.e. multiplication (Product) of all Objects in a Category. The same goes for the dual - the Sum.

• Functor is a container, NaT repackages the container
• Naturality condition i.e. the Naturality Square:

$$Gf ∘ α a = α b ∘ Ff$$

---

The “naturalness” of NaT: the transformation is defined in a way that is consistent across the entire structure of the categories and functors it connects, without making arbitrary choices or depending on specific properties of objects within the categories.

Why Are They Called “Natural”?

The concept of naturality comes from the observation that certain transformations arise in a way that feels “natural” or “canonical,” without the need for arbitrary choices. For example, consider the identity functor ICIC​ on a category CC and any other functor FF from CC to CC. A natural transformation η:IC⇒Fη:IC​⇒F assigns to each object XX in CC a morphism ηX:X→F(X)ηX​:X→F(X) such that for any morphism f:X→Yf:X→Y in CC, we have F(f)∘ηX=ηY∘fF(f)∘ηX​=ηY​∘f. This condition ensures that the way ηη acts on morphisms is consistent and “naturally” aligned with how FF and ICIC​ act on those morphisms. Existence of Non-Natural Transformations

In the strict sense of category theory, transformations that are not “natural” in the sense described above are generally not considered or discussed because the concept of a transformation inherently carries the requirement of this naturality condition. However, one can think of mappings or constructions that are not natural in specific contexts. For example:

• A choice of a particular element from each set in a family of sets cannot be made “naturally” in the absence of additional structure (like an ordering or a distinguished element) because it requires an arbitrary choice.
• Mappings between objects or between functors that do not satisfy the coherence condition of a natural transformation can be considered “non-natural” in the sense that they do not respect the structure of the categories involved.

In essence, the “non-natural” transformations or mappings are those that fail to fulfill the coherence and compatibility criteria across the categories they relate. The power of natural transformations in category theory lies in their ability to capture the essence of “naturally occurring” relationships between mathematical structures in a broad and abstract way, facilitating the study of deeper connections between various areas of mathematics.

---

Compositons of Natural Transformations
See \href{https://math.vanderbilt.edu/dept/conf/tacl2013/coursematerials/SelingerTACL20132.pdf}{SelingerTACL20132}, e.g. NaT compositions in \href{https://gist.github.com/Mzk-Levi/752d1e0f2f7f30cd3bda}{Scala} \

Legend:
$A$ - an obj in the Category $\mathcal{C}$ $(…)A$ / $[…]A$ - an A-component of the NaT (…) / […] \ $α A$ / $β A$ - an A-component of the NaT $α$ / $β$ \ $α FA$ - an FA-component of the NaT $α$ \ $β GA$ / $β FA$ - $GA$ / $FA$ -component of the NaT $β$

\bigskip

Vertical composition

If $α:F → G$ and $β:G → H$ are NaTs, then their vertical composition $$β * α : F → H$$

is defined by: $$(β * α)A = β A \comp α A : FA → HA$$ where $A$ is an obj in the Category C and $(…)A$ is an A-component of the NaT (…)

• is associative and has an id, and allows one to consider the collection

of all functors C → D itself as a category.

\bigskip

Right Whiskering
If $F, G : C → D$ and $H : D → E$ are Ftors, and if $α : F → G$ is a NaT, the right whiskering $$H \comp α : H \comp F → H \comp G$$ is defined as $$(H \comp α)A : H(FA) → H(GA)$$ by $(H \comp α)A = H(α A)$

\bigskip

Left Whiskering
If $F : C → D$ and $G, H : D → E$ are Ftors, and if $α : G → H$ is a NaT, the left whiskering $$α \comp F : G \comp F → H \comp F$$ is defined as $$(α \comp F)A : G(FA) → H(FA)$$ by $(α \comp F)A = α FA$

Horizontal composition

If $F, G : C → D$ and $H, K : D → E$ are Ftors, and if $α : F → G$ and $β : H → K$ are NaTs, the horizontal composition $$β \comp α : H \comp F → K \comp G$$

can be defined in two different ways:

• Right whiskering followed by left whiskering: $β \comp α = (β \comp G) * (H \comp α)$
• Left whiskering followed by right whiskering: $β \comp α = (K \comp α) * (β \comp F)$

The two definitions coincide, because $$(β \comp G) * (H \comp α) A = β GA \comp H(α A)$$ $$(K \comp α) * (β \comp F) A = K(α A) \comp β FA$$

• is associative with an id, and the id coincides with that for vertical

composition.

Enriched Category

The set of morphisms between objects $X$ and $Y$ in some category $\cat{C}$: $\Hom_\cat{C}(X,Y)$:
If the $\Hom_\cat{C}(X,Y)$ is also a vector space then the $\cat{C}$ is enriched over the category of sets. \ If the $\Hom_\cat{C}(X,Y)$ is also an abelian group then the $\cat{C}$ is enriched over the category of abelian groups. \

Yoneda perspective, embeding and lemma

Yoneda Perspective - idea:
An object is completely determined by its relationships to other objects.

\bigskip

Yoneda Embedding - idea:
Replace content of an obj (picked i.e. fixed) by all arrows impinging on (ending in) this obj. See \href{https://youtu.be/JH_Ou17_zyU?t=1h8m9s}{Object in Context}.

It’s content and properties.
How to map from every possible obj $X_i ∈ \cat{C}$ to the set of arrows ending in $A$: $\{X_i → A\}$: \ For every obj $A ∈ \cat{C}$ get a different functor $\Fun{F}_A: \cat{C} → \SmSet$

\bigskip

Yoneda Lemma - idea:

G f : (a -> b) -> (G a -> G b)

NaT and ftor (i.e. Container) can replace each other: $[\mathcal{C},\SmSet](\cat{C}(A,−), \Fun{F}) \iso \Fun{F}A$
also: $[\cat{C},\SmSet](\cat{C}(A,−), \cat{C}(B,−)) \iso \cat{C}(B,A)$ \ Description of integration over a special ftor, i.e. Hom functor.

$A$ is some arbitrary obj of $\cat{C}$.
$F$ is some arbitrary ftor acting on the obj $A$. \ $\iso$ - “naturally isomorphic”, i.e. a NaT exists such that its components are all invertible isomorphisms. \

Hom functors intuition: Serve for the same purposes as Free monoids.

It’s enough to define this NaT on one obj, i.e. set $\cat{C}(A,A)$ and moreover it’s enough to define it on one point in this set i.e. the $\id_A$. The rest of the NaT is transported from this point.

\begin{verbatim} ( ) \iso \Fun{F}A

⎜	⎜
⎜ +– Container of the obj a (i.e. the data structure)

+------------------- Polymorphic higher order Function

(∀ X : (A → X) → \Fun{F}X) \iso \Fun{F}A

⎜	⎜	⎜	⎜
⎜	⎜	⎜ +— Container of the obj $A$, i.e data structure
⎜	⎜ +---------- Functor
⎜ +------------- NaT i.e. Polymorphic Higher Order Function

+------------------ … \end{verbatim}

\begin{equation*} (∀ X : \tikz[baseline]{ \node[fill=blue!20,anchor=base] (t1) {$ (A → X) $}; } → \Fun{F}X) \iso \Fun{F}A \end{equation*}

\begin{itemize}[<+-| alert@+>] \item NaT i.e. Polymorphic Higher Order Function \tikz[na]\node [coordinate] (n1) {}; \end{itemize}

\begin{tikzpicture}[overlay] \path[->]<1-> (n1) edge [bend right] (t1); \end{tikzpicture}

Adjoints, Adjunctions, Adjointness

• Adjunction: a relationship between two functors.
• Adjoints / adjoint functors - functors with a relation of adjunction between them.

If $\Fun{F}$ is (left) adjoint to $\Fun{G}$ and $\Fun{G}$ is (right) adjoint to $\Fun{F}$, then there is typically some formula of the type $(x, \Fun{G}y) \iso (\Fun{F}x, y)$.

\bigskip

Adjunctions: weakening of “equality” of Categories “inverse” is defined only for functions not functors, e.g. Currying: from a Pair to Function type

\bigskip

Adjointness: constructing / generating principle

• Adjunctions/Adjoins are monads ???

Examples:

• product is left adjoint to exponential: $(−) \cross A \ladj (−)^A$
• left adjointness of sum (coproduct), pairing and product: $Σ \ladj Δ \ladj Π$

induction, recursion, Natural Numbers (inductively defined), Lists, … conjunction, disjunction, True, False, Exponentiation Quantifiers: $∀$ Every, $∃$ Exists; $Σ$ Sigma, $Π$ Pi

\bigskip

Abstraction: the non-invertibility

• from all properties (i.e. all points of a fibre) I’m interested only in one
• e.g. I’m not interested in what was the exact input value of a function,

I’m interested only if it was an even or odd value

\bigskip

Modeling: mapping / injecting HomSet of category $\cat{C}$: $\Hom_\cat{C}(A,B) = \{f: A → B\}$

• Set of all morphisms $A → B$ in the category $\cat{C}$. Objects of $\cat{C}$ don’t need to be sets.
• A collection of two monoids $A$,$B$ (The identity on an object is its monoidal operation) with a set of compatible transitions between them.

External vs. Internal Homset

\bigskip

Free Monoid: has a unique mapping to every other monoid
A list of accumulated vals

\bigskip

Hom functor: Functor to category of Sets
Has a NaT to every other functor. This NaT is not unique but limited Reader functor in Haskell

\bigskip

Covariant Hom functor
$\Hom(A,−) : \cat{C} → \SmSet$ \ Same directions in src and dst Category - Haskell type signature:

F f :: (a -> b) -> (F a -> F b)

$\Hom(A,−)$ maps each obj $X ∈ \cat{C}$ to the set of morphisms $\Hom(A,X)$
$\Hom(A,−)$ maps each morphism $f : X → Y$ to the function \ $\Hom(A,f) : \Hom(A,X) → \Hom(A,Y)$ given by

\bigskip

Contravariant Hom functor
$\Hom(−,B) : \cat{C}\op → Set$ \ Reverse directions in src and dst category - Haskell type signature:

F f :: (a -> b) -> (F b -> F a)

$\Hom(−,B)$ maps each obj $X ∈ \cat{C}$ to the set of morphisms $\Hom(X,B)$
$\Hom(−,B)$ maps each morphism $h : X → Y$ to the function \ $\Hom(h,B) : \Hom(Y,B) → \Hom(X,B)$ given by \

\bigskip

Representable functor $\Fun{F}: \cat{C^\op} → \SmSet$ is naturally isomorphic to homset $HomC(−,Y)$ for some obj $X$ of $\cat{C}$. I.e. $\Fun{F}$ can be “represented” by an object $Y$ in $\cat{C}$ such that for any object $X$ in $\cat{C}$ the set of morphisms from $X → Y$ captures the essential information of the functor $F$ applied to $X$.

\bigskip

Representable functor represents:

• Objects of $\cat{C}$ as sets
• Morphisms of $\cat{C}$ as morphisms between sets, i.e. the functions “tabulate” and “index” can be created; mapping of function to a data-type
• Think of a functor $\Fun{F}: \cat{C} → \cat{D}$ as giving a picture, or “representation” of $\cat{C}$ in $\cat{D}$ (Lawvere). Following Lawvere, logicians often call the category ‘theory’, and the functor $\Fun{F} : \cat{C} → \cat{D}$ a “model” of this theory.

\bigskip

For any fixed object $A$ in $\cat{C}$, we have a $HomC(A,−)$, such that we have a mapping $HomC(A,X) → HomC(A, Y)$ when there is a morphism $X → Y$.

\bigskip

Examples: The forgetful functor …

• $\Cat{Grp} → \Cat{Set}$ on the category of groups $(G, *, e)$ is represented by $(\ZZ, 1)$.
• $\Cat{Ring} → \Cat{Set}$ on the category of rings is represented by $(\ZZ[x], x)$, the polynomial ring in one variable with integer coefficients.
• $\Cat{Vect} → \Cat{Set}$ on the category of real vector spaces is represented by $(\RR, 1)$.
• $\Cat{Top} → \Cat{Set}$ on the category of topological spaces is represented by any singleton topological space with its unique $e$.

Kleisli category

• dependency of `negate` on `log` is like a long distance interaction in quantum mechanics: changes to `log` have a “long distance” influence on the `negate`, although `negate` just takes and returns a boolean value.

(def log (atom ""))
(defn negate
  [x]
  {:pre [(boolean? x)] :post [(boolean? ret-val)]}
  (swap! log (fn [_] (str log "negate")))
  (not x))

• embellishment of functions. Embellishment is a monad.
• naturally associated to any monad T
• equivalent to a the category of free T-Algebras

Monad

• Monad is “just” a way of composing special type of functions
• Monad is sort of dual to F-Algebra (sometimes called just Algebra): Algebra takes a term and evaluates it Monad can be used to create terms

Algebra and F-Algebra

Intuition in programming: Algebra provides a way to combine elements inside a container (i.e. Monad). Algebra is defined for a specific type of elements.

In Category Theory F-Algebra is a tuple $(\const{A}, \Fun{F})$ where:

• $\Fun{F} : \cat{C} → \cat{C}$ is an endofunctor in category $\cat{C}$.
• $\const{A} ∈ \Ob{\cat{C}}$ is an object in $\cat{C}$

F-Algebras satisfying coherence conditions for a monad:

$σ \comp η_a = \id_a$
$σ \comp μ_a = σ \comp T σ$

are called Monad Algebras. And these Monad Algebras form Eilenberg-Moore category.

\bigskip

-- f is the endofunctor; t is the carrier type
newtype Algebra f t = Algebra (f t -> t)
sumAlg :: Algebra [] Int
sumAlg = Algebra (foldr (+) 0)

Type signature of Monad-?functions? in Haskell:

return :: a -> m a
bind :: m a -> (a -> m b) -> m b
-- In Haskell monad is defined on sets therefore the type signature of bind is ???
join :: m (m a) -> m b
fmap :: (a -> b) -> m a -> m b
bind f m  = join (fmap f m)
-- and

You can operate on IO Monad
You can’t extract anything from IO Monad (it’s lost) \ Monoid in the category of Endofunctors \

Comonad - Haskell type signature:

(w a -> b) -> (w b -> c) -> (w a -> c)

You can extract from IO Monad
You can’t put anything to IO Monad

Indexed Monad

IxMonad - Haskell type signature:

ibind: m i j a -> (a -> m j k b) -> m i k b

state composition
Session Types, Dependent Types, Dependent State Types

Curry-Howard-Lambek correspondence

Intuitionistic Logic $\bij$ Type Theory $\bij$ Category Theory

\bigskip

Function $A → B$ is a proof of logical implication $A \imp B$
Direct relationship between computer programs and mathematical proofs; from 1940-ties \ Link between Computation and Logic \ Proofs-as-programs and propositions- or formulae-as-types interpretation \ Proofs (= Programs) can be executed \ Typed lambda calculi derived from the Curry–Howard-Lambek paradigm led to software like Coq; \ Curry-Howard-Lambek correspondence might lead to unification between mathematical logic and foundational computer science; \ Popular approach: use monads to segregate provably terminating from potentially non-terminating code \ Alternative: $P$ or $Q$ - “doesn’t really matter what which one it is as long as at least one works”

INTUITIONISTIC (Constructive) LOGIC	TYPE THEORY - Functional Programming	CATEGORY THEORY
Howard	Curry	Jim Lambek
Proposition of some type - (something is true)	Type (contract - a set of values that passes the contract)	Objects
Proof of some type	Term (A program - guarded fn)	Morphisms
Normalisation (Proof equality)	Computation (substitute variable with value)
P implies Q: $P → Q$ (i.e. there exists one)	particular fn of fn of P-contract to guarded fn of Q-contract: $P → Q$, i.e. the $λ$ type	Exponential
$→$ is constructive implication	→ is function from-to
$false → false$ (implies)	{} → {} no values (empty set); contract cannot be satisfied
$false → true$	{} → {.} (one element set)
$true → true$	{.} → {.} (identity function)
true (not →) false (does not imply)	{.} (not →) {}
Conjunction - and: P ∧ Q	Pair (P, Q) (proof-of-P, proof-of-Q)	Product
Alternative - or: P ∨ Q	Union of (different) proofs P, Q	Sum

Correspondance of type habitation and proposition

inhabited - has elements / members
“Either $a$ $b$” is inhabited if either $a$ or $b$ is inhabited (at least one of them is true / provable)

Curry: ((a,b) -> c) -> (a -> (b -> c))
Uncurry: (a -> (b -> c)) -> ((a,b) -> c)

Eval: a function of two args / a pair
$((a \imp b), a) → b$ this is Modus ponens in logic $(a \imp b) ∧ a → b$

True proposition	False proposition	Conjunction $a ∧ b$	Disjunction $a ∨ b$	Implication $a \imp b$
Unit-type	Void-type	Pair $(a,b)$	Either $a$ or $b$	Function type $a → b$
is inhabited	not inhabited
Terminal obj $\termObj$	Initial obj $\initObj$	Categorical product $a \cprod b$	Categorical coproduct $a \csum b$	Exponential obj $b^a$

0 - void type - ?
1 - unit type - 0th-power: terminal obj \ 2 - bool type (two possible values): 1st-power: the obj itself \ 3 - int type - 2nd-power: product \ 4 - real type (if continuum hypothesis holds :-) \ 5 - ? type \

JavaScript & Category Theory: Category == Contracts + Functions guarded by contracts

Set vs. Category theory comparision

Set theory	Category theory	JavaScript
membership relation	-
elements	objects	contracts
sets	categories
-	morphisms: preserve structure between objs	fns guarded by contracts
functions	functors: maps between categories
equations between elems	isomorphisms between objects
equations between sets	equivalences between categories
equations between fns	NaTs: maps between functors

Categorification: structure-weakening process, weakening equalities down to natural isomorphisms and then adding-in rules that these natural isomorphisms have to follow (so it behaves well) Counting number of elements in sets is decategorification; from category we get set or from set we get a number

Monoid homomorphisms: a function between the sets of monoid elements that preserved the monoid structure

Monoidal functors: a functor between categories that preserves the monoidal structure (should preserve multiplication) from functor(prodn([x, y, ..])) to prodn([functor(x), functor(y), ..]) Monoidal monad: ???

Functor: “forget the indexing (domain functor)”

Contract = Object

Product: examples:

Objects - numbers Morphisms - functions ‘less than / greater or equal than’

Isomorphism (bijection when f is a function on set / sets):

∀ f: X → Y there ∃ g: Y → X such that $g \after f = id_X$ and $f \after g = id_Y$ where $id_X$, $id_Y$ are identity morphisms on $X$, $Y$, i.e. $f$ is invertible and $g$ is the inverse of $f$.

Category theory - Modeling (new vocabulary)

hierarchies	partial orders
symmetries	group elements ?
data models	categories
agent actions	monoid actions
local-to-global principles	sheaves (lanovica)
self-similarity	operads
context	monads

olog = ontology log

Different branches of mathematics can be formalized into categories. These categories can then be connected together by functors. And the sense in which these functors provide powerful communication of ideas is that facts and theorems proven in one category can be transferred through a connecting functor to yield proofs of an analogous theorem in another category. A functor is like a conductor of mathematical truth.

Ultimatelly the human lang to talk about ideas is the lang of math.

Formulas, Multiplication, stupid mistakes in deriving, simplification etc. CT looks nicer: no numbers, it’s about ideas

Semantics: TODO rewatch Bartosz Milewski

Designing computer language - Semantics must be provided; done by providing operational semantics

Programming - understanding the meaning i.e. semantics: what does it mean: (+ 1 2)? None of the main prog. languages have (operational semantics) only partially provided.

Operational semantics: “if state === stateX then state = stateY”

“How it executes”; reduction relation: $e1 → e2$ for computers: local, progress oriented Mind machine: We keep on imagining the if-then-else steps. This is bad way - computers are much better at it.

Denotational semantics

Denotational: mapping into mathematics; interpretation of terms: $⟦e⟧ = ?$ e.g.: $⟦ v : τ ⊢ v : τ ⟧ = idτ $ - i.e. the meaning of $⟦…⟧$ is an identity on $τ$ i.e. an access to variable $v$ TODO [klipse “(identity 1)”] programs can be translated to math - math is a better lang for humans “Programm has a meaning i.e. it’s a piece of math: operation, declaration, definition”

Mathematical semantics: Functional Programming

HoTT: functions, types and proofs

A type is an abstraction about a set of vals; it is its construction, i.e. it is about “what” (function declaration). It consists of:
Constructor: how to create an element of this type \ Induction: how to use elements of this type \

For mathematicians the Set Theory is a low level assembly lang of mathematics (recently started to be avoided).

Difference between a type and a set - See \href{https://youtu.be/ba4E6EMagj0?t=283}{La théorie des types | Infini 24}:
A type provides tools for creation of funtions using this type. A set doesn’t provide such tools. I.e. a type has more stucture than a set.\

A (pure) function: mapping between sets. It’s about “how” (function body) - ? contrary of abstraction ?

A proof is an object to be constructed analogically as an object of a certain type.
$x = y$ is an equality-type. To proove this equality means to create an object of the equality-type. \

$x ≡ y$ definitional equality - does not correspond to a type
$x$ and $y$ can constructed from the definition of their type using the type-constructor. I.e. they’re basically constructed “the same way” \

$x = y$ propositional equality
if x and y are definitionally equal then an associated propositionally equal element can be deduced from this. \

Theorem:

• for every function $f$ there is a function $ap-f: (x = y) → (f(x) = f(y))$
• from (an element of the type) $(x = y)$ the $ap-f$ is going to construct

(an element of the type) $(f(x) = f(y))$

• in logic the funtion $ap-f$ corresponds to an implication. In general in the

type theory a funtion is nothing else than an implication

Classical logic and type theory correspondence
Type theory searches for construction of a type-dependent function $f$ (or $z$) …:

classical logic	type theory	notation
∀ n ∀ m (n+m = m+n)	f:(n,m) → (n+m = m+n)	f: Π n:N π m:N (n+m = m+n)
∃ n ∀ m (n+m = m)		z: Σ n:N σ m:N (n+m = m)

Simplified Categorical view of functions and types:

• Functions: arrows between objects
• Types: objects whose properties are defined by arrows
• Composition, associativity, identity: see Group-like structures

Composition $\comp$: read as “this function after that function”
No deeper specification of what the functions and objects are.

Mapping between Category Theory and Functional Programming:

Views → Change of perspective

• Set-theoretical: properties of sets defined by elems of sets
• Categorical: Shrink the set to a point “I can’t look at the structure of a set”

Describe different kinds of sets by their interraction with other sets, i.e. by arrows.
Tell me who your friends are and I tell you who you are. \

Phenomenons of Introduction / Construction and Elimination
Constructors build values, eliminators take apart values (build by constructors).

Data types:

• Void (empty set): we don’t know that it has no elems; describe/define the props

using arrows, i.e. saying something universal; universal property UP initial obj: Univ prop: unique(1.) arrow to every(2.) single other obj (corresponds to falsehood in logic)

• intro: can’t be constructed (can’t construct a fn returning an elem of empty set)

??? Identity fn on void ???

• elim: Void → A (arrow from; polymorphic fn - works for any type)

Unit (one-elem set): univ prop: terminal obj (opposite i.e. dual to init-obj); Duality - invert the arrows and you get something for free

intro: A → Unit (fn: just ignore the fn input)

elim: Unit → A (fn: pick one elem of a type i.e. set; some sort of “cheating” - instead of an elem we pick a morphism)

Cartesian(?) Product

• https://youtu.be/8AGWTWVOJ74?t=1329 “I have one thing, I have another thing and now I have two things”
• set of all pairs: UP (universal construction) - best product triangle: for all

other types there’s the unique arrow projections: $f: C → A$, $g: C → B$

• tuple (pair aka record) is better than tripple ??? loop-over-all-types: for each of

all possible types: 38:20

intro: $A → B → (A,B)$ tupple

elim: tupple $(A,B) → A; (A,B) → B$

Relation

A subset of a Cartesian Product; doesn’t have a directionality; n-to-n relation

Sum type (dual to product - coproduct)

intro: A → either A or B, B → either A or B

elim: case e of: left a → f a, right b → f b

in functional programming - tagged unions

Monoidal category

Has objects, arrows and product; looks kinda like multiplication / addition
Algebra of types … \ (ADT - abstract algebraic data type) \

Monoidal category has:

• categorical product $\tensor$ s.t. $\cat{C} \tensor \cat{C} → \cat{C}$ i.e. tensor product.
• terminal object $\const{I}$ s.t. $\const{I} \tensor c = c \tensor \const{I} = c$ for every $c ∈ \Ob(\cat{C})$, i.e. unit object.

Functor

Structure preserving mapping $\Fun{F}: \cat{C} → \cat{D}$ between two categories (objects to objects, morphisms to morphisms): i.e. if there’s an arrow $c_1 → c_2$, then there must be arrow $\Fun{F}c_1 → \Fun{F}c_2$ where $\Fun{F}c_i ∈ \Ob(\cat{D})$.

A functor may collapse things, preserves unit object and composition.

Endofunctor:
Mapping $\cat{C} → \cat{C}$ from the same Cat to the same Cat. Endo ~ inside, “Endoscopy”

Functor category

Functors between two categories $\cat{C}$, $\cat{D}$ form a Functor category $[\cat{C},\cat{D}]$ where:

• Objects are functors
• Morphisms are natural transformations between functors

Endofunctor category:
$[\cat{C},\cat{C}]$ is a category of functors from $\cat{C}$ to $\cat{C}$.

Adjoints, Adjunctions, Adjointness

Adjunction: a relationship between two functors.
Adjoints / adjoint functors - functors with a relation of adjunction between them.

A pair of functors $\Fun{F}$, $\Fun{G}$: $\Fun{F}$ is adjunct (but not inverse) to $\Fun{G}$.

Object in a Category of Types such that: For every $A$, $B$ there is a set of arrows from $A$ to $B$. This obj is called function-type. It can be defined by an adjunction of two endofunctors.

\begin{center} \begin{tikzcd} A \arrow[rr, “F”’, bend left] \arrow[d, “\bar{g}”’, dotted] \arrow[dd, “G(q) ˆ \bar{g}”’, dotted, bend right=60] & & F(A) \arrow[d, “g”, dotted] \arrow[dd, “q ˆ g”, dotted, bend left=60] \arrow[ll, “G”’, bend left]
G(B) \arrow[d, “G(q)”’, dotted] \arrow[rr, “F”’, bend left] & & B \arrow[d, “q”, dotted] \arrow[ll, “G”’, bend left] \ G(B’) \arrow[rr, “F”’, bend left] & & B’ \arrow[ll, “G”’, bend left] \end{tikzcd} \end{center}

Functor $F$ is left adjoint to the functor $G$: $F \ladj G$ and $G$ is right adjoint to $F$: $G \radj F$

$$m_C \iso n_D$$ $$\cat{C}(C_1, GD_2) ≅ \cat{D}(FC_1, D_2)$$

Left adjointness $\ladj$

morphisms $m_C$, $n_D$ in the categories $\cat{C}$, $\cat{D}$ are drawn from the top to the bottom, functor components $F_1$, $G_2$ are drawn clockwise. (Components $F_2$, $G_1$ are not drawn.)

\begin{center} \begin{tikzcd} C_1= GD_1 \arrow[rrr, “F_1”’, bend left] \arrow[dd, “m_C = Gn_D”’, dotted] \arrow[“Id_{C_1}”’, dotted, loop, distance=2em, in=125, out=55] & & & D_1 = FC_1 \arrow[dd, “n_D = Fm_C”, dotted] \arrow[lll, “G_1”’, bend left] \arrow[“Id_{D_1}”’, dotted, loop, distance=2em, in=125, out=55]
& & & \ C_2 = GD_2 \arrow[rrr, “F_2”’, bend left] \arrow[“Id_{C_2}”’, dotted, loop, distance=2em, in=305, out=235] & & & D_2 = FC_2 \arrow[lll, “G_2”’, bend left] \arrow[“Id_{D_2}”’, dotted, loop, distance=2em, in=305, out=235] \end{tikzcd} \end{center}

It’s more interesting if F, G are not an inverse of each other

F left adjoing to G:

left side: prepare an argument for some function using functor F

right side: modifying the output of some function using functor G

F A === (A, C) ftor F acts on A and creates a pair type (A, C) G B === C → B ftor G acts on B and creates a function type from C to B

Currying arrises from an Adjunction: (A, C) → B is isomorphic (i.e. equivalent) to A → (C → B)

If you have a pairing (product) and if you have such an adjunction in your Cat then you are able to define a function type (en exponential).

A Cat with such pairing and adjunction is called cartesian closed (i.e. this Cat has a function type)

function intro: lambda

function elim: eval

Natural transformations

NaTs: Polymorphic functions: mapping between ftors. See a [picture](https://youtu.be/JH_Ou17_zyU?t=1h6m23s)

Polymorphic function

a function for every single type i.e. multiplication (Product) of all obj in a category. Also the dual - the Sum

Categorical End (i.e. Product) and CoEnd (i.e. CoProduct i.e. Sum)

notation is the integral sign

Monadic return-function

universally polymorphic function - works for any type \href{https://www.youtube.com/watch?v=CfoaY2Ybf8M&t=7m}{B. Milewski: 7:00}

Generalization of everything. They sub-sume everything else, like adjuctions at a higher level

Limits, Colimits, Monads Adjunctions can be redefined as Khan Extentions

Intuition of Khan Extentions is difficult - they are more abstract than monads Adjunction between a Product and a Function Type is Currying

Product generalization: Tensor Product in a monoidal category

Generalizations

Get rid of:

• distinct objects you get a monoid.
• composition/identity being always defined you get a paracategory. If you generalize composition as in “many morphisms can be composed together” you get an operad.
• idea of composition/identity laws having to hold with equality you get higher categories.

Category theory - definition dependencies

Based on definitions in The Joy of Cats. https://www.johndcook.com/blog/category_theory/

N-Categories

\href{https://youtu.be/6bnU7_6CNa0}{Tom Leinster: “An introduction to n-categories”}

\href{https://youtu.be/6bnU7_6CNa0?t=3369}{56:09}
$-2$ -Category: There’s only one. (Tom provides no explanation in the video.) \ $-1$ -Category: Boolean truth values, i.e. there are two $-1$ categories: $True$, $False$. \ $+0$ -Category: set \ $+1$ -Category: …

Vertical and horizontal composition of NaTs

Probably erroneous. See \href{https://arxiv.org/pdf/1612.09375.pdf}{page 38},

\begin{center} \begin{tikzcd} F’(F(X)) \arrow[rrrrr, “F’(F(f))”’, dotted, bend left] \arrow[ddd, “(α’ * α)_X” description, Rightarrow] & & & & & F’(F(Y)) \arrow[ddd, “(α’ * α)_Y” description, Rightarrow]
& & & & & \ & & F(X) \arrow[d, “α_X” description, Rightarrow] \arrow[r, “F(f)”’, dotted] \arrow[lluu, “(F’ \comp F)_X” description] & F(Y) \arrow[d, “α_Y” description, Rightarrow] \arrow[rruu, “(F’ \comp F)_Y” description] & {} & {} \ G’(G(X)) \arrow[ddd, “(β’ * β)_X” description, Rightarrow] \arrow[rrrrr, “G’(G(f))”, dotted, bend left=49] & & G(X) \arrow[d, “β_X” description, Rightarrow] \arrow[r, “G(f)”’, dotted] \arrow[ll, “(G’ \comp G)_X”’] & G(Y) \arrow[d, “β_Y” description, Rightarrow] \arrow[rr, “(G’ \comp G)_Y”] & & G’(G(Y)) \arrow[ddd, “(β’ * β)_Y” description, Rightarrow] \ & & H(X) \arrow[r, “H(f)”’, dotted] \arrow[lldd, “(H’ \comp H)_X” description] & H(Y) \arrow[rrdd, “(H’ \comp H)_Y” description] & & \ & & & & & \ H’(H(X)) \arrow[rrrrr, “H’(H(f))” description, dotted] & & & & & H’(H(Y)) \end{tikzcd} \end{center}

\begin{center} \begin{tikzcd} X \arrow[rrrr, “f”] & {} \arrow[rrddddd, “H”, dotted] & {} \arrow[rdddd, “G”, dotted] & {} \arrow[ddd, “F”, dotted] & Y & & & & & &
& & & & & & & F’(F(X)) \arrow[rrr, “F’(F(f))”] \arrow[d, “α’_X”’, Rightarrow] \arrow[dd, “(β’ \comp α’)_X”’, Rightarrow, bend right=71] & {} & & F’(F(Y)) \arrow[d, “α’_Y”’, Rightarrow] \ & & & & & & & G’(G(X)) \arrow[d, “β’_X”’, Rightarrow] \arrow[rrr, “G’(G(f))”] & {} & & G’(G(Y)) \arrow[d, “β’_Y”’, Rightarrow] \ & & F(X) \arrow[d, “α_X”’, Rightarrow] \arrow[rrr, “F(f)”’] \arrow[dd, “(β \comp α)_X”’, Rightarrow, bend right=74] & {} & {} \arrow[rrrruu, “F’”’, dotted] & F(Y) \arrow[d, “α_Y”’, Rightarrow] & & H’(H(X)) \arrow[rrr, “H’(H(f))”] & {} & & H’(H(Y)) \ & & G(X) \arrow[d, “β_X”’, Rightarrow] \arrow[rrr, “G(f)”’] & {} & {} \arrow[rrrruu, “G’”’, dotted] & G(Y) \arrow[d, “β_Y”’, Rightarrow] & & & & & \ & & H(X) \arrow[rrr, “H(f)”’] & {} & {} \arrow[rrrruu, “H’”’, dotted] & H(Y) & & & & & \end{tikzcd} \end{center}

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZARgBoAGAXVJADcBDAGwFcYkQAhAAgB0e8AtvC4cQAX1LpMufIRTlSxanSat2oiVOx4CRAEyLlDFm0SdxkkBm2yiZPUdWnzmq9J1ySpAMyOT7AEELLRldFDIAVj81MwDefiwhOC4g12tQzwUAFmjnVMt0j31SHJpjGJB8kKKUA18yp3Zgtxsw5AV6lX8zcWUYKABzeCJQADMAJwgBJCyaHAgkCJpGLDBnKHo4AAt+kAbukD4YAA8sOBw4AEIAfSqQCamkbzmFxAUQFbX2De3d-YqjqdzldrqIaDt6FAkGBmIxGHN6FhGOxIF9XA9pm8XkgDB9Vs44BAVlDwTBIdDYfCQDhEcizKi2P9nHw0FhrsA9KCxM0MUh3vMkGQ8V8zITiXsQBCoYgYXCEUiUQRGV0ATxWeziFyJYx6AAjGCMAAK7lsZnGWAGWxwPMmmNm1NezxVzlG2r1BuNrTkIFW2FgNseiAAbNjEELyi63fqjSawh8YKNrejbUgAOyh3ER9iu5bumNe9jmy1Jyy84Oh+2fdYQZi6xjKqWKr7yungJUBu2h9PC6u1+sSxv09stptsZOBpYOtNM9gstkc27c3PRz0ZQsWq0dxahkPO2dq+eagLc8eYp0CsPLfHfGt1htk6Vt5vU2mjreIc+vXFVm99+-kodnxpBVALHUsU0Qe0LwADivEUQCgW9+1JACn2VYDWwZCVtiwRMkAAWgATlPGZQ0IuDezvAcHzfEdQOwrZcOtRBiMoMQgA \begin{tikzcd} & B × B \arrow[rd, “π_{2_B}”] \arrow[ld, “π_{1_B}”’] &
B & & B \ & B \arrow[uu, “∃!_B”, dashed] \arrow[lu, no head, Rightarrow] \arrow[ru, no head, Rightarrow] & \ {} & A \arrow[dd, “∃!_A”, dashed] \arrow[u, “f” description] \arrow[rd, no head, Rightarrow] \arrow[r, no head, Rightarrow, shift left=9] \arrow[l, no head, Rightarrow, shift right=9] & {} \ A \arrow[uuu, “f”] \arrow[ru, no head, Rightarrow] & & A \arrow[uuu, “f”’] \ & A × A \arrow[ru, “π_{2_A}”’] \arrow[lu, “π_{1_A}”] & \end{tikzcd}

Effect in Functional Programming

An effect is the thing that a monad handles. (Typically an IO operation)

Option is a monad that models the effect of optionality (of something being optional) Future is a monad that models latency (oneskorenie, cakacia doba) as an effect Try is a monad that models the effect of failures (manages exceptions as effects) Reader is a monad that models the effect of composing operations that depend on some input Writer is a monad that models logging as an effect State is a monad that models the effect of state (composing a series of computations that maintain state)

effectful function is a function that returns F[A] rather than [A]

Terminal and initial categories

A category may server as a terminal and/or initial category. We assume that such a category has a has a single object. It must have the identity morphism, but probably it may have some other morphism(s) on this singleton object.

Lindenbaum category

tool for exploring the connections between logic, algebra, and category theory.

Lindenbaum construction

can be used to create a category where:

• The objects are formulas or propositions within the theory, sometimes considered up to logical equivalence (two formulas are equivalent if the theory proves them to be either both true or both false).
• The morphisms represent logical implications or derivations between these formulas.

Gödel’s incompleteness theorems

First

Some true statements cannot be proven

Second

a theory with ×, + operations (products and sums) may lead to be inconsistencies

diagramatische komposition ; ˆ

global elements siehe Wikipedia A morphism from the terminal object to a given object (to which it is said to belong).