functor

IsFunctorId

def IsFunctorId (F : Type -> Type) (fmap : (A : Type) -> (B : Type) -> (A -> B) -> F A -> F B) : Type 1

The functor identity law for fmap: mapping the identity function leaves every value unchanged.

IsFunctorComp

def IsFunctorComp (F : Type -> Type) (fmap : (A : Type) -> (B : Type) -> (A -> B) -> F A -> F B) : Type 1

The functor composition law for fmap, stated pointwise: fmap (g ∘ f) x = fmap g (fmap f x).

IsFunctor

def IsFunctor (F : Type -> Type) (fmap : (A : Type) -> (B : Type) -> (A -> B) -> F A -> F B) : Type 1

The type saying fmap makes F a lawful functor: both the identity and composition laws hold.

IsMonadLeftId

def IsMonadLeftId (M : Type -> Type) (ret : (A : Type) -> A -> M A) (bnd : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B) : Type 1

The monad left identity law: bind (return a) f = f a.

IsMonadRightId

def IsMonadRightId (M : Type -> Type) (ret : (A : Type) -> A -> M A) (bnd : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B) : Type 1

The monad right identity law: bind m return = m.

mapOptionFull

def mapOptionFull (A : Type) (B : Type) (f : A -> B) (mx : Option A) : Option B

The functor map for Maybe with explicit type arguments: applies f inside just, keeps nothing.

optionMapId

def optionMapId (A : Type) (mx : Option A) : mapOptionFull A A (fun (x : A) => x) mx ≡ mx

Mapping the identity over a Maybe leaves it unchanged.

optionMapComp

def optionMapComp (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> C) (mx : Option A) : mapOptionFull A C (fun (a : A) => g (f a)) mx ≡ mapOptionFull B C g (mapOptionFull A B f mx)

Mapping over Maybe respects composition: map (g ∘ f) = map g ∘ map f.

optionIsFunctor

def optionIsFunctor : IsFunctor Option mapOptionFull

Maybe with mapMaybeFull is a lawful functor.

optionReturn

def optionReturn (A : Type) (a : A) : Option A

The monadic return for Maybe: wraps a value in just.

optionBind

def optionBind (A : Type) (B : Type) (mx : Option A) (f : A -> Option B) : Option B

The monadic bind for Maybe: passes the contained value to f, or propagates nothing.

optionLeftId

def optionLeftId (A : Type) (B : Type) (a : A) (f : A -> Option B) : optionBind A B (optionReturn A a) f ≡ f a

The Maybe monad satisfies left identity: bind (return a) f = f a.

optionRightId

def optionRightId (A : Type) (mx : Option A) : optionBind A A mx (optionReturn A) ≡ mx

The Maybe monad satisfies right identity: bind m return = m.

optionAssoc

def optionAssoc (A : Type) (B : Type) (C : Type) (mx : Option A) (f : A -> Option B) (g : B -> Option C) : optionBind B C (optionBind A B mx f) g ≡ optionBind A C mx (fun (a : A) => optionBind B C (f a) g)

The Maybe monad’s bind is associative: bind (bind m f) g = bind m (fun a => bind (f a) g).

optionIsMonadLeftId

def optionIsMonadLeftId : IsMonadLeftId Option optionReturn optionBind

Maybe with maybeReturn and maybeBind satisfies the monad left identity law.

mapListFull

def mapListFull (A : Type) (B : Type) (f : A -> B) (xs : List A) : List B

The functor map for List with explicit type arguments: applies f to every element.

listMapId

def listMapId (A : Type) (xs : List A) : mapListFull A A (fun (x : A) => x) xs ≡ xs

Mapping the identity over a list leaves it unchanged.

listMapComp

def listMapComp (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> C) (xs : List A) : mapListFull A C (fun (a : A) => g (f a)) xs ≡ mapListFull B C g (mapListFull A B f xs)

Mapping over a list respects composition: map (g ∘ f) = map g ∘ map f.

listIsFunctor

def listIsFunctor : IsFunctor List mapListFull

List with mapListFull is a lawful functor.

listReturn

def listReturn (A : Type) (a : A) : List A

The monadic return for List: the singleton list.

concatMapList

def concatMapList (A : Type) (B : Type) (xs : List A) (f : A -> List B) : List B

The monadic bind for List (flatMap): applies f to each element and concatenates the results.

concatMapListRightId

def concatMapListRightId (A : Type) (xs : List A) : concatMapList A A xs (fun (x : A) => cons x nil) ≡ xs

Binding a list with the singleton function gives back the list.

listLeftId

def listLeftId (A : Type) (B : Type) (a : A) (f : A -> List B) : concatMapList A B (listReturn A a) f ≡ f a

The List monad satisfies left identity: bind [a] f = f a.

listRightId

def listRightId (A : Type) (xs : List A) : concatMapList A A xs (listReturn A) ≡ xs

The List monad satisfies right identity: bind xs return = xs.

idFmap

def idFmap (A : Type) (B : Type) (f : A -> B) (x : A) : B

The functor map of the identity functor: plain function application.

idMapId

def idMapId (A : Type) (x : A) : idFmap A A (fun (a : A) => a) x ≡ x

The identity functor satisfies the functor identity law.

idMapComp

def idMapComp (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> C) (x : A) : idFmap A C (fun (a : A) => g (f a)) x ≡ idFmap B C g (idFmap A B f x)

The identity functor satisfies the functor composition law.

mapOptionSome

def mapOptionSome (A : Type) (B : Type) (f : A -> B) (x : A) : mapOptionFull A B f (some x) ≡ some (f x)

Mapping over just x gives just (f x).

concatMapListNil

def concatMapListNil (A : Type) (B : Type) (f : A -> List B) : concatMapList A B (nil : List A) f ≡ (nil : List B)

Binding the empty list gives the empty list.

mapOptionFullCompSome

def mapOptionFullCompSome (f : Nat -> Nat) (g : Nat -> Nat) (x : Nat) : mapOptionFull Nat Nat f (mapOptionFull Nat Nat g (some x)) ≡ mapOptionFull Nat Nat (fun (a : Nat) => f (g a)) (some x)

Mapping two functions in turn over just x equals mapping their composite (on Nat).

mapOptionFullCompNone

def mapOptionFullCompNone (f : Nat -> Nat) (g : Nat -> Nat) : mapOptionFull Nat Nat f (mapOptionFull Nat Nat g (none : Option Nat)) ≡ mapOptionFull Nat Nat (fun (a : Nat) => f (g a)) (none : Option Nat)

Mapping two functions in turn over nothing equals mapping their composite (on Nat).

optionBindNone

def optionBindNone (A : Type) (B : Type) (f : A -> Option B) : optionBind A B (none : Option A) f ≡ (none : Option B)

Binding nothing gives nothing.

optionBindSome

def optionBindSome (A : Type) (B : Type) (a : A) (f : A -> Option B) : optionBind A B (some a) f ≡ f a

Binding just a applies the continuation: bind (just a) f = f a.

concatMapListCons

def concatMapListCons (A : Type) (B : Type) (x : A) (xs : List A) (f : A -> List B) : concatMapList A B (cons x xs) f ≡ append (f x) (concatMapList A B xs f)

Binding a cons list: bind (x :: xs) f = f x ++ bind xs f.

kleisliOption

def kleisliOption (A : Type) (B : Type) (C : Type) (f : A -> Option B) (g : B -> Option C) (a : A) : Option C

Kleisli composition for Maybe: run f, then feed its result to g.

kleisliList

def kleisliList (A : Type) (B : Type) (C : Type) (f : A -> List B) (g : B -> List C) (a : A) : List C

Kleisli composition for List: run f, then bind every result through g.

headOptionNatural

def headOptionNatural (A : Type) (B : Type) (f : A -> B) (xs : List A) : mapOptionFull A B f (headOption xs) ≡ headOption (mapListFull A B f xs)

headMaybe is natural: taking the head commutes with mapping a function.

optionToListNatural

def optionToListNatural (A : Type) (B : Type) (f : A -> B) (mx : Option A) : mapListFull A B f (Option.toList A mx) ≡ Option.toList B (mapOptionFull A B f mx)

maybeToList is natural: converting to a list commutes with mapping a function.

optionMapIdNat

def optionMapIdNat (mx : Option Nat) : mapOptionFull Nat Nat (fun (x : Nat) => x) mx ≡ mx

The Maybe functor identity law specialized to Nat.

optionMapIdBool

def optionMapIdBool (mx : Option Bool) : mapOptionFull Bool Bool (fun (x : Bool) => x) mx ≡ mx

The Maybe functor identity law specialized to Bool.

optionMapCompSuccSucc

def optionMapCompSuccSucc (mx : Option Nat) : mapOptionFull Nat Nat (fun (a : Nat) => succ (succ a)) mx ≡ mapOptionFull Nat Nat succ (mapOptionFull Nat Nat succ mx)

The Maybe functor composition law for succ after succ.

listMapIdNat

def listMapIdNat (xs : List Nat) : mapListFull Nat Nat (fun (x : Nat) => x) xs ≡ xs

The List functor identity law specialized to Nat.

listMapIdBool

def listMapIdBool (xs : List Bool) : mapListFull Bool Bool (fun (x : Bool) => x) xs ≡ xs

The List functor identity law specialized to Bool.

listMapCompSuccSucc

def listMapCompSuccSucc (xs : List Nat) : mapListFull Nat Nat (fun (a : Nat) => succ (succ a)) xs ≡ mapListFull Nat Nat succ (mapListFull Nat Nat succ xs)

The List functor composition law for succ after succ.

bimapPair

def bimapPair (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> C) (g : B -> D) (p : A × B) : C × D

Maps both components of a pair: (a, b) goes to (f a, g b).

bimapPairId

def bimapPairId (A : Type) (B : Type) (p : A × B) : bimapPair A B A B (fun (a : A) => a) (fun (b : B) => b) p ≡ p

Mapping identities over both components leaves a pair unchanged.

bimapPairComp

def bimapPairComp (A : Type) (B : Type) (C : Type) (D : Type) (E : Type) (F : Type) (f1 : A -> C) (f2 : C -> E) (g1 : B -> D) (g2 : D -> F) (p : A × B) : bimapPair C D E F f2 g2 (bimapPair A B C D f1 g1 p) ≡ bimapPair A B E F (fun (a : A) => f2 (f1 a)) (fun (b : B) => g2 (g1 b)) p

Bimapping a pair respects composition in both components.

firstPair

def firstPair (A : Type) (B : Type) (C : Type) (f : A -> C) (p : A × B) : C × B

Maps the first component of a pair, keeping the second.

secondPair

def secondPair (A : Type) (B : Type) (D : Type) (g : B -> D) (p : A × B) : A × D

Maps the second component of a pair, keeping the first.

firstPairId

def firstPairId (A : Type) (B : Type) (p : A × B) : firstPair A B A (fun (a : A) => a) p ≡ p

Mapping the identity over the first component leaves a pair unchanged.

secondPairId

def secondPairId (A : Type) (B : Type) (p : A × B) : secondPair A B B (fun (b : B) => b) p ≡ p

Mapping the identity over the second component leaves a pair unchanged.

dimapFn

def dimapFn (A : Type) (B : Type) (C : Type) (D : Type) (f : C -> A) (g : B -> D) (h : A -> B) : C -> D

The profunctor map for functions: precompose with f and postcompose with g, giving g ∘ h ∘ f.

dimapFnId

def dimapFnId (A : Type) (B : Type) (h : A -> B) (a : A) : dimapFn A B A B (fun (x : A) => x) (fun (y : B) => y) h a ≡ h a

Dimapping identities over a function leaves it unchanged at every point.

lmapFn

def lmapFn (A : Type) (B : Type) (C : Type) (f : C -> A) (h : A -> B) : C -> B

Maps the input side of a function: precomposes h with f.

rmapFn

def rmapFn (A : Type) (B : Type) (D : Type) (g : B -> D) (h : A -> B) : A -> D

Maps the output side of a function: postcomposes h with g.

mapEitherRight

def mapEitherRight (E : Type) (A : Type) (B : Type) (f : A -> B) (ea : Either E A) : Either E B

The functor map for Either over its right component: applies f to right values, keeps left values.

mapEitherRightId

def mapEitherRightId (E : Type) (A : Type) (ea : Either E A) : mapEitherRight E A A (fun (a : A) => a) ea ≡ ea

Mapping the identity over the right of an Either leaves it unchanged.

mapEitherRightComp

def mapEitherRightComp (E : Type) (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> C) (ea : Either E A) : mapEitherRight E A C (fun (a : A) => g (f a)) ea ≡ mapEitherRight E B C g (mapEitherRight E A B f ea)

Mapping over the right of an Either respects composition.

constFmap

def constFmap (C : Type) (A : Type) (B : Type) (f : A -> B) (c : C) : C

The functor map of the constant functor at C: ignores f and returns the value unchanged.

constFmapId

def constFmapId (C : Type) (A : Type) (c : C) : constFmap C A A (fun (a : A) => a) c ≡ c

The constant functor satisfies the functor identity law.

constFmapComp

def constFmapComp (C : Type) (A : Type) (B : Type) (D : Type) (f : A -> B) (g : B -> D) (c : C) : constFmap C A D (fun (a : A) => g (f a)) c ≡ constFmap C B D g (constFmap C A B f c)

The constant functor satisfies the functor composition law.

mapViaBindOption

def mapViaBindOption (A : Type) (B : Type) (f : A -> B) (mx : Option A) : mapOptionFull A B f mx ≡ optionBind A B mx (fun (a : A) => some (f a))

Mapping over Maybe is binding with just ∘ f.

bindMapOption

def bindMapOption (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> Option C) (mx : Option A) : optionBind B C (mapOptionFull A B f mx) g ≡ optionBind A C mx (fun (a : A) => g (f a))

Binding after mapping fuses: bind (map f m) g = bind m (g ∘ f).

mapBindOption

def mapBindOption (A : Type) (B : Type) (C : Type) (f : B -> C) (g : A -> Option B) (mx : Option A) : mapOptionFull B C f (optionBind A B mx g) ≡ optionBind A C mx (fun (a : A) => mapOptionFull B C f (g a))

Mapping after binding moves inside: map f (bind m g) = bind m (fun a => map f (g a)).

mapViaConcatMapList

def mapViaConcatMapList (A : Type) (B : Type) (f : A -> B) (xs : List A) : mapListFull A B f xs ≡ concatMapList A B xs (fun (a : A) => cons (f a) nil)

Mapping over a list is binding with the singleton of f.

compFmapOptionList

def compFmapOptionList (A : Type) (B : Type) (f : A -> B) (xs : Option (List A)) : Option (List B)

The functor map of the composite functor Maybe ∘ List.

compFmapId

def compFmapId (A : Type) (xs : Option (List A)) : compFmapOptionList A A (fun (a : A) => a) xs ≡ xs

The composite functor Maybe ∘ List satisfies the functor identity law.

optionIsMonadRightId

def optionIsMonadRightId : IsMonadRightId Option optionReturn optionBind

Maybe with maybeReturn and maybeBind satisfies the monad right identity law.

headOptionOptionToList

def headOptionOptionToList (A : Type) (mx : Option A) : headOption (Option.toList A mx) ≡ mx

Converting a Maybe to a list and taking its head gives back the Maybe.

headOptionSingleton

def headOptionSingleton (A : Type) (x : A) : headOption (cons x nil) ≡ some x

The head of a singleton list is just its element.

optionToListNone

def optionToListNone (A : Type) : Option.toList A (none : Option A) ≡ (nil : List A)

Converting nothing to a list gives the empty list.

optionToListSome

def optionToListSome (A : Type) (x : A) : Option.toList A (some x) ≡ cons x (nil : List A)

Converting just x to a list gives the singleton list [x].

compFmapListOption

def compFmapListOption (A : Type) (B : Type) (f : A -> B) (xs : List (Option A)) : List (Option B)

The functor map of the composite functor List ∘ Maybe.

compFmapLMId

def compFmapLMId (A : Type) (xs : List (Option A)) : compFmapListOption A A (fun (a : A) => a) xs ≡ xs

The composite functor List ∘ Maybe satisfies the functor identity law.

bimapEither

def bimapEither (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> C) (g : B -> D) (e : Either A B) : Either C D

Maps both sides of an Either: f on left values, g on right values.

bimapEitherId

def bimapEitherId (A : Type) (B : Type) (e : Either A B) : bimapEither A B A B (fun (a : A) => a) (fun (b : B) => b) e ≡ e

Bimapping identities over an Either leaves it unchanged.

bimapEitherComp

def bimapEitherComp (A : Type) (B : Type) (C : Type) (D : Type) (E : Type) (F : Type) (f1 : A -> C) (f2 : C -> E) (g1 : B -> D) (g2 : D -> F) (e : Either A B) : bimapEither C D E F f2 g2 (bimapEither A B C D f1 g1 e) ≡ bimapEither A B E F (fun (a : A) => f2 (f1 a)) (fun (b : B) => g2 (g1 b)) e

Bimapping an Either respects composition on both sides.

firstPairComp

def firstPairComp (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> C) (g : C -> D) (p : A × B) : firstPair C B D g (firstPair A B C f p) ≡ firstPair A B D (fun (a : A) => g (f a)) p

Mapping the first component twice equals mapping the composite once.

secondPairComp

def secondPairComp (A : Type) (B : Type) (C : Type) (D : Type) (f : B -> C) (g : C -> D) (p : A × B) : secondPair A C D g (secondPair A B C f p) ≡ secondPair A B D (fun (b : B) => g (f b)) p

Mapping the second component twice equals mapping the composite once.

firstSecondComm

def firstSecondComm (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> C) (g : B -> D) (p : A × B) : firstPair C D C (fun (c : C) => c) (secondPair C B D g (firstPair A B C f p)) ≡ secondPair C B D g (firstPair A B C f p)

Mapping the identity over the first component after mapping both components changes nothing.

bimapPairViaFirstSecond

def bimapPairViaFirstSecond (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> C) (g : B -> D) (p : A × B) : bimapPair A B C D f g p ≡ secondPair C B D g (firstPair A B C f p)

Bimapping a pair is mapping the first component and then the second.

kleisliLeftIdOption

def kleisliLeftIdOption (A : Type) (B : Type) (f : A -> Option B) (a : A) : kleisliOption A A B (optionReturn A) f a ≡ f a

Return is a left identity for Kleisli composition in Maybe.

optionAp

def optionAp (A : Type) (B : Type) (mf : Option (A -> B)) (mx : Option A) : Option B

The applicative apply for Maybe: applies a wrapped function to a wrapped value, nothing if either is missing.

optionApId

def optionApId (A : Type) (mx : Option A) : optionAp A A (some (fun (a : A) => a)) mx ≡ mx

The Maybe applicative satisfies the identity law: cong (just id) m = m.

optionApHomo

def optionApHomo (A : Type) (B : Type) (f : A -> B) (x : A) : optionAp A B (some f) (some x) ≡ some (f x)

The Maybe applicative satisfies the homomorphism law: cong (just f) (just x) = just (f x).