# Equational reasoning

## Example of type restriction

From the Functoriality of Category Theory for Programmers I came across some "equational reasoning" for deriving relation between `>=>`

(fish operator) and `fmap`

.

```
fmap :: Functor f => (a -> b) -> f a -> f b
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
id :: a -> a
-- gives
fmap f = id >=> (\x -> return (f x))
```

Bartosz tries to explain it, but I still don't see it clearly.

"Here, the fish operator combines two functions: one of them is the familiar id, and the other is a lambda that applies return to the result of acting with f on the lambda’s argument. The hardest part to wrap your brain around is probably the use of id. Isn’t the argument to the fish operator supposed to be a function that takes a “normal” type and returns an embellished type? Well, not really. Nobody says that a in a -> Writer b must be a “normal” type. It’s a type variable, so it can be anything, in particular it can be an embellished type, like Writer b.

So id will take Writer a and turn it into Writer a. The fish operator will fish out the value of a and pass it as x to the lambda. There, f will turn it into a b and return will embellish it, making it Writer b. Putting it all together, we end up with a function that takes Writer a and returns Writer b, exactly what fmap is supposed to produce."

One part I don't understand is related to the following.

```
Prelude> let f0 :: a -> Maybe a; f0 a = Just a
Prelude> let f1 :: (a -> Maybe b) -> a -> Maybe b; f1 f a = f a
Prelude> :t f1 f0
f1 f0 :: b -> Maybe b -- this part I do understand
Prelude> :t f1 id
f1 id :: Maybe b -> Maybe b -- but not this one
```

What is the best way to tackle these problems?

I got some help from a college, Lars. The type `Maybe b -> Maybe b`

may be seen as restriction on the more general `a -> Maybe b`

and also `a -> a`

, but they are still compatible types. So `f1 id`

is the same as `f1 f0`

with the additional restriction that first argument is of type `Maybe b`

.

## Group Theory

### Group

Definition: An algebraic structure consisting of a set of elements equipped with an operation that combines two elements to form a third element

Example: Integers (Z) together with addition (.)

Axioms:

- Closure - for
`a`

and`b`

in`G`

`a.b`

is also in`G`

- Associativity -
`(a.b).c = a.(b.c)`

- Unique identity element (
`e`

) -`e.a = a.e = a`

- Inverse element - for every element
`a`

there is an inverse element`b = inv(a)`

(or $$a^-1$$) where`a.b = b.a = e`

#### Cyclic group

A group where all elements are powers of a particlular element `a`

```
e, a, a.a, a.a.a, ...
```

#### Finite group

A group with finite number of elements

#### Category

A group with only associativity (2) and identity (3) axioms required

Note that associativity axiom should be the same as existence of function composition. In other words ...

Category definition: The ability to compose the arrows associatively and the existence of an identity arrow for each object.

### Homomorphism

Definition: a map between two algebraic structures of the same type (that is of the same name), that preserves the operations of the structures

For operation * and mapping f: A -> B this means that

```
f(a * b) = f(A) * f(B)
```

### Isomorphism

Definition: A homomorphism which admits an inverse

if `g`

is the inverse to `f`

then `f.g = id`

i.e. identity morphism

## Inital and terminal object

an initial object of a category `C`

is an object `I`

in `C`

such that for every object `X`

in `C`

,

there exists precisely one morphism `I -> X`

.

`T`

is terminal if for every object `X`

in `C`

there exists a single morphism `X -> T`