ðŸŽ‰ FUN WITH CATEGORIES ðŸŽ‰
What is category theory?
general setting to speak about composition and computation
provides concepts as `Functor`

, `Monad`

, `Natural Transformation`

Category Theory is indeed general abstract nonsense
and that it is precisely because of that that it is
so important both mathematically and philosophically.

from "What is Category Theory?"

by Jean-Pierre Marquis

what is category theory?

even among mathematicians sometimes described as abstract nonsense

but that is good because:

A Category Theory library
statebox/idris-ct

practically usable
verified
we need to have the same safety which math provides (even more, because proof checked)

still, not too abstract so that it becomes inpractical

Types allow us to encode proofs
```
data LTE : (n, m : Nat) -> Type where
LTEZero : LTE Z right
LTESucc : LTE left right -> LTE (S left) (S right)
```

Haskell

`head : List A -> A`

Safer Haskell

`headMaybe : List A -> Maybe A`

Idris

`nonEmptyHead : (l : List A ** IsNonEmpty l) -> A`

Mapping objects

Mapping morphisms

Make a category out of it

Map out of it with a functor

Map out of it with a functor

Map out of it with a functor

Recap
Categorise it
Add a semantic
ðŸŽ‰ HAVE FUN ðŸŽ‰