Functor.Comp.ext
theorem Functor.Comp.ext :
∀ {F : Type u → Type w} {G : Type v → Type u} {α : Type v} {x y : Functor.Comp F G α}, x.run = y.run → x = y := by
sorry
The theorem `Functor.Comp.ext` states that for all type functions `F` mapping from type `u` to type `w`, `G` mapping from type `v` to type `u` and any type `α` of type `v`, given two elements `x` and `y` of the composite functor `Functor.Comp F G α`, if the application of the `Functor.Comp.run` function on `x` results in the same value as the application on `y`, then `x` and `y` must be equal. This theorem essentially asserts the injectiveness of the `Functor.Comp.run` function, saying that no two distinct values in the composite functor can map to the same value in the composed functor `F (G α)`.
More concisely: If `F : Type u -> Type w` and `G : Type v -> Type u` are functors, and `x` and `y` are elements of `Functor.Comp F G α`, then `Functor.Comp.run F G x = Functor.Comp.run F G y` implies `x = y`.
|
Functor.Comp.run_pure
theorem Functor.Comp.run_pure :
∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] {α : Type v} (x : α),
(pure x).run = pure (pure x)
The theorem `Functor.Comp.run_pure` states that for all type constructors `F` and `G`, where `F` maps a type from universe `u` to `w` and `G` maps a type from `v` to `u`, given that `F` and `G` are both Applicative functors, and for any type `α` in universe `v` and any term `x` of type `α`, running the composition functor on `pure x` (i.e., applying `pure` to `x` and then using `run` function on it) yields the same result as applying `pure` twice on `x` (i.e., first applying `pure` to `x` and then again applying `pure` to the result). In essence, it is a property of applicative composition of functors.
More concisely: For all Applicative functors F : Type u -> Type w and G : Type v -> Type u, the application of the composition functor (F ∘ G) to a term x : Type v is equivalent to applying F twice to x, i.e., F (G x) ≈ F (pure x).
|