Many-sorted algebra: core layer

SSet

For a type $S$ (in universe $u$), $\mathrm{SSet}\;S$ is defined to be the type of functions $S \to \mathrm{Type}\;u$. An element $A : \mathrm{SSet}\;S$ is therefore an $S$-indexed family of types; the value of $A$ at an index $s : S$ is written $A_s$ below. This type itself lives one universe level up ($\mathrm{Type}\,(u+1)$). It is introduced as an abbreviation, so it is definitionally equal to $S \to \mathrm{Type}\;u$ and unfolds freely.

SMap

Given an implicit type $S$ and two explicit families $A, B : \mathrm{SSet}\;S$, the type $\mathrm{SMap}\;A\;B$ is defined to be the dependent function type

$$\prod_{s : S} \big( A_s \to B_s \big).$$

That is, an element of $\mathrm{SMap}\;A\;B$ assigns to every index $s : S$ a function from $A_s$ to $B_s$. No compatibility or naturality condition is imposed; it is just an index-wise family of ordinary functions.

SSub

Given an implicit type $S$ and an explicit family $A : \mathrm{SSet}\;S$, the type $\mathrm{SSub}\;A$ is defined to be

$$\prod_{s : S} \mathcal{P}(A_s),$$

where $\mathcal{P}(A_s)$ is the type of subsets of $A_s$ (predicates on $A_s$). So an element $X : \mathrm{SSub}\;A$ picks out, for each index $s$, a subset $X_s \subseteq A_s$.

PartialOrder (SSub A) instance

For every implicit type $S$ and every $A : \mathrm{SSet}\;S$, this registers a partial-order structure on $\mathrm{SSub}\;A$. The order is defined by

$$X \le Y \iff \forall s : S,\; X_s \subseteq Y_s,$$

i.e. index-wise inclusion of subsets. The instance also supplies the three proofs making this a partial order: reflexivity ($X \le X$ always holds, since $X_s \subseteq X_s$ for each $s$); transitivity (if $X \le Y$ and $Y \le Z$ then $X \le Z$, by chaining $X_s \subseteq Y_s \subseteq Z_s$ at each $s$); and antisymmetry (if $X \le Y$ and $Y \le X$ then $X = Y$, obtained by function extensionality over $s$ together with antisymmetry of set inclusion at each index). In particular equality of elements of $\mathrm{SSub}\;A$ is index-wise equality of subsets.

delta

Given an implicit type $S$ equipped with decidable equality, an implicit family $A : \mathrm{SSet}\;S$, an explicit index $t : S$, and an explicit subset $U : \mathcal{P}(A_t)$, the term $\mathrm{delta}\;t\;U$ is the element of $\mathrm{SSub}\;A$ whose value at an index $s : S$ is:

$$(\mathrm{delta}\;t\;U)_s \;=\; \begin{cases} U, & \text{if } s = t,\\[2pt] \varnothing \subseteq A_s, & \text{if } s \neq t. \end{cases}$$

In the first branch, where a proof $h : s = t$ is available, $U$ (a subset of $A_t$) is reinterpreted as a subset of $A_s$ by transporting along the equality $h$. In every branch with $s \neq t$ the value is the empty subset of $A_s$. So $\mathrm{delta}\;t\;U$ is the family that is concentrated at the single index $t$, carrying $U$ there and nothing anywhere else.

SFinite

Given an implicit type $S$ and an explicit family $A : \mathrm{SSet}\;S$, $\mathrm{SFinite}\;A$ is defined to be the proposition that the dependent-sum type

$$\Sigma_{s : S}\; A_s$$

(the total space of the family, whose elements are pairs $(s, a)$ with $a : A_s$) is a finite type, in the sense of Mathlib's Finite typeclass-style predicate. This simultaneously constrains $S$ and every fiber $A_s$: the disjoint union of all fibers must have finitely many elements. It says nothing directly beyond finiteness of that sigma type (e.g. it is satisfied when $S$ is empty).

Signature

For a type $S$ (in universe $u$), $\mathrm{Signature}\;S$ is defined to be the type of functions

$$\mathrm{List}\;S \;\to\; S \;\to\; \mathrm{Type}\;u.$$

An element $\mathrm{sig} : \mathrm{Signature}\;S$ therefore assigns, to each finite word $w : \mathrm{List}\;S$ of input sorts and each output sort $s : S$, a type $\mathrm{sig}\;w\;s$; this type is to be thought of as the collection of operation symbols with input arity $w$ and result sort $s$. The type $\mathrm{Signature}\;S$ lives in $\mathrm{Type}\,(u+1)$.

SigFinite

Given an implicit type $S$ and an explicit $\mathrm{sig} : \mathrm{Signature}\;S$, $\mathrm{SigFinite}\;\mathrm{sig}$ is defined to be the proposition that the iterated dependent-sum type

$$(w : \mathrm{List}\;S) \times (s : S) \times \mathrm{sig}\;w\;s$$

is finite (Finite). Elements of that type are triples consisting of an input word $w$, an output sort $s$, and an operation symbol in $\mathrm{sig}\;w\;s$. So $\mathrm{SigFinite}\;\mathrm{sig}$ asserts that, across all input words and all output sorts together, there are only finitely many operation symbols in total.

Args

Given an implicit type $S$ and an explicit family $A : \mathrm{SSet}\;S$, $\mathrm{Args}\;A$ is a function $\mathrm{List}\;S \to \mathrm{Type}\;u$ defined by recursion on the list:

$$\mathrm{Args}\;A\;[\,] \;=\; \mathrm{PUnit}, \qquad \mathrm{Args}\;A\;(s :: w) \;=\; A_s \times \mathrm{Args}\;A\;w.$$

Here $\mathrm{PUnit}$ is a one-element type. Consequently, for a word $w = [s_1, s_2, \dots, s_n]$, the type $\mathrm{Args}\;A\;w$ is the nested product $A_{s_1} \times (A_{s_2} \times (\cdots \times (A_{s_n} \times \mathrm{PUnit})))$: a tuple with exactly one entry drawn from $A_{s_i}$ for each position $i$ of the word, and for the empty word it is the singleton type.

Args.map

Given an implicit type $S$, implicit families $A, B : \mathrm{SSet}\;S$, an explicit $f : \mathrm{SMap}\;A\;B$ (an index-wise family of functions $f_s : A_s \to B_s$), and an implicit word $w : \mathrm{List}\;S$, the function $\mathrm{Args.map}\;f$ maps $\mathrm{Args}\;A\;w \to \mathrm{Args}\;B\;w$ by recursion on $w$:

• on the empty word it returns the unique element $\mathrm{PUnit.unit}$;
• on a cons word, given a pair $(a, \mathrm{rest})$ with $a : A_{s}$ for the head sort $s$, it returns $\big(f_{s}(a),\; \mathrm{Args.map}\;f\;\mathrm{rest}\big)$.

In effect it applies $f$ at the appropriate sort to each component of the tuple, leaving the shape (the word $w$) unchanged.

Args.All

Given an implicit type $S$, an implicit family $A : \mathrm{SSet}\;S$, an explicit predicate $P : \prod_{s : S}(A_s \to \mathrm{Prop})$, and an implicit word $w : \mathrm{List}\;S$, $\mathrm{Args.All}\;P$ is a predicate on $\mathrm{Args}\;A\;w$ defined by recursion on $w$:

$$\mathrm{Args.All}\;P\;(\text{tuple over }[\,]) \;=\; \mathrm{True}, \qquad \mathrm{Args.All}\;P\;(a, \mathrm{rest}) \;=\; P_{s}(a) \;\wedge\; \mathrm{Args.All}\;P\;\mathrm{rest},$$

where $s$ is the head sort. Thus $\mathrm{Args.All}\;P\;\mathrm{args}$ holds exactly when $P$ holds of every component of the tuple $\mathrm{args}$; for the empty word it is vacuously true.

Args.map_id

This theorem (tagged as a simp lemma) states: for every implicit type $S$ and every family $A : \mathrm{SSet}\;S$, for every implicit word $w : \mathrm{List}\;S$ and every tuple $\mathrm{args} : \mathrm{Args}\;A\;w$,

$$\mathrm{Args.map}\;\big(\lambda\,\_\;a.\;a\big)\;\mathrm{args} \;=\; \mathrm{args}.$$

That is, mapping the tuple with the family of identity functions (the function that at every sort sends $a$ to $a$) yields the original tuple unchanged.

Args.map_comp

This theorem states: for every implicit type $S$, implicit families $A, B, C : \mathrm{SSet}\;S$, explicit $g : \mathrm{SMap}\;B\;C$ and explicit $f : \mathrm{SMap}\;A\;B$, for every implicit word $w : \mathrm{List}\;S$ and every tuple $\mathrm{args} : \mathrm{Args}\;A\;w$,

$$\mathrm{Args.map}\;\big(\lambda\,s\;a.\;g_s(f_s(a))\big)\;\mathrm{args} \;=\; \mathrm{Args.map}\;g\;\big(\mathrm{Args.map}\;f\;\mathrm{args}\big).$$

That is, mapping with the index-wise composite of $g$ after $f$ equals first mapping with $f$ and then mapping the result with $g$.

Algebra

Given an implicit type $S$ and an explicit signature $\mathrm{sig} : \mathrm{Signature}\;S$, the structure $\mathrm{Algebra}\;\mathrm{sig}$ bundles two data:

• a field $\mathrm{carrier} : \mathrm{SSet}\;S$, an $S$-indexed family of types (the underlying carriers, one per sort);
• a field $\mathrm{op}$: for every implicit word $w : \mathrm{List}\;S$ and every implicit sort $s : S$, a function taking an operation symbol $\sigma : \mathrm{sig}\;w\;s$ and an argument tuple in $\mathrm{Args}\;\mathrm{carrier}\;w$ and producing an element of $\mathrm{carrier}_s$.

So an algebra interprets each operation symbol of profile $(w, s)$ as an actual operation from tuples of carrier elements matching $w$ to a carrier element of sort $s$. No equational axioms are imposed.

Hom

Given an implicit type $S$, an implicit signature $\mathrm{sig} : \mathrm{Signature}\;S$, and two explicit algebras $A, B : \mathrm{Algebra}\;\mathrm{sig}$, the structure $\mathrm{Hom}\;A\;B$ bundles:

• a field $\mathrm{toFun} : \mathrm{SMap}\;A.\mathrm{carrier}\;B.\mathrm{carrier}$, i.e. for each sort $s$ a function $\mathrm{toFun}_s : A.\mathrm{carrier}_s \to B.\mathrm{carrier}_s$;
• a field $\mathrm{map\_op}$: for all implicit $w : \mathrm{List}\;S$ and implicit $s : S$, for every operation symbol $\sigma : \mathrm{sig}\;w\;s$ and every argument tuple $\mathrm{args} : \mathrm{Args}\;A.\mathrm{carrier}\;w$,

$$\mathrm{toFun}_s\big(A.\mathrm{op}\;\sigma\;\mathrm{args}\big) \;=\; B.\mathrm{op}\;\sigma\;\big(\mathrm{Args.map}\;\mathrm{toFun}\;\mathrm{args}\big).$$

That is, applying the map after an $A$-operation equals applying the corresponding $B$-operation to the componentwise-mapped arguments, for every operation symbol.

Hom.id

Given an implicit type $S$, an implicit signature $\mathrm{sig}$, and an explicit algebra $A : \mathrm{Algebra}\;\mathrm{sig}$, $\mathrm{Hom.id}\;A$ is the element of $\mathrm{Hom}\;A\;A$ whose $\mathrm{toFun}$ is the index-wise identity $\lambda\,\_\;a.\;a$ (at every sort, $a \mapsto a$), together with the required proof of the $\mathrm{map\_op}$ condition for this choice (discharged by simplification).

Hom.comp

Given an implicit type $S$, an implicit signature $\mathrm{sig}$, implicit algebras $A, B, C : \mathrm{Algebra}\;\mathrm{sig}$, an explicit $g : \mathrm{Hom}\;B\;C$ and an explicit $f : \mathrm{Hom}\;A\;B$, the term $\mathrm{Hom.comp}\;g\;f$ is the element of $\mathrm{Hom}\;A\;C$ whose $\mathrm{toFun}$ at each sort $s$ is $a \mapsto g.\mathrm{toFun}_s\big(f.\mathrm{toFun}_s(a)\big)$, together with a proof of its $\mathrm{map\_op}$ condition (established using the $\mathrm{map\_op}$ fields of $f$ and $g$ and the lemma $\mathrm{Args.map\_comp}$). Note the argument order: $\mathrm{Hom.comp}\;g\;f$ is "first $f$, then $g$".