# Documentation

Mathlib.Control.Functor

# Functors #

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

## 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

theorem Functor.map_id {F : Type u → Type v} {α : Type u} [inst : ] [inst : ] :
(fun x x_1 => x <$> x_1) id = id theorem Functor.map_comp_map {F : Type u → Type v} {α : Type u} {β : Type u} {γ : Type u} [inst : ] [inst : ] (f : αβ) (g : βγ) : (fun x x_1 => x <$> x_1) g (fun x x_1 => x <$> x_1) f = (fun x x_1 => x <$> x_1) (g f)
theorem Functor.ext {F : Type u_1 → Type u_2} {F1 : } {F2 : } [inst : ] [inst : ] :
(∀ (α β : Type u_1) (f : αβ) (x : F α), f <$> x = f <$> x) → F1 = F2
def id.mk {α : Sort u} :
αid α

Introduce id as a quasi-functor. (Note that where a lawful Monad or Applicative or Functor is needed, Id is the correct definition).

Equations
• id.mk = id
def Functor.Const (α : Type u_1) (_β : Type u_2) :
Type 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.AddConst.)

Equations
• = α
@[match_pattern]
def Functor.Const.mk {α : Type u_1} {β : Type u_2} (x : α) :

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

Equations
def Functor.Const.mk' {α : Type u_1} (x : α) :

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} (x : ) :
α

Extract the element of α from the Const functor.

Equations
theorem Functor.Const.ext {α : Type u_1} {β : Type u_2} {x : } {y : } (h : ) :
x = y
def Functor.Const.map {γ : Type u_1} {α : Type u_2} {β : Type u_3} (_f : αβ) (x : ) :

The map operation of the Const γ functor.

Equations
instance Functor.Const.functor {γ : Type u_1} :
Equations
• Functor.Const.functor = { map := , mapConst := fun {α β} => Functor.Const.map }
instance Functor.Const.lawfulFunctor {γ : Type u_1} :
Equations
instance Functor.Const.instInhabitedConst {α : Type u_1} {β : Type u_2} [inst : ] :
Equations
• Functor.Const.instInhabitedConst = { default := default }
def Functor.AddConst (α : Type u_1) (_β : Type u_2) :
Type u_1

AddConst α is a synonym for constant functor Const α, mapping every type to α. When α has a additive monoid structure, AddConst α has an Applicative instance. (If α has a multiplicative monoid structure, see Functor.Const.)

Equations
@[match_pattern]
def Functor.AddConst.mk {α : Type u_1} {β : Type u_2} (x : α) :

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

Equations
def Functor.AddConst.run {α : Type u_1} {β : Type u_2} :
α

Extract the element of α from the constant functor.

Equations
instance Functor.AddConst.functor {γ : Type u_1} :
Equations
instance Functor.AddConst.lawfulFunctor {γ : Type u_1} :
Equations
instance Functor.instInhabitedAddConst {α : Type u_1} {β : Type u_2} [inst : ] :
Equations
• Functor.instInhabitedAddConst = { default := default }
def Functor.Comp (F : Type u → Type w) (G : Type v → Type u) (α : Type v) :

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
@[match_pattern]
def Functor.Comp.mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (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 u → Type w} {G : Type v → Type u} {α : Type v} (x : Functor.Comp F 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 u → Type w} {G : Type v → Type u} {α : Type v} {x : Functor.Comp F G α} {y : Functor.Comp F G α} :
x = y
instance Functor.Comp.instInhabitedComp {F : Type u → Type w} {G : Type v → Type u} {α : Type v} [inst : Inhabited (F (G α))] :
Equations
• Functor.Comp.instInhabitedComp = { default := default }
def Functor.Comp.map {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] {α : Type v} {β : Type v} (h : αβ) :
Functor.Comp F G αFunctor.Comp F G β

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

Equations
instance Functor.Comp.functor {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] :
Equations
• Functor.Comp.functor = { map := @Functor.Comp.map F G inst inst, mapConst := fun {α β} => Functor.Comp.map }
theorem Functor.Comp.map_mk {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] {α : Type v} {β : Type v} (h : αβ) (x : F (G α)) :
= Functor.Comp.mk ((fun x x_1 => x <$> x_1) h <$> x)
@[simp]
theorem Functor.Comp.run_map {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] {α : Type v} {β : Type v} (h : αβ) (x : Functor.Comp F G α) :
Functor.Comp.run (h <$> x) = (fun x x_1 => x <$> x_1) h <$> theorem Functor.Comp.id_map {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type v} (x : Functor.Comp F G α) : = x theorem Functor.Comp.comp_map {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type v} {β : Type v} {γ : Type v} (g' : αβ) (h : βγ) (x : Functor.Comp F G α) : instance Functor.Comp.lawfulFunctor {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] : Equations theorem Functor.Comp.functor_comp_id {F : Type u_1 → Type u_2} [AF : ] [inst : ] : Functor.Comp.functor = AF theorem Functor.Comp.functor_id_comp {F : Type u_1 → Type u_2} [AF : ] [inst : ] : Functor.Comp.functor = AF def Functor.Comp.seq {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] {α : Type v} {β : Type v} : Functor.Comp F G (αβ)(UnitFunctor.Comp F G α) → Functor.Comp F G β The <*> operation for the composition of applicative functors. Equations instance Functor.Comp.instPureComp {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] : Pure () Equations instance Functor.Comp.instSeqComp {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] : Seq () Equations • Functor.Comp.instSeqComp = { seq := fun {α β} f x => } @[simp] theorem Functor.Comp.run_pure {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] {α : Type v} (x : α) : = pure (pure x) @[simp] theorem Functor.Comp.run_seq {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] {α : Type v} {β : Type v} (f : Functor.Comp F G (αβ)) (x : Functor.Comp F G α) : Functor.Comp.run (Seq.seq f fun x => x) = Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <$> ) fun x =>
instance Functor.Comp.instApplicativeComp {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] :
Equations
• Functor.Comp.instApplicativeComp = let src := Functor.Comp.instPureComp; Applicative.mk
def Functor.Liftp {F : Type u → Type u} [inst : ] {α : Type u} (p : αProp) (x : F α) :

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
• = u, Subtype.val <$> u = x def Functor.Liftr {F : Type u → Type u} [inst : ] {α : Type u} (r : ααProp) (x : F α) (y : F α) : 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 • = u, (fun t => t.val.fst) <$> u = x (fun t => t.val.snd) <$> u = y def Functor.supp {F : Type u → Type u} [inst : ] {α : Type u} (x : 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 u → Type u} [inst : ] {α : Type u} {x : F α} {p : αProp} (h : ) (y : α) : p y def Functor.mapConstRev {f : Type u → Type v} [inst : ] {α : Type u} {β : Type u} : f βαf α 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

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