structure Data.Functor.Product (F G : Type u → Type v) (α : Type u) : Type v

The product functor $(\text{Product}\;F\;G)\;\alpha = F\;\alpha \times G\;\alpha$.

Pairs two functorial values at the same type parameter. Mapping over a product maps through both components independently.

$$\text{fmap}\;f\;(\text{Product}\;(a, b)) = \text{Product}\;(\text{fmap}\;f\;a,\;\text{fmap}\;f\;b)$$

• runProduct : F α × G α

  Unwrap the product to a pair: $F\;\alpha \times G\;\alpha$.

@[implicit_reducible]

instance Data.Functor.Product.instFunctor {F G : Type u_1 → Type u_2} [Functor F] [Functor G] : Functor (Product F G)

Functor instance for Product F G: maps through both components.

$$\text{fmap}\;f\;(\text{Product}\;(a, b)) = \text{Product}\;(\text{fmap}\;f\;a,\;\text{fmap}\;f\;b)$$

Equations

• Data.Functor.Product.instFunctor = { map := fun {α β : Type ?u.33} (f : α → β) (p : Data.Functor.Product F G α) => { runProduct := (f <$> p.runProduct.fst, f <$> p.runProduct.snd) } }

@[implicit_reducible]

instance Data.Functor.Product.instBEq {F G : Type u_1 → Type u_2} {α : Type u_1} [BEq (F α)] [BEq (G α)] : BEq (Product F G α)

BEq instance for Product F G α: both components must be equal.

$$(\text{Product}\;(a_1, b_1)) = (\text{Product}\;(a_2, b_2)) \iff a_1 = a_2 \land b_1 = b_2$$

Equations

• Data.Functor.Product.instBEq = { beq := fun (a b : Data.Functor.Product F G α) => a.runProduct.fst == b.runProduct.fst && a.runProduct.snd == b.runProduct.snd }

theorem Data.Functor.Product.map_id {F G : Type u_1 → Type u_2} {α : Type u_1} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] (x : Product F G α) : id <$> x = x

Identity law for product functors: $\text{fmap}\;\text{id} = \text{id}$.

If $F$ and $G$ are both lawful functors, their product is also lawful.

theorem Data.Functor.Product.map_comp {F G : Type u_1 → Type u_2} {β γ α : Type u_1} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] (f : β → γ) (g : α → β) (x : Product F G α) : (f ∘ g) <$> x = f <$> g <$> x

Composition law for product functors: $\text{fmap}\;(f \circ g) = \text{fmap}\;f \circ \text{fmap}\;g$.

Follows from the composition laws of $F$ and $G$ individually.