inductive Data.Functor.FunctorSum (F G : Type u → Type v) (α : Type u) : Type v

The sum (coproduct) functor $(\text{FunctorSum}\;F\;G)\;\alpha = F\;\alpha + G\;\alpha$.

Holds either an F α (via inl) or a G α (via inr). Mapping over a sum maps through whichever branch is inhabited.

$$\text{fmap}\;f\;(\text{inl}\;a) = \text{inl}\;(\text{fmap}\;f\;a)$$ $$\text{fmap}\;f\;(\text{inr}\;b) = \text{inr}\;(\text{fmap}\;f\;b)$$

• inl {F G : Type u → Type v} {α : Type u} : F α → FunctorSum F G α

  Left injection: wraps an $F\;\alpha$.

• inr {F G : Type u → Type v} {α : Type u} : G α → FunctorSum F G α

  Right injection: wraps a $G\;\alpha$.

@[implicit_reducible]

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

Functor instance for FunctorSum F G: maps through whichever branch is present.

$$\text{fmap}\;f\;(\text{inl}\;a) = \text{inl}\;(\text{fmap}\;f\;a)$$ $$\text{fmap}\;f\;(\text{inr}\;b) = \text{inr}\;(\text{fmap}\;f\;b)$$

Equations

• One or more equations did not get rendered due to their size.

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

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

Proceeds by cases: each branch reduces to the identity law of the respective functor.

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

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

Proceeds by cases: each branch reduces to the composition law of the respective functor.