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)