CategoricalStructure
plain-language theorem explainer
CategoricalStructure enumerates five core elements of category theory as an inductive type with decidable equality and finite cardinality. Researchers embedding category theory into Recognition Science cite it to align categorical structure with configuration dimension five. The definition proceeds by direct enumeration of the five constructors deriving the required type classes.
Claim. The inductive type consists of five constructors corresponding to objects, morphisms, functors, natural transformations, and adjunctions, equipped with decidable equality, representation, boolean equality, and finite type structure.
background
In the Recognition Science treatment of category theory the five canonical structures are objects, morphisms, functors, natural transformations, and adjunctions. This enumeration is identified with configuration dimension D equal to five. Recognition maps are treated as functors that preserve J-cost structure, where the J-cost satisfies the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module documentation states that the Yoneda lemma embeds the recognition field into the functor category.
proof idea
The declaration is the inductive definition itself. It lists the five constructors directly and derives DecidableEq, Repr, BEq, and Fintype from the finite enumeration; no lemmas or tactics are invoked.
why it matters
This definition supplies the type whose cardinality is proved equal to five by the downstream theorem categoricalStructureCount and is packaged in the structure CategoryTheoryCert. It realizes the module claim that category theory contributes five dimensions inside the Recognition Science framework, consistent with the forcing chain that fixes D = 3 spatial dimensions while allowing auxiliary categorical structure of dimension five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.