LawfulTraversable.naturality
theorem LawfulTraversable.naturality :
∀ {t : Type u → Type u} [inst : Traversable t] [self : LawfulTraversable t] {F G : Type u → Type u}
[inst_1 : Applicative F] [inst_2 : Applicative G] [inst_3 : LawfulApplicative F] [inst_4 : LawfulApplicative G]
(η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α),
(fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x
The theorem `LawfulTraversable.naturality` states the naturality axiom for lawful traversable functors. In particular, for any traversable functor `t`, any two applicative functors `F` and `G`, and an applicative transformation `η` from `F` to `G`, for any function `f : α → F β` and any `x : t α`, the application of `η` to the result of traversing `x` with `f` is the same as traversing `x` with `f` first and then applying `η`. This theorem is a key property ensuring the correct interaction between traversable and applicative functors.
More concisely: For any traversable functor `t`, applicative functors `F` and `G`, and an applicative transformation `η` from `F` to `G`, if `f : α → F β` and `x : t α`, then `η (traverse t x f) = traverse t x (η ∘ f)`.
|
ApplicativeTransformation.preserves_map
theorem ApplicativeTransformation.preserves_map :
∀ {F : Type u → Type v} [inst : Applicative F] [inst_1 : LawfulApplicative F] {G : Type u → Type w}
[inst_2 : Applicative G] [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u}
(x : α → β) (y : F α), (fun {α} => η.app α) (x <$> y) = x <$> (fun {α} => η.app α) y
The theorem `ApplicativeTransformation.preserves_map` states that for all types `F` and `G` that are applicative and lawful applicative, and for an applicative transformation `η` from `F` to `G`, and for all types `α` and `β`, and for a function `x` from `α` to `β` and a value `y` of type `F α`, applying the transformation `η` to the result of mapping `x` over `y` is the same as mapping `x` over the result of applying the transformation `η` to `y`. In other words, the transformation `η` preserves the `map` operation.
More concisely: For all applicative and lawful functors F and G, and applicative transformation η from F to G, the map operation is preserved: for all types α and β and functions x: α → β and values y: F α, η (map x y) = map x (η y).
|
LawfulTraversable.id_traverse
theorem LawfulTraversable.id_traverse :
∀ {t : Type u → Type u} [inst : Traversable t] [self : LawfulTraversable t] {α : Type u} (x : t α),
traverse pure x = x
This theorem, `LawfulTraversable.id_traverse`, states that for any type `t` that is an instance of the `Traversable` and `LawfulTraversable` typeclasses, and for any type `α` and value `x` of type `t α`, applying the `traverse` function with `pure` of the identity monad to `x` yields `x` itself. In other words, traversing a structure with the identity monad leaves the structure unchanged.
More concisely: For any `Traversable t` and `α`, the identity monad's `traverse` function applied to an element `x` of type `t α` returns `x` itself.
|
LawfulTraversable.comp_traverse
theorem LawfulTraversable.comp_traverse :
∀ {t : Type u → Type u} [inst : Traversable t] [self : LawfulTraversable t] {F G : Type u → Type u}
[inst_1 : Applicative F] [inst_2 : Applicative G] [inst_3 : LawfulApplicative F] [inst_4 : LawfulApplicative G]
{α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α),
traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
The theorem `LawfulTraversable.comp_traverse` establishes the compatibility of the `traverse` function with the composition of applicative functors. Specifically, for all types `t`, `F`, `G`, `α`, `β`, and `γ`, given a `Traversable` instance for `t`, `LawfulTraversable` instance for `t`, `Applicative` instances for `F` and `G`, `LawfulApplicative` instances for `F` and `G`, a function `f` from `β` to `F γ`, a function `g` from `α` to `G β`, and a value `x` of type `t α`, the theorem shows that traversing with a composite functor created by first applying `g`, then `Functor.map` of `f`, and finally `Functor.Comp.mk`, is equivalent to first performing a traverse with `g`, then a traverse with `f`, and finally applying `Functor.Comp.mk` to the result. This theorem essentially exhibits how `traverse` respects the structure of composition in the context of applicative functors.
More concisely: For any types `t`, `F`, `G`, `α`, `β`, `γ` with `Traversable t`, `LawfulTraversable t`, `Applicative F`, `LawfulApplicative F`, `Applicative G`, `LawfulApplicative G`, functions `f : β -> F γ` and `g : α -> G β`, and value `x : t α`, the following equality holds: `traverse (Functor.Comp.mk (G.map g) f) x = traverse g (traverse f x)`.
|
ApplicativeTransformation.preserves_pure
theorem ApplicativeTransformation.preserves_pure :
∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
(η : ApplicativeTransformation F G) {α : Type u} (x : α), (fun {α} => η.app α) (pure x) = pure x
This theorem states that for any two applicative functors `F` and `G`, and any applicative transformation `η` from `F` to `G`, the transformation `η` preserves the "pure" operation. Given any type `α` and any value `x` of type `α`, the result of applying the transformation `η` to `pure x` (where `pure` is a function that embeds a value into a functor) is the same as `pure x`. In other words, the transformation doesn't change the result of the "pure" operation.
More concisely: Given any applicative functors `F` and `G` and an applicative transformation `η` from `F` to `G`, for all types `α` and values `x` of type `α`, `η (pure x) = pure x`.
|
LawfulTraversable.traverse_eq_map_id
theorem LawfulTraversable.traverse_eq_map_id :
∀ {t : Type u → Type u} [inst : Traversable t] [self : LawfulTraversable t] {α β : Type u} (f : α → β) (x : t α),
traverse (pure ∘ f) x = id.mk (f <$> x)
This theorem, `LawfulTraversable.traverse_eq_map_id`, states that for any type constructor `t` that has a `Traversable` and `LawfulTraversable` instance, and for any types `α` and `β`, and a function `f` from `α` to `β`, and a value `x` of type `t α`, the operation of traversing `x` with the function `pure ∘ f` is equivalent to mapping `f` over `x` and then applying `id.mk` to the result. Here, `pure` is a function that wraps a value of type `β` into the `Id` applicative functor, `fmap` is the function mapping operation, and `id.mk` is a function that wraps a value into the `Id` type.
More concisely: For any `Traversable t` and `LawfulTraversable t`, any types `α` and `β`, and any function `f: α → β`, the traversal of `t x` with `pure ∘ f` is equal to the application of `f` to each element of `x` and wrapping the result in `Id`.
|
ApplicativeTransformation.ext
theorem ApplicativeTransformation.ext :
∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
⦃η η' : ApplicativeTransformation F G⦄,
(∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x) → η = η'
This theorem called `ApplicativeTransformation.ext` states that for any two Applicative Transformations `η` and `η'` from an applicative functor `F` to another applicative functor `G`, if for all types `α` and for all elements `x` of type `F α`, the application of `η` to `x` is equal to the application of `η'` to `x`, then `η` must be equal to `η'`. In simpler terms, if two Applicative Transformations behave the same way for all inputs, they must be the same transformation.
More concisely: If two applicative functor transformations η and η' from F to G satisfy η(x) = η'(x) for all x : F α, then η = η'.
|
ApplicativeTransformation.preserves_seq
theorem ApplicativeTransformation.preserves_seq :
∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
(η : ApplicativeTransformation F G) {α β : Type u} (x : F (α → β)) (y : F α),
(fun {α} => η.app α) (Seq.seq x fun x => y) = Seq.seq ((fun {α} => η.app α) x) fun x => (fun {α} => η.app α) y
The theorem `ApplicativeTransformation.preserves_seq` asserts that for any two types `F` and `G` that are instances of the Applicative typeclass, and for any Applicative Transformation `η` from `F` to `G`, and for any two values `x` of type `F (α → β)` and `y` of type `F α`, applying `η` to the result of performing the `Seq.seq` operation on `x` and `y` is the same as performing `Seq.seq` on the result of applying `η` to `x` and a function that applies `η` to `y`. In other words, it states that the `Seq.seq` operation is preserved under an Applicative Transformation, which is a fundamental property that ensures the behavior of computations remains consistent when transformed from one context (Applicative) to another.
More concisely: Given Applicative functors F and G, an Applicative transformation η from F to G, and values x : F (α → β) and y : F α, Seq.seq (η <$> x) (η <$ y) is equivalent to η (Seq.seq x y).
|
ApplicativeTransformation.preserves_pure'
theorem ApplicativeTransformation.preserves_pure' :
∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
(self : ApplicativeTransformation F G) {α : Type u} (x : α), self.app α (pure x) = pure x
This theorem states that an `ApplicativeTransformation` preserves the `pure` function. In more detail, for any applicative functors `F` and `G`, if there is an `ApplicativeTransformation` from `F` to `G`, then applying this transformation to `pure x` in the `F` context results in `pure x` in the `G` context, for any type `α` and value `x` of type `α`. This essentially means that an `ApplicativeTransformation` doesn't change the value encapsulated by the `pure` function, it only changes the context from `F` to `G`.
More concisely: For any applicative functors F and G, and any type α and value x, if there exists an ApplicativeTransformation from F to G, then applying the transformation to pure x in the F context equals pure x in the G context.
|
ApplicativeTransformation.preserves_seq'
theorem ApplicativeTransformation.preserves_seq' :
∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
(self : ApplicativeTransformation F G) {α β : Type u} (x : F (α → β)) (y : F α),
self.app β (Seq.seq x fun x => y) = Seq.seq (self.app (α → β) x) fun x => self.app α y
The theorem `ApplicativeTransformation.preserves_seq'` states that for any two types `α` and `β`, and any two applicative functors `F` and `G` (represented as `Type u → Type v` and `Type u → Type w` respectively), if we have an applicative transformation from `F` to `G` (denoted as `self : ApplicativeTransformation F G`), then this transformation preserves the `seq` operation.
In other words, given a function within the context of `F` and a value in `F`, when we first apply the function to the value using `Seq.seq` in the context of `F` and then transform the result into the context of `G` using `self.app`, it's the same as if we first transformed the function and the value into `G` and then applied the function to the value in the context of `G`.
This is expressed in the Lean theorem as: `self.app β (Seq.seq x fun x => y) = Seq.seq (self.app (α → β) x) fun x => self.app α y`.
More concisely: Given any applicative functors F and G with an applicative transformation self from F to G, the sequence of a function and a value in F transformed and then applied is equal to applying the transformed function to the transformed value in G. That is, `self.app β (Seq.seq x fun x => y) = Seq.seq (self.app (α → β) x) fun x => self.app α y`.
|