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} [Functor F] [LawfulFunctor F] : (fun (x : F α) => id <$> x) = id

theorem Functor.map_comp_map {F : Type u → Type v} {α β γ : Type u} [Functor F] [LawfulFunctor F] (f : α → β) (g : β → γ) : ((fun (x : F β) => g <$> x) ∘ fun (x : F α) => f <$> x) = fun (x : F α) => (g ∘ f) <$> x

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

@[deprecated "Use `pure : α → Id α` instead." (since := "2025-05-21")]

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

• Functor.Const α _β = α

@[match_pattern]

def Functor.Const.mk {α : Type u_1} {β : Type u_2} (x : α) : Const α β

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

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

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

Equations

• Functor.Const.mk' x = x

def Functor.Const.run {α : Type u_1} {β : Type u_2} (x : Const α β) : α

Extract the element of α from the Const functor.

Equations

• x.run = x

theorem Functor.Const.ext {α : Type u_1} {β : Type u_2} {x y : Const α β} (h : x.run = y.run) : x = y

def Functor.Const.map {γ : Type u_1} {α : Type u_2} {β : Type u_3} (_f : α → β) (x : Const γ β) : Const γ α

The map operation of the Const γ functor.

Equations

• Functor.Const.map _f x = x

instance Functor.Const.functor {γ : Type u_1} : Functor (Const γ)

Equations

• Functor.Const.functor = { map := @Functor.Const.map γ }

instance Functor.Const.lawfulFunctor {γ : Type u_1} : LawfulFunctor (Const γ)

instance Functor.Const.instInhabited {α : Type u_1} {β : Type u_2} [Inhabited α] : Inhabited (Const α β)

Equations

• Functor.Const.instInhabited = { 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 an additive monoid structure, AddConst α has an Applicative instance. (If α has a multiplicative monoid structure, see Functor.Const.)

Equations

• Functor.AddConst α = Functor.Const α

@[match_pattern]

def Functor.AddConst.mk {α : Type u_1} {β : Type u_2} (x : α) : AddConst α β

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

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

Extract the element of α from the constant functor.

Equations

• Functor.AddConst.run = id

instance Functor.AddConst.functor {γ : Type u_1} : Functor (AddConst γ)

Equations

• Functor.AddConst.functor = Functor.Const.functor

instance Functor.AddConst.lawfulFunctor {γ : Type u_1} : LawfulFunctor (AddConst γ)

instance Functor.instInhabitedAddConst {α : Type u_1} {β : Type u_2} [Inhabited α] : Inhabited (AddConst α β)

Equations

• Functor.instInhabitedAddConst = { default := default }

def Functor.Comp (F : Type u → Type w) (G : Type v → Type u) (α : Type v) : Type 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

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

@[match_pattern]

def Functor.Comp.mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (G α)) : Comp 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

• Functor.Comp.mk x = x

def Functor.Comp.run {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : Comp F G α) : F (G α)

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

Equations

• x.run = x

theorem Functor.Comp.ext {F : Type u → Type w} {G : Type v → Type u} {α : Type v} {x y : Comp F G α} : x.run = y.run → x = y

instance Functor.Comp.instInhabited {F : Type u → Type w} {G : Type v → Type u} {α : Type v} [Inhabited (F (G α))] : Inhabited (Comp F G α)

Equations

• Functor.Comp.instInhabited = { default := default }

def Functor.Comp.map {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) : Comp F G α → Comp F G β

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

Equations

• Functor.Comp.map h x✝ = Functor.Comp.mk ((fun (x : G α) => h <$> x) <$> x✝)

instance Functor.Comp.functor {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] : Functor (Comp F G)

Equations

• Functor.Comp.functor = { map := @Functor.Comp.map F G inst✝¹ inst✝ }

theorem Functor.Comp.map_mk {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x : F (G α)) : h <$> mk x = mk ((fun (x : G α) => h <$> x) <$> x)

@[simp]

theorem Functor.Comp.run_map {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x : Comp F G α) : (h <$> x).run = (fun (x : G α) => h <$> x) <$> x.run

theorem Functor.Comp.id_map {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] {α : Type v} (x : Comp F G α) : Comp.map id x = x

theorem Functor.Comp.comp_map {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] {α β γ : Type v} (g' : α → β) (h : β → γ) (x : Comp F G α) : Comp.map (h ∘ g') x = Comp.map h (Comp.map g' x)

instance Functor.Comp.lawfulFunctor {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] : LawfulFunctor (Comp F G)

theorem Functor.Comp.functor_comp_id {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F] : functor = AF

theorem Functor.Comp.functor_id_comp {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F] : functor = AF

def Functor.Comp.seq {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] {α β : Type v} : Comp F G (α → β) → (Unit → Comp F G α) → Comp F G β

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

Equations

• x✝¹.seq x✝ = match x✝ () with | x => Functor.Comp.mk ((fun (x1 : G (α → β)) (x2 : G α) => x1 <*> x2) <$> x✝¹ <*> x)

instance Functor.Comp.instPure {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] : Pure (Comp F G)

Equations

• Functor.Comp.instPure = { pure := fun {α : Type ?u.26} (x : α) => Functor.Comp.mk (pure (pure x)) }

instance Functor.Comp.instSeq {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] : Seq (Comp F G)

Equations

• Functor.Comp.instSeq = { seq := fun {α β : Type ?u.30} (f : Functor.Comp F G (α → β)) (x : Unit → Functor.Comp F G α) => f.seq x }

@[simp]

theorem Functor.Comp.run_pure {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] {α : Type v} (x : α) : (pure x).run = pure (pure x)

@[simp]

theorem Functor.Comp.run_seq {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] {α β : Type v} (f : Comp F G (α → β)) (x : Comp F G α) : (f <*> x).run = (fun (x1 : G (α → β)) (x2 : G α) => x1 <*> x2) <$> f.run <*> x.run

instance Functor.Comp.instApplicativeComp {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] : Applicative (Comp F G)

Equations

• Functor.Comp.instApplicativeComp = { map := @Functor.Comp.map F G inst✝¹.toFunctor inst✝.toFunctor, toPure := Functor.Comp.instPure, seq := @Functor.Comp.seq F G inst✝¹ inst✝ }

def Functor.Liftp {F : Type u → Type u} [Functor F] {α : Type u} (p : α → Prop) (x : 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

• Functor.Liftp p x = ∃ (u : F (Subtype p)), Subtype.val <$> u = x

def Functor.Liftr {F : Type u → Type u} [Functor F] {α : Type u} (r : α → α → Prop) (x y : 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

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

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

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

theorem Functor.of_mem_supp {F : Type u → Type u} [Functor F] {α : Type u} {x : F α} {p : α → Prop} (h : Liftp p x) (y : α) : y ∈ supp x → p y

@[reducible, inline]

abbrev Functor.mapConstRev {f : Type u → Type v} [Functor f] {α β : 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

• a $> b = Functor.mapConst b a

def Functor.«term_$>_» : Lean.TrailingParserDescr

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

• Functor.«term_$>_» = Lean.ParserDescr.trailingNode `Functor.«term_$>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " $> ") (Lean.ParserDescr.cat `term 101))