Walking Arrow

definition example

The walking arrow $\underline{2}$ (DaoFP; 7 Sketches writes $2$) is the Free Category on the graph $v_1\stackrel{f_1}{\to }{v}_2$: two objects and three morphisms ${\mathrm{id}}_{v_1},f_1,{\mathrm{id}}_{v_2}$. A Functor $\underline{2}\to \mathcal{C}$ picks out a morphism of $\mathcal{C}$ (DaoFP Exercise 8.2.1); a functor $\underline{2}\to \mathbf{Set}$ is a Function (7 Sketches §3.3.1: the schema of a function is “a labeled version of $2$”, two tables — e.g. Beatles and Instruments).

Sources: 7 Sketches Eq. (3.8), Example 3.36, Exercises 3.37, 3.40, 3.90; DaoFP §8.1–8.2, §9.4 (“picking objects”), §20.1 (the monoidal walking arrow = $\mathbf{Bool}$); CTfS Exercise 4.1.2.28 (the free arrow category $[1]$), Example 4.3.1.4, Exercise 4.3.2.10

• Functors $\underline{2}\to \underline{3}$: six of them, determined by where the two objects go, since $\underline{3}$ is a preorder (Example 3.36, 7S Exercise 3.37). Functors $\bullet \to \bullet$ into $\bullet \rightrightarrows \bullet$ are not determined by objects (7S Exercise 3.40).
• The walking iso adds an arrow back; functors out of it pick isomorphisms (DaoFP Exercise 8.2.2). The discrete $2$ (two objects, no arrow) indexes products/coproducts and $\mathcal{C}\times \mathcal{C}\cong [2,\mathcal{C}]$ (DaoFP §10.2).
• $\underline{1}\times \underline{2}\cong \underline{2}$ (7S Exercise 3.90); the Limit of a diagram of shape $\underline{2}$ is its first object (DaoFP Exercise 9.5.1).
• CTfS’s $[1]$ (Exercise 4.1.2.28, Example 4.3.1.4): $\mathrm{Hom}(v_0,v_0)=\{\mathrm{id}\}$, $\mathrm{Hom}(v_0,v_1)=\{e\}$, $\mathrm{Hom}(v_1,v_0)=\varnothing$, $\mathrm{Hom}(v_1,v_1)=\{\mathrm{id}\}$. A functor $[1]\to \mathcal{D}$ is a morphism of $\mathcal{D}$, a natural transformation between two such is a commutative square, so $\mathrm{Fun}([1],\mathcal{D})$ is the arrow category of $\mathcal{D}$; and a natural transformation $F\Rightarrow G:\mathcal{C}\to \mathcal{D}$ is a functor $\mathcal{C}\times [1]\to \mathcal{D}$.
• As a Preorder it is the Booleans $\mathsf{false}\le \mathsf{true}$; enriching over it (monoidally) gives preorders.

JuliaLeanHaskell

Docs: ACSets API · Theories & presentations

using Catlab
@present WalkingArrow(FreeSchema) begin
  (v1, v2)::Ob
  f1::Hom(v1, v2)
end
# a functor 2 → Set is a FinFunction; as an ACSet on this schema:
@acset_type Fn(WalkingArrow)
F = @acset Fn begin v1 = 3; v2 = 2; f1 = [1, 2, 2] end   # the function 3 → 2 as a Fn-instance

-- Mathlib: the walking arrow is `Fin 2` as a preorder category, or `WalkingPair` (discrete) for products
#check CategoryTheory.Limits.WalkingPair        -- discrete two objects
#check CategoryTheory.ComposableArrows          -- ComposableArrows C n : functors from Fin (n+1)
example : CategoryTheory.Category (Fin 2) := inferInstance

-- a functor out of the walking arrow is a single arrow: a value of type (a -> b) with its endpoints
data Arrow' = Arrow' { src' :: String, tgt' :: String }   -- purely syntactic