control.functor

# Functors

This module provides additional lemmas, definitions, and instances for functors.

## Main definitions

• const α is the functor that sends all types to α.
• add_const α is const α but for when α has an additive structure.
• 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

theorem functor.map_id {F : Type uType v} {α : Type u} [functor F]  :

theorem functor.map_comp_map {F : Type uType v} {α β γ : Type u} [functor F] (f : α → β) (g : β → γ) :

theorem functor.ext {F : Type u_1Type u_2} {F1 F2 : functor F}  :
(∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x)F1 = F2

def id.mk {α : Sort u} :
α → id α

Introduce the id functor. Incidentally, this is pure for id as a monad and as an applicative functor.

Equations
@[nolint]
def functor.const  :
Type u_1Type u_2Type u_1

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.add_const.)

Equations
• = α
def functor.const.mk {α : Type u_1} {β : Type u_2} :
α →

const.mk is the canonical map α → const α β (the identity), and it can be used as a pattern to extract this value.

Equations
def functor.const.mk' {α : Type u_1} :
α →

const.mk' is const.mk but specialized to map α to const α punit, where punit is the terminal object in Type*.

Equations
def functor.const.run {α : Type u_1} {β : Type u_2} :
→ α

Extract the element of α from the const functor.

Equations
theorem functor.const.ext {α : Type u_1} {β : Type u_2} {x y : β} :
x.run = y.runx = y

@[nolint]
def functor.const.map {γ : Type u_1} {α : Type u_2} {β : Type u_3} :
(α → β)

The map operation of the const γ functor.

Equations
• = x
@[instance]
def functor.const.functor {γ : Type u_1} :

Equations
@[instance]
def functor.const.is_lawful_functor {γ : Type u_1} :

@[instance]
def functor.const.inhabited {α : Type u_1} {β : Type u_2} [inhabited α] :

Equations
Type u_1Type u_2Type u_1

add_const α is a synonym for constant functor const α, mapping every type to α. When α has a additive monoid structure, add_const α has an applicative instance. (If α has a multiplicative monoid structure, see functor.const.)

Equations
def functor.add_const.mk {α : Type u_1} {β : Type u_2} :
α →

add_const.mk is the canonical map α → add_const α β, which is the identity, where add_const α β = const α β. It can be used as a pattern to extract this value.

Equations
def functor.add_const.run {α : Type u_1} {β : Type u_2} :
→ α

Extract the element of α from the constant functor.

Equations
@[instance]
def functor.add_const.functor {γ : Type u_1} :

Equations
@[instance]
def functor.add_const.is_lawful_functor {γ : Type u_1} :

@[instance]
def functor.add_const.inhabited {α : Type u_1} {β : Type u_2} [inhabited α] :

Equations
def functor.comp  :
(Type uType w)(Type vType u)Type vType w

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
• G α = F (G α)
def functor.comp.mk {F : Type uType w} {G : Type vType u} {α : Type v} :
F (G α) G α

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
def functor.comp.run {F : Type uType w} {G : Type vType u} {α : Type v} :
G αF (G α)

Extract a term of F (G α) from a term of comp F G α, which is the same type.

Equations
theorem functor.comp.ext {F : Type uType w} {G : Type vType u} {α : Type v} {x y : G α} :
x.run = y.runx = y

@[instance]
def functor.comp.inhabited {F : Type uType w} {G : Type vType u} {α : Type v} [inhabited (F (G α))] :
inhabited G α)

Equations
def functor.comp.map {F : Type uType w} {G : Type vType u} [functor F] [functor G] {α β : Type v} :
(α → β) G α G β

The map operation for the composition comp F G of functors F and G.

Equations
@[instance]
def functor.comp.functor {F : Type uType w} {G : Type vType u} [functor F] [functor G] :

Equations
theorem functor.comp.map_mk {F : Type uType w} {G : Type vType u} [functor F] [functor G] {α β : Type v} (h : α → β) (x : F (G α)) :
=

@[simp]
theorem functor.comp.run_map {F : Type uType w} {G : Type vType u} [functor F] [functor G] {α β : Type v} (h : α → β) (x : G α) :

theorem functor.comp.id_map {F : Type uType w} {G : Type vType u} [functor F] [functor G] {α : Type v} (x : G α) :

theorem functor.comp.comp_map {F : Type uType w} {G : Type vType u} [functor F] [functor G] {α β γ : Type v} (g' : α → β) (h : β → γ) (x : G α) :
functor.comp.map (h g') x = x)

@[instance]
def functor.comp.is_lawful_functor {F : Type uType w} {G : Type vType u} [functor F] [functor G]  :

theorem functor.comp.functor_comp_id {F : Type u_1Type u_2} [AF : functor F]  :

theorem functor.comp.functor_id_comp {F : Type u_1Type u_2} [AF : functor F]  :

def functor.comp.seq {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α β : Type v} :
G (α → β) G α G β

The <*> operation for the composition of applicative functors.

Equations
@[instance]
def functor.comp.has_pure {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] :

Equations
@[instance]
def functor.comp.has_seq {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] :

Equations
@[simp]
theorem functor.comp.run_pure {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α : Type v} (x : α) :
(pure x).run = pure (pure x)

@[simp]
theorem functor.comp.run_seq {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α β : Type v} (f : G (α → β)) (x : G α) :
(f <*> x).run = <*> x.run

@[instance]
def functor.comp.applicative {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] :

Equations
def functor.liftp {F : Type uType u} [functor F] {α : Type u} :
(α → Prop)F α → Prop

If we consider x : F α to, in some sense, contain values of type α, predicate liftp p x holds iff every value contained by x satisfies p.

Equations
def functor.liftr {F : Type uType u} [functor F] {α : Type u} :
(α → α → Prop)F αF α → Prop

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
def functor.supp {F : Type uType u} [functor F] {α : Type u} :
F αset α

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
• = {y : α | ∀ ⦃p : α → Prop⦄, p y}
theorem functor.of_mem_supp {F : Type uType u} [functor F] {α : Type u} {x : F α} {p : α → Prop} (h : x) (y : α) :
p y

@[instance]

Equations