Documentation

Mathlib.Control.Functor

Functors #

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

Main definitions #

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
    Instances For
      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
        Instances For
          @[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
            Instances For
              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
                Instances For
                  def Functor.Const.run {α : Type u_1} {β : Type u_2} (x : Const α β) :
                  α

                  Extract the element of α from the Const functor.

                  Equations
                    Instances For
                      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
                        Instances For
                          instance Functor.Const.functor {γ : Type u_1} :
                          Equations
                            instance Functor.Const.instInhabited {α : Type u_1} {β : Type u_2} [Inhabited α] :
                            Equations
                              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
                                Instances For
                                  @[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
                                    Instances For
                                      def Functor.AddConst.run {α : Type u_1} {β : Type u_2} :
                                      AddConst α βα

                                      Extract the element of α from the constant functor.

                                      Equations
                                        Instances For
                                          instance Functor.AddConst.functor {γ : Type u_1} :
                                          Equations
                                            instance Functor.instInhabitedAddConst {α : Type u_1} {β : Type u_2} [Inhabited α] :
                                            Equations
                                              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
                                                Instances For
                                                  @[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
                                                    Instances For
                                                      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
                                                        Instances For
                                                          theorem Functor.Comp.ext {F : Type u → Type w} {G : Type v → Type u} {α : Type v} {x y : Comp F G α} :
                                                          x.run = y.runx = 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
                                                            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
                                                              Instances For
                                                                instance Functor.Comp.functor {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] :
                                                                Equations
                                                                  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 α) :
                                                                  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] :
                                                                  theorem Functor.Comp.functor_comp_id {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F] :
                                                                  theorem Functor.Comp.functor_id_comp {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F] :
                                                                  def Functor.Comp.seq {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] {α β : Type v} :
                                                                  Comp F G (αβ)(UnitComp F G α)Comp F G β

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

                                                                  Equations
                                                                    Instances For
                                                                      instance Functor.Comp.instPure {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] :
                                                                      Pure (Comp F G)
                                                                      Equations
                                                                        instance Functor.Comp.instSeq {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] :
                                                                        Seq (Comp F G)
                                                                        Equations
                                                                          @[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] :
                                                                          Equations
                                                                            def Functor.Liftp {F : Type u → Type u} [Functor F] {α : 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
                                                                              Instances For
                                                                                def Functor.Liftr {F : Type u → Type u} [Functor F] {α : Type u} (r : ααProp) (x 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
                                                                                  Instances For
                                                                                    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
                                                                                      Instances For
                                                                                        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 xp 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
                                                                                          Instances For

                                                                                            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
                                                                                              Instances For