Notation reference

Disclaimer. The content of this page is largely LM-generated. It was written as a stopgap to make the panproto system legible while we work through the book verifying and editing the content by hand. When a chapter has been verified or edited by a human, the parts that were verified or edited will be noted at the head of the chapter.

A lookup for the non-standard symbols and typographic conventions used in the book. The table lists each symbol, its meaning, and the chapter in which it is introduced.

Categorical notation

Symbol	Meaning	Introduced in
$C, D$	A category	Categories
$Ob (C)$	The class of objects of $C$	Categories
$C (A, B)$ , $Hom_{C} (A, B)$	The hom-set of morphisms $A \to B$ in $C$	Categories
$f : A \to B$	A morphism from $A$ to $B$	Categories
$g \circ f$	Composition of $f : A \to B$ and $g : B \to C$	Categories
$id_{A}$	The identity morphism on $A$	Categories
$A ≅ B$	$A$ and $B$ are isomorphic	Categories
$F : C \to D$	A functor	Functors and natural transformations
$α : F \Rightarrow G$	A natural transformation	Functors and natural transformations
$α_{A}$	The component of a natural transformation at $A$	Functors and natural transformations
$A \times B$ , $π_{1}, π_{2}$	Product of $A$ and $B$ with its projections	Universal properties
$A + B$ , $ι_{1}, ι_{2}$	Coproduct of $A$ and $B$ with its injections	Universal properties
$⟨ f, g ⟩$	Pairing into a product	Universal properties
$[f, g]$	Co-pairing out of a coproduct	Universal properties
$1$ , $0$	Terminal and initial objects	Universal properties
$D : J \to C$	A diagram in $C$ with shape $J$	Colimits and pushouts
$Δ X$	The constant functor at $X$	Colimits and pushouts

GAT and model notation

Symbol	Meaning	Introduced in
$T$ , $P$	A generalised algebraic theory / a panproto protocol	Algebraic and generalised algebraic theories
$Th (T)$	The syntactic contextual category of $T$	Algebraic and generalised algebraic theories
$Mod (T)$	The category of models of $T$	Algebraic and generalised algebraic theories
$M, S$	A model / a panproto schema	Protocols as theories, schemas as instances
$f : T_{1} \to T_{2}$	A theory morphism	Theory morphisms and instance migration
$Δ_{f}$ , $Σ_{f}$ , $Π_{f}$	The pullback and pushforward functors along $f$	Theory morphisms and instance migration
$m_{ij} : S_{i} \to S_{j}$	A migration between panproto schemas	Theory morphisms and instance migration
$Inst_{P}$	The instance functor for protocol $P$	Protocols as theories, schemas as instances

Lens notation

Symbol	Meaning	Introduced in
$get$ , $put$	The two functions of an asymmetric lens	Bidirectional lenses
GetPut, PutGet, PutPut	The lens round-trip laws	Bidirectional lenses
$P$	A protolens	Protolenses
$F (S), G (S)$	Source and target of a schema-indexed lens	Protolenses

Type-theoretic notation

Symbol	Meaning	Introduced in
`a -> b`, $a \to b$	A function type	Categories
`.`, $\circ$	Function composition (Haskell period, mathematical circle)	Categories
`id :: a -> a`	Haskell’s polymorphic identity function	Categories
`{l1 = e1, ...}`	Record literal (panproto-expr)	Syntax and semantics
`[e1 \| x <- e2]`	List comprehension (panproto-expr)	Syntax and semantics
`e ⟶ e'`	Small-step reduction	Syntax and semantics

Inline code and type names appear in monospace: SchemaBuilder, panproto-mig, compile. Italicised terms (category, protolens, complement) mark a definition being introduced on first appearance, and bold terms (Associativity, Identity) are concept labels the reader may want to scan for.

Every first mention of an external tool or library is a hyperlink to its canonical home page: Haskell, Rust, tree-sitter. Every first mention of a panproto module, type, or function is a hyperlink to the corresponding docs.rs page. Later mentions in the same chapter appear as plain prose.

Citations follow Pandoc syntax rendered by mdbook-bib in Chicago author-date style. Inline: @key for textual (“Smith 2010”), [@key] for parenthetical (“(Smith 2010)”), [-@key] for year only. Every cited work has a BibTeX entry in book/src/references.bib.

Keyboard shortcuts

panproto

Notation reference

Categorical notation

GAT and model notation

Lens notation

Type-theoretic notation

Typographic conventions