# functor

Functor package contains functor implementation and laws packed in Sigma container.

```
functor (F: U -> U): U
= (fmap: (A B: U) -> (A -> B) -> F A -> F B)
* (id: (A: U) -> (x: F A) -> Path (F A) (fmap A A (idfun A) x) x)
* (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F A) ->
Path (F C) (fmap A C (o A B C f g) x)
((o (F A) (F B) (F C) (fmap B C f) (fmap A B g)) x)) * Unit
```

The package also contains proof-free code for runtime facilities.

```
functor_ (A B: U) (F: U -> U): U
= (fmap: (A -> B) -> F A -> F B) * Unit
```

# Implementation

## fmap

`fmap: (A B: U) -> (A -> B) -> F A -> F B`

For a given function, its domain and codomain, the fmap returns a function on domain and codomain that are constructed by applying a functor to original domain and codomain.

# Laws

## id

```
id: (A: U) -> (x: F A) ->
Path (F A) (fmap A A (idfun A) x) x
```

Functorial id law states that fmap preserves the id functions. I.e. applying a functor to types should preserve the identity properties.

## compose

```
compose (A B C: U) (f: B -> C) (g: A -> B) (x: F A) ->
Path (F C) (fmap A C (o A B C f g) x)
((o (F A) (F B) (F C) (fmap B C f) (fmap A B g)) x)
```

Functorial Compose law states that fmap preserves the composition over functors applied to types. I.e. when you have composition of two functions, functor will preserve its composition.

# Functor Instances

## Id Type

```
idtype (A: U): U = A
```

## Const Type

```
consttype (A B: U): U = A
```

## Function Type

```
functiontype (A B: U): U = A -> B
```

## Composition Type

`comptype (F G: U -> U) (t: U): U = F (G t)`