Finite-category specifications

A client specifies a finite category by a count of objects, a count of non-identity morphisms at each pair of objects, a composition function on those morphisms, and a Bool equation asserting associativity. The identities are not the client's to supply: one is reserved at the index one past the client's range in each endo-hom, so the identity laws hold of the reserved index by construction and only associativity is checked.

Main definitions

CategoryTheory.FinCat — the specification type.

CategoryTheory.FinCat.homCountOf, CategoryTheory.FinCat.homCount — the hom-count including the reserved identity.

CategoryTheory.FinCat.Mor, CategoryTheory.FinCat.emb, CategoryTheory.FinCat.id — the full hom type, the embedding of a client morphism, and the reserved identity.

CategoryTheory.FinCat.compTotalOf, CategoryTheory.FinCat.compTotal — composition on the full hom types.

CategoryTheory.FinCat.assocCheckOf, CategoryTheory.FinCat.assocCheck — the decidable associativity check on triples of client morphisms.

Main statements

FinCat.id_comp, FinCat.comp_id — the identity laws, at variable indices.

FinCat.assocCheck_eq_true_iff — the check reflects associativity on client triples.

FinCat.compTotal_assoc — associativity on all triples.

Implementation notes

Composition takes the hom-count matrix as primitive rather than a total morphism count with domain and codomain projections. Under the matrix the indexing makes well-typedness a typing obligation, and composition is total; under the projections it is partial, and the client and the checker carry the two side conditions relating the endpoints of a composite to those of its factors.

The identity is reserved one past the client's range rather than at index 0 so that the embedding of a client morphism into the full hom type is index-preserving both on and off the diagonal. Reserving 0 makes the embedding Fin.succ on the diagonal and the identity map off it, so a client's composition function would take arguments in one numbering and return a result in another.

Total composition dispatches on whether either argument is the reserved identity, which involves the equation i = j between objects. That equation is used only inside a Prop: each branch returns ⟨x.val, proof⟩, so the value component crosses with no Eq.rec and only the bound is transported. This is core's own idiom for Fin.castLE.

The specification type is declared structure _root_.CategoryTheory.FinCat inside namespace FinCat, so that its field types name the arithmetic unqualified and the module needs only one namespace block.

This module has no imports. Its Fin and Nat material is in the prelude, and nothing in its content mentions a category.

References

[JohnsonYau2021] § 1.1 — the notion of category, of which this module's specification type is a presentation.

Tags

category, finite category, decidable, constructive, choice-free

The number of morphisms i ⟶ j a specification with these counts has: the client's count, plus the reserved identity on the diagonal.

The embedding of a client morphism into the full hom type. It is index-preserving, on and off the diagonal.

Off the diagonal the reserved identity contributes nothing.

On the diagonal it contributes one.

An index at or beyond the client's count exists only on the diagonal: off the diagonal the conditional in homCountOf contributes 0.

An index at or beyond the client's count is the reserved identity index of its object.

Composition on the full hom types, dispatching on whether either argument is the reserved identity. Both elided bounds are objEq_of_le: the value component crosses unchanged and only the bound is transported.

Associativity of the total composition on triples of client morphisms, as a Bool. The composition in the statement is the total one, so a composite landing on the reserved identity index is covered.

A finite-category specification: a count of objects, a count of non-identity morphisms at each pair, a composition function on those morphisms, and the associativity check. The client designates no identities, states no identity laws, and supplies no domain or codomain data.

The number of objects, indexed by Fin objCount.

The number of non-identity morphisms i ⟶ j.

Composition of client morphisms. It lands in the full hom type, because a composite of two non-identity morphisms may be an identity.

Associativity on triples of client morphisms. A client with a concrete category discharges this by rfl.

The number of morphisms i ⟶ j of S.

The morphisms i ⟶ j of S, client morphisms and the reserved identity together. An abbrev rather than a def: instance search does not unfold a plain def, so DecidableEq (S.Mor i j) would not be found and compCheckOf's and natCheckOf's decide bodies — equalities at Mor — would not elaborate.

The embedding of a client morphism of S into the full hom type.

The reserved identity at i, at the index one past the client's range.

Composition on the full hom types of S.

Associativity of S on triples of client morphisms, as a Bool.

An index at or beyond S's client count exists only on the diagonal.

An index at or beyond S's client count is the reserved identity index.

The reserved identity is a left identity for the total composition.

The reserved identity is a right identity for the total composition.

The specification with no objects. deriving Inhabited fails, there being no Inhabited instance for the Prop-valued assoc field.

The associativity check reflects associativity on triples of client morphisms.

Associativity of the total composition, on all triples of morphisms of S. A triple of client morphisms is the check's; a triple with the reserved identity among it is the identity laws'.