doc-next-gen

Mathlib.Control.Functor

Module docstring

{"# 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 "}

Functor.map_id theorem
: (id <$> ·) = (id : F α → F α)
Full source 
theorem Functor.map_id : (idid <$> ·) = (id : F α → F α) := funext id_map
Functor Map Preserves Identity: $(id <\$> \cdot) = id$
Informal description
For any functor $F$ and type $\alpha$, the map operation applied to the identity function is equal to the identity function on $F \alpha$, i.e., $(id <\$> \cdot) = id$.
Functor.map_comp_map theorem
(f : α → β) (g : β → γ) : ((g <$> ·) ∘ (f <$> ·) : F α → F γ) = ((g ∘ f) <$> ·)
Full source 
theorem Functor.map_comp_map (f : α → β) (g : β → γ) :
    ((g <$> ·) ∘ (f <$> ·) : F α → F γ) = ((g ∘ f) <$> ·) :=
  funext fun _ => (comp_map _ _ _).symm
Functorial Mapping Preserves Function Composition
Informal description
For any functor $F$ and functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, the composition of the functorial mappings $(g <$> \cdot) \circ (f <$> \cdot)$ is equal to the functorial mapping of the function composition $(g \circ f) <$> \cdot$. In other words, the following diagram commutes: $$ \begin{CD} F \alpha @>{f <$> \cdot}>> F \beta \\ @V{(g \circ f) <$> \cdot}VV @VV{g <$> \cdot}V \\ F \gamma @= F \gamma \end{CD} $$
Functor.ext theorem
{F} : ∀ {F1 : Functor F} {F2 : Functor F} [@LawfulFunctor F F1] [@LawfulFunctor F F2], (∀ (α β) (f : α → β) (x : F α), @Functor.map _ F1 _ _ f x = @Functor.map _ F2 _ _ f x) → F1 = F2
Full source 
theorem Functor.ext {F} :
    ∀ {F1 : Functor F} {F2 : Functor F} [@LawfulFunctor F F1] [@LawfulFunctor F F2],
    (∀ (α β) (f : α → β) (x : F α), @Functor.map _ F1 _ _ f x = @Functor.map _ F2 _ _ f x) →
    F1 = F2
  | ⟨m, mc⟩, ⟨m', mc'⟩, H1, H2, H => by
    cases show @m = @m' by funext α β f x; apply H
    congr
    funext α β
    have E1 := @map_const _ ⟨@m, @mc⟩ H1
    have E2 := @map_const _ ⟨@m, @mc'⟩ H2
    exact E1.trans E2.symm
Functor Instance Extensionality
Informal description
For any functor $F$ with two lawful functor instances $F_1$ and $F_2$, if for all types $\alpha$ and $\beta$, all functions $f : \alpha \to \beta$, and all $x : F \alpha$, the map operations under $F_1$ and $F_2$ coincide (i.e., $F_1.\text{map}\, f\, x = F_2.\text{map}\, f\, x$), then $F_1$ and $F_2$ are equal as functor instances.
id.mk definition
{α : Sort u} : α → id α
Full source 
/-- Introduce `id` as a quasi-functor. (Note that where a lawful `Monad` or
`Applicative` or `Functor` is needed, `Id` is the correct definition). -/
def id.mk {α : Sort u} : α → id α :=
  id
Identity functor constructor
Informal description
The function maps an element $x$ of type $\alpha$ to itself, viewed as an element of the identity functor $\mathrm{id}\,\alpha$.
Functor.Const definition
(α : Type*) (_β : Type*)
Full source 
/-- `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`.) -/
@[nolint unusedArguments]
def Const (α : Type*) (_β : Type*) :=
  α
Constant Functor
Informal description
The constant functor `Const α` maps every type `β` to the fixed type `α`. When `α` has a monoid structure, `Const α` can be given an `Applicative` instance. (For an additive monoid structure on `α`, see `Functor.AddConst`.)
Functor.Const.mk definition
{α β} (x : α) : Const α β
Full source 
/-- `Const.mk` is the canonical map `α → Const α β` (the identity), and
it can be used as a pattern to extract this value. -/
@[match_pattern]
def Const.mk {α β} (x : α) : Const α β :=
  x
Constructor for the constant functor
Informal description
The function maps an element $x$ of type $\alpha$ to itself, viewed as an element of the constant functor $\mathrm{Const}\,\alpha\,\beta$.
Functor.Const.mk' definition
{α} (x : α) : Const α PUnit
Full source 
/-- `Const.mk'` is `Const.mk` but specialized to map `α` to
`Const α PUnit`, where `PUnit` is the terminal object in `Type*`. -/
def Const.mk' {α} (x : α) : Const α PUnit :=
  x
Constant functor constructor with PUnit target
Informal description
The function `Const.mk'` maps an element $x$ of type $\alpha$ to the constant functor `Const α PUnit`, where `PUnit` is the terminal object in the category of types. This is a specialization of `Const.mk` where the target type is fixed to `PUnit`.
Functor.Const.run definition
{α β} (x : Const α β) : α
Full source 
/-- Extract the element of `α` from the `Const` functor. -/
def Const.run {α β} (x : Const α β) : α :=
  x
Extraction from constant functor
Informal description
Given an element `x` of the constant functor `Const α β`, this function extracts the underlying element of type `α`.
Functor.Const.ext theorem
{α β} {x y : Const α β} (h : x.run = y.run) : x = y
Full source 
protected theorem ext {α β} {x y : Const α β} (h : x.run = y.run) : x = y :=
  h
Extensionality of Constant Functor Elements
Informal description
For any types $\alpha$ and $\beta$, and any elements $x, y$ of the constant functor $\operatorname{Const} \alpha \beta$, if the underlying elements $x.\operatorname{run}$ and $y.\operatorname{run}$ are equal, then $x = y$.
Functor.Const.map definition
{γ α β} (_f : α → β) (x : Const γ β) : Const γ α
Full source 
/-- The map operation of the `Const γ` functor. -/
@[nolint unusedArguments]
protected def map {γ α β} (_f : α → β) (x : Const γ β) : Const γ α :=
  x
Mapping operation of the constant functor
Informal description
The map operation of the constant functor `Const γ` takes a function `f : α → β` and a value `x : Const γ β` (which is essentially just a value of type `γ`), and returns `x` unchanged as a `Const γ α`. In other words, the mapping operation ignores the function `f` and simply returns the original value wrapped in the constant functor.
Functor.Const.functor instance
{γ} : Functor (Const γ)
Full source 
instance functor {γ} : Functor (Const γ) where map := @Const.map γ
The Functor Structure on Constant Functors
Informal description
For any type $\gamma$, the constant functor $\mathrm{Const}\,\gamma$ is a functor.
Functor.Const.lawfulFunctor instance
{γ} : LawfulFunctor (Const γ)
Full source 
instance lawfulFunctor {γ} : LawfulFunctor (Const γ) := by constructor <;> intros <;> rfl
Lawfulness of the Constant Functor
Informal description
For any type $\gamma$, the constant functor $\mathrm{Const}\,\gamma$ is a lawful functor. This means that it satisfies the functor laws: the identity function is preserved under mapping, and composition of functions is preserved under mapping.
Functor.Const.instInhabited instance
{α β} [Inhabited α] : Inhabited (Const α β)
Full source 
instance {α β} [Inhabited α] : Inhabited (Const α β) :=
  ⟨(default : α)⟩
Inhabitedness of Constant Functor
Informal description
For any inhabited type $\alpha$ and any type $\beta$, the constant functor $\mathrm{Const}\,\alpha\,\beta$ is also inhabited.
Functor.AddConst definition
(α : Type*)
Full source 
/-- `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`.) -/
def AddConst (α : Type*) :=
  Const α
Additive Constant Functor
Informal description
The functor `AddConst α` is a synonym for the constant functor `Const α`, which maps every type to the fixed type `α`. When `α` has an additive monoid structure, `AddConst α` can be given an `Applicative` instance. (For a multiplicative monoid structure on `α`, see `Functor.Const`.)
Functor.AddConst.mk definition
{α β} (x : α) : AddConst α β
Full source 
/-- `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. -/
@[match_pattern]
def AddConst.mk {α β} (x : α) : AddConst α β :=
  x
Inclusion into additive constant functor
Informal description
The function maps an element $x$ of type $\alpha$ to the constant functor $\mathrm{AddConst}\,\alpha\,\beta$ with value $x$, where $\mathrm{AddConst}\,\alpha\,\beta$ is defined as $\mathrm{Const}\,\alpha\,\beta$.
Functor.AddConst.run definition
{α β} : AddConst α β → α
Full source 
/-- Extract the element of `α` from the constant functor. -/
def AddConst.run {α β} : AddConst α β → α :=
  id
Extraction from additive constant functor
Informal description
The function extracts the element of type $\alpha$ from the constant functor $\mathrm{AddConst}\,\alpha\,\beta$.
Functor.AddConst.functor instance
{γ} : Functor (AddConst γ)
Full source 
instance AddConst.functor {γ} : Functor (AddConst γ) :=
  @Const.functor γ
The Functor Structure on Additive Constant Functors
Informal description
For any type $\gamma$, the additive constant functor $\mathrm{AddConst}\,\gamma$ is a functor.
Functor.AddConst.lawfulFunctor instance
{γ} : LawfulFunctor (AddConst γ)
Full source 
instance AddConst.lawfulFunctor {γ} : LawfulFunctor (AddConst γ) :=
  @Const.lawfulFunctor γ
Lawfulness of the Additive Constant Functor
Informal description
For any type $\gamma$, the additive constant functor $\mathrm{AddConst}\,\gamma$ is a lawful functor. This means it satisfies the functor laws: identity preservation ($\mathrm{map}\, \mathrm{id} = \mathrm{id}$) and composition preservation ($\mathrm{map}\, (f \circ g) = \mathrm{map}\, f \circ \mathrm{map}\, g$).
Functor.instInhabitedAddConst instance
{α β} [Inhabited α] : Inhabited (AddConst α β)
Full source 
instance {α β} [Inhabited α] : Inhabited (AddConst α β) :=
  ⟨(default : α)⟩
Inhabitedness of Additive Constant Functor
Informal description
For any types $\alpha$ and $\beta$, if $\alpha$ is inhabited, then the additive constant functor $\text{AddConst } \alpha \ \beta$ is also inhabited.
Functor.Comp definition
(F : Type u → Type w) (G : Type v → Type u) (α : Type v) : Type w
Full source 
/-- `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. -/
def Comp (F : Type u → Type w) (G : Type v → Type u) (α : Type v) : Type w :=
  F <| G α
Composition of functors
Informal description
The composition of two functors \( F \) and \( G \), denoted \( \text{Comp } F \ G \), is a functor that first applies \( G \) and then applies \( F \) to the result. Specifically, for a type \( \alpha \), \( \text{Comp } F \ G \ \alpha \) is defined as \( F (G \ \alpha) \).
Functor.Comp.mk definition
{F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (G α)) : Comp F G α
Full source 
/-- 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 α)`. -/
@[match_pattern]
def Comp.mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (G α)) : Comp F G α :=
  x
Constructor for composition of functors
Informal description
Given functors \( F \) and \( G \) and a type \( \alpha \), the function constructs an element of the composition functor \( \text{Comp } F \ G \ \alpha \) from an element of \( F (G \ \alpha) \). This can also be used as a pattern to extract an element of \( F (G \ \alpha) \) from a term of \( \text{Comp } F \ G \ \alpha \).
Functor.Comp.run definition
{F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : Comp F G α) : F (G α)
Full source 
/-- Extract a term of `F (G α)` from a term of `Comp F G α`, which is the same type. -/
def Comp.run {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : Comp F G α) : F (G α) :=
  x
Extraction from functor composition
Informal description
Given a term \( x \) of type \( \text{Comp } F \ G \ \alpha \), which represents the composition of functors \( F \) and \( G \) applied to type \( \alpha \), the function extracts the underlying term of type \( F (G \ \alpha) \).
Functor.Comp.ext theorem
{α} {x y : Comp F G α} : x.run = y.run → x = y
Full source 
protected theorem ext {α} {x y : Comp F G α} : x.run = y.run → x = y :=
  id
Extensionality of Functor Composition: $x.\text{run} = y.\text{run} \to x = y$
Informal description
For any type $\alpha$ and any two elements $x, y$ of the composition functor $\text{Comp } F \ G \ \alpha$, if the underlying terms $x.\text{run}$ and $y.\text{run}$ in $F (G \alpha)$ are equal, then $x$ and $y$ are equal.
Functor.Comp.instInhabited instance
{α} [Inhabited (F (G α))] : Inhabited (Comp F G α)
Full source 
instance {α} [Inhabited (F (G α))] : Inhabited (Comp F G α) :=
  ⟨(default : F (G α))⟩
Inhabitedness of Functor Composition
Informal description
For any type $\alpha$, if $F (G \alpha)$ is inhabited, then the composition functor $\text{Comp } F \ G \ \alpha$ is also inhabited.
Functor.Comp.map definition
{α β : Type v} (h : α → β) : Comp F G α → Comp F G β
Full source 
/-- The map operation for the composition `Comp F G` of functors `F` and `G`. -/
protected def map {α β : Type v} (h : α → β) : Comp F G α → Comp F G β
  | Comp.mk x => Comp.mk ((h <$> ·) <$> x)
Map operation for functor composition
Informal description
The map operation for the composition `Comp F G` of functors `F` and `G` takes a function `h : α → β` and applies it to the underlying structure, first mapping `h` over `G α` and then mapping the resulting function over `F (G α)`. Specifically, given an element `Comp.mk x` where `x : F (G α)`, the result is `Comp.mk ((h <$> ·) <$> x)`.
Functor.Comp.functor instance
: Functor (Comp F G)
Full source 
instance functor : Functor (Comp F G) where map := @Comp.map F G _ _
Functor Structure on Composition of Functors
Informal description
The composition of two functors $F$ and $G$ forms a functor, where the map operation is given by composing the map operations of $F$ and $G$.
Functor.Comp.map_mk theorem
{α β} (h : α → β) (x : F (G α)) : h <$> Comp.mk x = Comp.mk ((h <$> ·) <$> x)
Full source 
@[functor_norm]
theorem map_mk {α β} (h : α → β) (x : F (G α)) : h <$> Comp.mk x = Comp.mk ((h <$> ·) <$> x) :=
  rfl
Functor Composition Map Property: $h <$> \text{Comp.mk } x = \text{Comp.mk } ((h <$> \cdot) <$> x)$
Informal description
For any function $h : \alpha \to \beta$ and any element $x : F (G \alpha)$, the map operation applied to the composition functor satisfies: \[ h <$> \text{Comp.mk } x = \text{Comp.mk } ((h <$> \cdot) <$> x) \]
Functor.Comp.run_map theorem
{α β} (h : α → β) (x : Comp F G α) : (h <$> x).run = (h <$> ·) <$> x.run
Full source 
@[simp]
protected theorem run_map {α β} (h : α → β) (x : Comp F G α) :
    (h <$> x).run = (h <$> ·) <$> x.run :=
  rfl
Commutativity of Map and Run Operations in Functor Composition
Informal description
For any function $h : \alpha \to \beta$ and any element $x$ in the composition functor $\text{Comp } F \ G \ \alpha$, applying the map operation $h <$> to $x$ and then extracting the result via $\text{run}$ is equivalent to first extracting $x$ via $\text{run}$ and then applying the map operation $(h <$> \cdot)$ to the result. In symbols: \[ \text{run}(h <$> x) = (h <$> \cdot) <$> \text{run}(x) \]
Functor.Comp.id_map theorem
: ∀ x : Comp F G α, Comp.map id x = x
Full source 
protected theorem id_map : ∀ x : Comp F G α, Comp.map id x = x
  | Comp.mk x => by simp only [Comp.map, id_map, id_map']; rfl
Identity Preservation Law for Functor Composition
Informal description
For any element $x$ of the functor composition $\text{Comp } F \ G \ \alpha$, the map operation with the identity function leaves $x$ unchanged, i.e., $\text{Comp.map } \text{id } x = x$.
Functor.Comp.comp_map theorem
(g' : α → β) (h : β → γ) : ∀ x : Comp F G α, Comp.map (h ∘ g') x = Comp.map h (Comp.map g' x)
Full source 
protected theorem comp_map (g' : α → β) (h : β → γ) :
    ∀ x : Comp F G α, Comp.map (h ∘ g') x = Comp.map h (Comp.map g' x)
  | Comp.mk x => by simp [Comp.map, Comp.mk, Functor.map_comp_map, functor_norm, Function.comp_def]
Composition Law for Functor Map: $\text{map}(h \circ g') = \text{map } h \circ \text{map } g'$
Informal description
For any functor composition $\text{Comp } F \ G$ and functions $g' : \alpha \to \beta$ and $h : \beta \to \gamma$, the map operation satisfies the composition law: \[ \text{Comp.map } (h \circ g') \ x = \text{Comp.map } h \ (\text{Comp.map } g' \ x) \] for all $x : \text{Comp } F \ G \ \alpha$.
Functor.Comp.lawfulFunctor instance
: LawfulFunctor (Comp F G)
Full source 
instance lawfulFunctor : LawfulFunctor (Comp F G) where
  map_const := rfl
  id_map := Comp.id_map
  comp_map := Comp.comp_map
Lawful Functor Composition
Informal description
The composition of two lawful functors $F$ and $G$ is a lawful functor, meaning it satisfies the functor laws (identity preservation and composition preservation) when both $F$ and $G$ individually satisfy these laws.
Functor.Comp.functor_comp_id theorem
{F} [AF : Functor F] [LawfulFunctor F] : @Comp.functor F Id _ _ = AF
Full source 
theorem functor_comp_id {F} [AF : Functor F] [LawfulFunctor F] :
    @Comp.functor F Id _ _ = AF :=
  @Functor.ext F _ AF (Comp.lawfulFunctor (G := Id)) _ fun _ _ _ _ => rfl
Composition with Identity Functor Preserves Functor Instance
Informal description
For any lawful functor $F$, the functor instance obtained by composing $F$ with the identity functor $\text{Id}$ is equal to the original functor instance $AF$ of $F$.
Functor.Comp.functor_id_comp theorem
{F} [AF : Functor F] [LawfulFunctor F] : @Comp.functor Id F _ _ = AF
Full source 
theorem functor_id_comp {F} [AF : Functor F] [LawfulFunctor F] : @Comp.functor Id F _ _ = AF :=
  @Functor.ext F _ AF (Comp.lawfulFunctor (F := Id)) _ fun _ _ _ _ => rfl
Identity Functor Left Composition Law: $\text{Comp.functor}\ \text{Id}\ F = F$
Informal description
For any functor $F$ with a lawful functor instance, the composition of the identity functor with $F$ is equal to $F$ itself as a functor instance.
Functor.Comp.seq definition
{α β : Type v} : Comp F G (α → β) → (Unit → Comp F G α) → Comp F G β
Full source 
/-- The `<*>` operation for the composition of applicative functors. -/
protected def seq {α β : Type v} : Comp F G (α → β) → (Unit → Comp F G α) → Comp F G β
  | Comp.mk f, g => match g () with
    | Comp.mk x => Comp.mk <| (· <*> ·) <$> f <*> x
Sequential application for functor composition
Informal description
The sequential application operation `<*>` for the composition of applicative functors `F` and `G`. Given a composition `Comp F G (α → β)` representing a function and a thunk producing a composition `Comp F G α`, it returns a composition `Comp F G β` by applying the function to the value inside the functors.
Functor.Comp.instPure instance
: Pure (Comp F G)
Full source 
instance : Pure (Comp F G) :=
  ⟨fun x => Comp.mk <| pure <| pure x⟩
Pure Operation for Functor Composition
Informal description
For any functors $F$ and $G$, the composition $\text{Comp } F \ G$ has a canonical pure operation inherited from the pure operations of $F$ and $G$.
Functor.Comp.instSeq instance
: Seq (Comp F G)
Full source 
instance : Seq (Comp F G) :=
  ⟨fun f x => Comp.seq f x⟩
Sequential Application Operation for Functor Composition
Informal description
For any functors $F$ and $G$, the composition $\text{Comp } F \ G$ has a canonical sequential application operation inherited from the sequential application operations of $F$ and $G$.
Functor.Comp.run_pure theorem
{α : Type v} : ∀ x : α, (pure x : Comp F G α).run = pure (pure x)
Full source 
@[simp]
protected theorem run_pure {α : Type v} : ∀ x : α, (pure x : Comp F G α).run = pure (pure x)
  | _ => rfl
Extraction of Pure Value in Functor Composition
Informal description
For any type $\alpha$ and any element $x \in \alpha$, the result of extracting the underlying functor composition of the pure value $x$ in $\text{Comp } F \ G \ \alpha$ is equal to the pure value of the pure value $x$ in $F (G \alpha)$. In other words, $(pure\ x).run = pure (pure\ x)$.
Functor.Comp.run_seq theorem
{α β : Type v} (f : Comp F G (α → β)) (x : Comp F G α) : (f <*> x).run = (· <*> ·) <$> f.run <*> x.run
Full source 
@[simp]
protected theorem run_seq {α β : Type v} (f : Comp F G (α → β)) (x : Comp F G α) :
    (f <*> x).run = (· <*> ·) <$> f.run(· <*> ·) <$> f.run <*> x.run :=
  rfl
Sequential Application Extraction in Functor Composition
Informal description
For any types $\alpha$ and $\beta$, given a function $f$ in the composition functor $\text{Comp } F \ G (\alpha \to \beta)$ and a value $x$ in $\text{Comp } F \ G \alpha$, the extraction of the sequential application $f <*> x$ is equal to the sequential application of the lifted sequential application function $(· <*> ·)$ over the extracted $f$ and $x$. In symbols: $$(f <*> x).\text{run} = (· <*> ·) <\$> f.\text{run} <*> x.\text{run}$$
Functor.Comp.instApplicativeComp instance
: Applicative (Comp F G)
Full source 
instance instApplicativeComp : Applicative (Comp F G) :=
  { map := @Comp.map F G _ _, seq := @Comp.seq F G _ _ }
Applicative Functor Composition
Informal description
For any two applicative functors $F$ and $G$, their composition $\text{Comp } F \ G$ is also an applicative functor.
Functor.Liftp definition
{α : Type u} (p : α → Prop) (x : F α) : Prop
Full source 
/-- 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`. -/
def Liftp {α : Type u} (p : α → Prop) (x : F α) : Prop :=
  ∃ u : F (Subtype p), Subtype.val <$> u = x
Lifting of a predicate to a functor
Informal description
Given a predicate $p : \alpha \to \text{Prop}$ and a term $x : F \alpha$, the predicate $\text{Liftp } p \, x$ holds if there exists a term $u : F \{a : \alpha \mid p a\}$ such that mapping the subtype inclusion function over $u$ yields $x$. In other words, $\text{Liftp } p \, x$ is true if $x$ can be "lifted" from a term whose elements all satisfy $p$.
Functor.Liftr definition
{α : Type u} (r : α → α → Prop) (x y : F α) : Prop
Full source 
/-- 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. -/
def Liftr {α : Type u} (r : α → α → Prop) (x y : F α) : Prop :=
  ∃ u : F { p : α × α // r p.fst p.snd },
    (fun t : { p : α × α // r p.fst p.snd } => t.val.fst) <$> u = x ∧
      (fun t : { p : α × α // r p.fst p.snd } => t.val.snd) <$> u = y
Lifting of a relation to a functorial context
Informal description
Given a relation $r$ on a type $\alpha$ and two elements $x, y$ of type $F \alpha$, the predicate $\text{Liftr}\, r\, x\, y$ holds if and only if there exists an element $u$ of type $F \{(p : \alpha \times \alpha) \mid r\, p.1\, p.2\}$ such that the first projection of $u$ equals $x$ and the second projection of $u$ equals $y$ under the functorial mapping. In other words, $x$ and $y$ have the same "shape" and their corresponding elements are related by $r$.
Functor.supp definition
{α : Type u} (x : F α) : Set α
Full source 
/-- 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. -/
def supp {α : Type u} (x : F α) : Set α :=
  { y : α | ∀ ⦃p⦄, Liftp p x → p y }
Support of a functorial element
Informal description
For a functor `F` and an element `x : F α`, the support `supp x` is the set of all elements `y : α` such that for every predicate `p : α → Prop`, if `Liftp p x` holds (meaning `x` can be lifted from a term whose elements all satisfy `p`), then `p y` must hold. In other words, `supp x` collects all elements of `α` that are "contained" in `x` in the sense that they must satisfy any predicate that `x` can be lifted from.
Functor.of_mem_supp theorem
{α : Type u} {x : F α} {p : α → Prop} (h : Liftp p x) : ∀ y ∈ supp x, p y
Full source 
theorem of_mem_supp {α : Type u} {x : F α} {p : α → Prop} (h : Liftp p x) : ∀ y ∈ supp x, p y :=
  fun _ hy => hy h
Support Elements Satisfy Lifted Predicate
Informal description
For any functor `F`, element `x : F α`, and predicate `p : α → Prop`, if `Liftp p x` holds (meaning `x` can be lifted from a term whose elements all satisfy `p`), then for every element `y` in the support of `x`, the predicate `p y` holds.
Functor.mapConstRev abbrev
{f : Type u → Type v} [Functor f] {α β : Type u} : f β → α → f α
Full source 
/-- 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`. -/
abbrev mapConstRev {f : Type u → Type v} [Functor f] {α β : Type u} :
    f β → α → f α :=
  fun a b => Functor.mapConst b a
Mapping a Constant Function Through a Functor
Informal description
Given a functor $f$, an element $fb : f \beta$, and an element $a : \alpha$, the function `mapConstRev` applies the functor's mapping operation to the constant function $\lambda \_. a : \beta \to \alpha$ and evaluates it at $fb$. This is equivalent to applying the operation `const a <$> fb` in Haskell notation.
Functor.term_$>_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- 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`. -/
infix:100 " $> " => Functor.mapConstRev
Functor map constant reverse operator (`$>`)
Informal description
The infix operator `$>` is defined as `Functor.mapConstRev`, which for a functor `f`, an element `fb : f β`, and a value `a : α`, applies the functor's map operation to the constant function sending every element of `β` to `a`, and then evaluates this at `fb`. This is equivalent to `const a <$> fb`.