QPF.id_map
theorem QPF.id_map : ∀ {F : Type u → Type u} [inst : Functor F] [q : QPF F] {α : Type u} (x : F α), id <$> x = x := by
sorry
This theorem, `QPF.id_map`, states that for any type `F` that is a functor and a Quasi-Polynomial Functor (QPF), and for any type `α` and value `x` of type `F α`, applying the identity function (`id`) using the functor's `fmap` operation (`<$>`) to `x` returns `x` itself. In other words, this theorem asserts the identity law for the functor `F` when `F` is also a QPF, stating that mapping the identity function over a value does not change the value.
More concisely: For any Quasi-Polynomial Functor (QPF) `F` and type `α`, the application of the identity function through `F`'s `fmap` operation leaves the value unchanged: `id <$> x = x`.
|
QPF.comp_map
theorem QPF.comp_map :
∀ {F : Type u → Type u} [inst : Functor F] [q : QPF F] {α β γ : Type u} (f : α → β) (g : β → γ) (x : F α),
(g ∘ f) <$> x = g <$> f <$> x
This theorem, named 'QPF.comp_map', states that for any types `α`, `β`, and `γ`, and for any functions `f` from `α` to `β` and `g` from `β` to `γ`, operating on any instance `x` of type F α with the composition of `g` and `f` (i.e., `(g ∘ f) <$> x`) is equivalent to first applying `f` to `x`, then applying `g` to the result (i.e., `g <$> f <$> x`). Here, `<$>` denotes a functor map operation. The theorem holds for any Functor `F` that also has a Quotient Polynomial Functor (QPF) structure.
More concisely: For any Functor `F` with a QPF structure and any functions `f : α → β` and `g : β → γ`, the composition `(g ∘ f) <$> x` is equivalent to `g <$> f <$> x` for any `x : F α`.
|
QPF.Fix.rec_eq
theorem QPF.Fix.rec_eq :
∀ {F : Type u → Type u} [inst : Functor F] [q : QPF F] {α : Type u} (g : F α → α) (x : F (QPF.Fix F)),
QPF.Fix.rec g (QPF.Fix.mk x) = g (QPF.Fix.rec g <$> x)
The theorem `QPF.Fix.rec_eq` states that for any functor `F`, which forms a Quotient of Polynomial Functor (QPF), and any function `g : F α → α`, applying the recursor `QPF.Fix.rec g` to the result of the QPF constructor `QPF.Fix.mk x` on an `x : F (QPF.Fix F)` is the same as applying `g` to the result of transforming `x` with the functor map (`<$>`) of the same recursor `QPF.Fix.rec g`. In other words, the process of constructing and then destructing (recursion) an algebraic data type defined by a QPF commutes with applying the function `g`. This theorem provides the defining property of the recursion primitive for algebraic data types defined by QPFs.
More concisely: For any QPF functor `F` and function `g : F α → α`, the application of `QPF.Fix.rec g` to `QPF.Fix.mk x` is equal to `g (<$> QPF.Fix.rec g x)`.
|
QPF.supp_eq_of_isUniform
theorem QPF.supp_eq_of_isUniform :
∀ {F : Type u → Type u} [inst : Functor F] [q : QPF F],
QPF.IsUniform →
∀ {α : Type u} (a : (QPF.P F).A) (f : (QPF.P F).B a → α), Functor.supp (QPF.abs ⟨a, f⟩) = f '' Set.univ
This theorem states that for any type constructor `F` that is a Quasi-Polynomial Functor (QPF) with a functor instance, if `F` is uniform (meaning all polynomial functors representing a single value have the same range), then for any type `α` and any function `f` from the object part of `F`'s polynomial functor to `α`, the support of the abstraction of the functor object `a` and `f` (which is the set of `α` values that the functor contains) is equal to the image of the entire set of `α` under the function `f`. This essentially means that all values of `α` are present in the QPF if it is uniform.
More concisely: For any Quasi-Polynomial Functor `F` with a uniform instance, the image of `F`'s polynomial functor equals the set of values in the domain when mapping to any type `α`.
|
QPF.recF_eq_of_Wequiv
theorem QPF.recF_eq_of_Wequiv :
∀ {F : Type u → Type u} [inst : Functor F] [q : QPF F] {α : Type u} (u : F α → α) (x y : (QPF.P F).W),
QPF.Wequiv x y → QPF.recF u x = QPF.recF u y
The theorem `QPF.recF_eq_of_Wequiv` states that for any functor `F` of type `Type u -> Type u` with a `QPF` instance, and for any type `α` of `Type u`, the function `recF` is insensitive to the representation of its arguments. That is, if `x` and `y` are two elements of `QPF.P F.W` such that `x` and `y` are weakly equivalent (denoted by `QPF.Wequiv x y`), then applying `recF` to `u` and `x` (written as `QPF.recF u x`) yields the same result as applying `recF` to `u` and `y` (written as `QPF.recF u y`). In simpler terms, this theorem asserts that `recF` behaves in a consistent manner with respect to weakly equivalent arguments.
More concisely: For any type `α` and functor `F` with `QPF` instance, `QPF.recF u (x : QPF.P F.W) = QPF.recF u (y : QPF.P F.W)` whenever `x` and `y` are weakly equivalent.
|