# Functors #

This module provides additional lemmas, definitions, and instances for `Functor`

s.

## Main definitions #

`Functor.Const α`

is the functor that sends all types to`α`

.`Functor.AddConst α`

is`Functor.Const α`

but for when`α`

has an additive structure.`Functor.Comp F G`

for functors`F`

and`G`

is the functor composition of`F`

and`G`

.`Liftp`

and`Liftr`

respectively lift predicates and relations on a type`α`

to`F α`

. Terms of`F α`

are considered to, in some sense, contain values of type`α`

.

## Tags #

functor, applicative

`Const α`

is the constant functor, mapping every type to `α`

. When
`α`

has a monoid structure, `Const α`

has an `Applicative`

instance.
(If `α`

has an additive monoid structure, see `Functor.AddConst`

.)

## Equations

- Functor.Const α _β = α

## Instances For

`Const.mk`

is the canonical map `α → Const α β`

(the identity), and
it can be used as a pattern to extract this value.

## Equations

- Functor.Const.mk x = x

## Instances For

The map operation of the `Const γ`

functor.

## Equations

- Functor.Const.map _f x = x

## Instances For

## Equations

- Functor.Const.functor = { map := @Functor.Const.map γ, mapConst := fun {α β : Type u_2} => Functor.Const.map ∘ Function.const β }

## Equations

- ⋯ = ⋯

## Equations

- Functor.Const.instInhabited = { default := default }

`AddConst α`

is a synonym for constant functor `Const α`

, mapping
every type to `α`

. When `α`

has an additive monoid structure,
`AddConst α`

has an `Applicative`

instance. (If `α`

has a
multiplicative monoid structure, see `Functor.Const`

.)

## Equations

## Instances For

`AddConst.mk`

is the canonical map `α → AddConst α β`

, which is the identity,
where `AddConst α β = Const α β`

. It can be used as a pattern to extract this value.

## Equations

- Functor.AddConst.mk x = x

## Instances For

## Equations

- Functor.AddConst.functor = Functor.Const.functor

## Equations

- ⋯ = ⋯

## Equations

- Functor.instInhabitedAddConst = { default := default }

`Functor.Comp`

is a wrapper around `Function.Comp`

for types.
It prevents Lean's type class resolution mechanism from trying
a `Functor (Comp F id)`

when `Functor F`

would do.

## Equations

- Functor.Comp F G α = F (G α)

## Instances For

Construct a term of `Comp F G α`

from a term of `F (G α)`

, which is the same type.
Can be used as a pattern to extract a term of `F (G α)`

.

## Equations

- Functor.Comp.mk x = x

## Instances For

Extract a term of `F (G α)`

from a term of `Comp F G α`

, which is the same type.

## Equations

- x.run = x

## Instances For

The map operation for the composition `Comp F G`

of functors `F`

and `G`

.

## Equations

- Functor.Comp.map h x = match x with | x => Functor.Comp.mk ((fun (x : G α) => h <$> x) <$> x)

## Instances For

## Equations

- Functor.Comp.functor = { map := @Functor.Comp.map F G inst✝ inst, mapConst := fun {α β : Type v} => Functor.Comp.map ∘ Function.const β }

## Equations

- ⋯ = ⋯

The `<*>`

operation for the composition of applicative functors.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- Functor.Comp.instPure = { pure := fun {α : Type v} (x : α) => Functor.Comp.mk (pure (pure x)) }

## Equations

- Functor.Comp.instSeq = { seq := fun {α β : Type v} (f : Functor.Comp F G (α → β)) (x : Unit → Functor.Comp F G α) => f.seq x }

## Equations

- Functor.Comp.instApplicativeComp = Applicative.mk

If we consider `x : F α`

to, in some sense, contain values of type `α`

, then
`Liftr r x y`

relates `x`

and `y`

iff (1) `x`

and `y`

have the same shape and
(2) we can pair values `a`

from `x`

and `b`

from `y`

so that `r a b`

holds.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

If we consider `x : F α`

to, in some sense, contain values of type `α`

, then
`supp x`

is the set of values of type `α`

that `x`

contains.

## Equations

- Functor.supp x = {y : α | ∀ ⦃p : α → Prop⦄, Functor.Liftp p x → p y}

## Instances For

If `f`

is a functor, if `fb : f β`

and `a : α`

, then `mapConstRev fb a`

is the result of
applying `f.map`

to the constant function `β → α`

sending everything to `a`

, and then
evaluating at `fb`

. In other words it's `const a <$> fb`

.

## Equations

- a $> b = Functor.mapConst b a

## Instances For

If `f`

is a functor, if `fb : f β`

and `a : α`

, then `mapConstRev fb a`

is the result of
applying `f.map`

to the constant function `β → α`

sending everything to `a`

, and then
evaluating at `fb`

. In other words it's `const a <$> fb`

.

## Equations

- One or more equations did not get rendered due to their size.