Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A strict 2-category read as a Cat-enriched category
Example
Let be any strict 2-category with a set of objects and small hom-categories. Then itself is an example of a -enriched category: the hom-object from to is the hom-category , and enriched composition is horizontal composition.
Facts & Assumptions
Given: A strict 2-category with a set of objects and small hom-categories.
Such a strict 2-category is exactly the same thing as a -enriched category (A Cat-enriched category is exactly a strict 2-category with a set of objects and small hom-categories).
Verification
The hom-categories, horizontal composition, and identity 1-morphisms of are exactly the data that [L1] identifies with the hom-objects, enriched composition, and enriched identities of a -enriched category.
Therefore every such strict 2-category is read directly as a -enriched category.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Emily Riehl, Categorical Homotopy Theory, Section 3.1 (standard reference, not scraped)