class Control.Arrow (Cat : Type u → Type u → Type v) extends Control.Category Cat : Type (max (u + 1) v)

An Arrow is a Category with the ability to lift pure functions and apply them in parallel.

Operations:

• arr: Lift a pure function $f : \alpha \to \beta$ into the arrow. $$\text{arr}(f) : \text{Cat}(\alpha, \beta)$$
• first: Apply an arrow to the first component of a pair, passing the second through. $$\text{first}(f) : \text{Cat}(\alpha \times \gamma, \beta \times \gamma)$$
• second: Apply an arrow to the second component. $$\text{second}(f) : \text{Cat}(\gamma \times \alpha, \gamma \times \beta)$$
• split: Apply two arrows in parallel (product/fanout): $$f \mathbin{\&\&\&} g : \text{Cat}(\alpha \times \gamma, \beta \times \delta)$$

• id {α : Type u} : Cat α α
• comp {α β γ : Type u} : Cat α β → Cat β γ → Cat α γ
• arr {α β : Type u} : (α → β) → Cat α β

  Lift a pure function into the arrow.

• first {α β γ : Type u} : Cat α β → Cat (α × γ) (β × γ)

  Apply an arrow to the first component of a pair. $$\text{first}(f)(a, c) = (f(a), c)$$

• second {α β γ : Type u} : Cat α β → Cat (γ × α) (γ × β)

  Apply an arrow to the second component of a pair. $$\text{second}(f)(c, a) = (c, f(a))$$

• split {α β γ δ : Type u} : Cat α β → Cat γ δ → Cat (α × γ) (β × δ)

  Apply two arrows in parallel. $$\text{split}(f, g)(a, c) = (f(a), g(c))$$

class Control.ArrowChoice (Cat : Type u → Type u → Type v) extends Control.Arrow Cat : Type (max (u + 1) v)

ArrowChoice extends Arrow with the ability to choose between branches, working with sum types (Either).

Operations:

• left: Apply an arrow to the Left case, passing Right through. $$\text{left}(f)(\text{Left}(a)) = \text{Left}(f(a))$$ $$\text{left}(f)(\text{Right}(c)) = \text{Right}(c)$$
• right: Apply an arrow to the Right case.
• fanin: Merge two arrows: $$f \mathbin{|||} g : \text{Cat}(\text{Either}(\alpha, \gamma), \beta)$$

• id {α : Type u} : Cat α α
• comp {α β γ : Type u} : Cat α β → Cat β γ → Cat α γ
• arr {α β : Type u} : (α → β) → Cat α β
• first {α β γ : Type u} : Cat α β → Cat (α × γ) (β × γ)
• second {α β γ : Type u} : Cat α β → Cat (γ × α) (γ × β)
• split {α β γ δ : Type u} : Cat α β → Cat γ δ → Cat (α × γ) (β × δ)
• left {α β γ : Type u} : Cat α β → Cat (Data.Either α γ) (Data.Either β γ)

  Apply an arrow to the Left branch of an Either, passing Right through. $$\text{left}(f)(\text{Left}(a)) = \text{Left}(f(a)), \quad \text{left}(f)(\text{Right}(c)) = \text{Right}(c)$$

• right {α β γ : Type u} : Cat α β → Cat (Data.Either γ α) (Data.Either γ β)

  Apply an arrow to the Right branch of an Either, passing Left through. $$\text{right}(f)(\text{Right}(a)) = \text{Right}(f(a)), \quad \text{right}(f)(\text{Left}(c)) = \text{Left}(c)$$

• fanin {α γ β : Type u} : Cat α γ → Cat β γ → Cat (Data.Either α β) γ

  Merge two arrows from different branches into a single output. $$\text{fanin}(f, g)(\text{Left}(a)) = f(a), \quad \text{fanin}(f, g)(\text{Right}(c)) = g(c)$$

@[implicit_reducible]

instance Control.instArrowFun : Arrow Fun

Equations

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

@[implicit_reducible]

instance Control.instArrowChoiceFun : ArrowChoice Fun

Equations

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