mathlib docs: control.functor

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

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

functor.map g ∘ functor.map f = functor.map (g ∘ f)

source

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

F1 = F2

source

def id.mk {α : Sort u} (a : α) :

id α

Equations

id.mk = id

source

@[nolint]

def functor.const (α : Type u_1) (β : Type u_2) :

Type u_1

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

Equations

functor.const α β = α

source

def functor.const.mk {α : Type u_1} {β : Type u_2} (x : α) :

functor.const α β

Equations

functor.const.mk x = x

source

def functor.const.mk' {α : Type u_1} (x : α) :

functor.const α punit

Equations

functor.const.mk' x = x

source

def functor.const.run {α : Type u_1} {β : Type u_2} (x : functor.const α β) :

α

Equations

x.run = x

source

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

x = y

source

@[nolint]

def functor.const.map {γ : Type u_1} {α : Type u_2} {β : Type u_3} (f : α → β) (x : functor.const γ β) :

functor.const γ α

The map operation of the const γ functor.

Equations

functor.const.map f x = x

source

@[instance]

def functor.const.functor {γ : Type u_1} :

functor (functor.const γ)

Equations

functor.const.functor = {map := functor.const.map γ, map_const := λ (α β : Type u_2), functor.const.map ∘ function.const β}

source

@[instance]

def functor.const.is_lawful_functor {γ : Type u_1} :

is_lawful_functor (functor.const γ)

source

def functor.add_const (α : Type u_1) (β : Type u_2) :

Type u_1

Equations

functor.add_const α = functor.const α

source

def functor.add_const.mk {α : Type u_1} {β : Type u_2} (x : α) :

functor.add_const α β

Equations

functor.add_const.mk x = x

source

def functor.add_const.run {α : Type u_1} {β : Type u_2} (a : functor.add_const α β) :

α

Equations

functor.add_const.run = id

source

@[instance]

def functor.add_const.functor {γ : Type u_1} :

functor (functor.add_const γ)

Equations

functor.add_const.functor = functor.const.functor

source

@[instance]

def functor.add_const.is_lawful_functor {γ : Type u_1} :

is_lawful_functor (functor.add_const γ)

source

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 α)

source

def functor.comp.mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (G α)) :

functor.comp F G α

Equations

functor.comp.mk x = x

source

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

F (G α)

Equations

x.run = x

source

theorem functor.comp.ext {F : Type u → Type w} {G : Type v → Type u} {α : Type v} {x y : functor.comp F G α} (a : x.run = y.run) :

x = y

source

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

functor.comp F G β

Equations

functor.comp.map h (functor.comp.mk x) = functor.comp.mk (functor.map h <$> x)

source

@[instance]

def functor.comp.functor {F : Type u → Type w} {G : Type v → Type u} [functor F] [functor G] :

functor (functor.comp F G)

Equations

functor.comp.functor = {map := functor.comp.map _inst_2, map_const := λ (α β : Type v), functor.comp.map ∘ function.const β}

source

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 <$> functor.comp.mk x = functor.comp.mk (functor.map h <$> x)

source

@[simp]

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

functor.comp.run (h <$> x) = functor.map h <$> x.run

source

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

functor.comp.map id x = x

source

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

functor.comp.map (h ∘ g') x = functor.comp.map h (functor.comp.map g' x)

source

@[instance]

def functor.comp.is_lawful_functor {F : Type u → Type w} {G : Type v → Type u} [functor F] [functor G] [is_lawful_functor F] [is_lawful_functor G] :

is_lawful_functor (functor.comp F G)

source

theorem functor.comp.functor_comp_id {F : Type u_1 → Type u_2} [AF : functor F] [is_lawful_functor F] :

functor.comp.functor = AF

source

theorem functor.comp.functor_id_comp {F : Type u_1 → Type u_2} [AF : functor F] [is_lawful_functor F] :

functor.comp.functor = AF

source

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

functor.comp F G β

Equations

(functor.comp.mk f).seq (functor.comp.mk x) = functor.comp.mk (has_seq.seq <$> f <*> x)

source

@[instance]

def functor.comp.has_pure {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] :

has_pure (functor.comp F G)

Equations

functor.comp.has_pure = {pure := λ (_x : Type v) (x : _x), functor.comp.mk (pure (pure x))}

source

@[instance]

def functor.comp.has_seq {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] :

has_seq (functor.comp F G)

Equations

functor.comp.has_seq = {seq := λ (_x _x_1 : Type v) (f : functor.comp F G (_x → _x_1)) (x : functor.comp F G _x), f.seq x}

source

@[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)

source

@[simp]

theorem functor.comp.run_seq {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] {α β : Type v} (f : functor.comp F G (α → β)) (x : functor.comp F G α) :

(f <*> x).run = has_seq.seq <$> f.run <*> x.run

source

@[instance]

def functor.comp.applicative {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] :

applicative (functor.comp F G)

Equations

functor.comp.applicative = applicative.mk

source

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

source

def functor.liftr {F : Type u → Type u} [functor F] {α : Type u} (r : α → α → Prop) (x y : F α) :

Prop

liftr r x y relates x and y iff x and y have the same shape and that we can pair values a from x and b from y so that r a b holds

Equations

functor.liftr r x y = ∃ (u : F {p // r p.fst p.snd}), (λ (t : {p // r p.fst p.snd}), t.val.fst) <$> u = x ∧ (λ (t : {p // r p.fst p.snd}), t.val.snd) <$> u = y

source

def functor.supp {F : Type u → Type u} [functor F] {α : Type u} (x : F α) :

set α

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}

source

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

p y

source

@[instance]

def ulift.functor :

functor ulift

Equations

ulift.functor = {map := λ (α β : Type u_1) (f : α → β), ulift.up ∘ f ∘ ulift.down, map_const := λ (α β : Type u_1), (λ (f : β → α), ulift.up ∘ f ∘ ulift.down) ∘ function.const β}