Functors between setoid-enriched categories compose

Identifier: F:cats-isfunctor-comp
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any three CatS.Category records C, D, E, any object maps Fo : C.obj -> D.obj and Go : D.obj -> E.obj, any morphism maps Fm and Gm over them, if CatS.IsFunctor C D Fo Fm and CatS.IsFunctor D E Go Gm then CatS.IsFunctor C E (fun a => Go (Fo a)) (fun a b f => Gm (Fo a) (Fo b) (Fm a b f)). CatS.IsFunctor is the three-fold conjunction of congruence with respect to the two hom-equivalences, preservation of identities up to the target's hom-equivalence, and preservation of composition up to the same. Each of the three composite obligations is discharged by applying Gm's congruence to F's law and then chaining G's own law through the target's homTrans -- so the whole proof runs on the hom-equivalence and never on Eq. This is the composition law of the category of categories; with CatS.isFunctor_id it makes the collection of setoid-enriched categories a category in the same unbundled style ADR-1609 used for AlgS.Module.IsModule.

Formal statement

theorem CatS.isFunctor_comp : ((x0 : CatS.Category) -> ((x1 : CatS.Category) -> ((x2 : CatS.Category) -> ((x3 : ((x3 : CatS.Category.obj x0) -> CatS.Category.obj x1)) -> ((x4 : ((x4 : CatS.Category.obj x0) -> ((x5 : CatS.Category.obj x0) -> ((x6 : CatS.Category.hom x0 x4 x5) -> CatS.Category.hom x1 (x3 x4) (x3 x5))))) -> ((x5 : ((x5 : CatS.Category.obj x1) -> CatS.Category.obj x2)) -> ((x6 : ((x6 : CatS.Category.obj x1) -> ((x7 : CatS.Category.obj x1) -> ((x8 : CatS.Category.hom x1 x6 x7) -> CatS.Category.hom x2 (x5 x6) (x5 x7))))) -> ((x7 : CatS.IsFunctor x0 x1 x3 x4) -> ((x8 : CatS.IsFunctor x1 x2 x5 x6) -> CatS.IsFunctor x0 x2 (fun (x9 : CatS.Category.obj x0) => x5 (x3 x9)) (fun (x9 : CatS.Category.obj x0) => fun (x10 : CatS.Category.obj x0) => fun (x11 : CatS.Category.hom x0 x9 x10) => x6 (x3 x9) (x3 x10) (x4 x9 x10 x11)))))))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 0 direct dependents

Evidence

cats-isfunctor-comp-1

Kind: kernel-term
Status: checked

Supports: CatS.isFunctor_comp admits through Kernel::add_declaration with an empty Kernel::axiom_footprint, and is recorded as a Declaration::Theorem (so the kernel checked its proof term). The rejection control m1_a_constant_morphism_map_is_not_a_functor refuses the identity functor's proof term against the statement whose morphism map has been mutated to a constant, with the unmutated positive twin admitted in the same test.

Checker command

out=$(RUST_MIN_STACK=1073741824 cargo test -p axeyum-lean-kernel --lib --release category_setoid -- --test-threads=4 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'test result: ok\. 29 passed; 0 failed')" -ge 1

Evidence notes

The pinned count is 29 (14 for the ADR-1620 layer plus 14 for ADR-1626's Sigma residue; RECOUNTED from the suite's own output, not incremented). the_category_results_are_checked_theorems asserts the Declaration KIND for all ten theorems, so a definition silently replacing a theorem fails the gate.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum-lean-kernel nat_prelude::category_setoid, lane categories-setoid, ADR-1620 (roadmap W3-3).",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/category_setoid.rs (declare_is_functor_comp, declared as CatS.isFunctor_comp); tests nat_prelude::category_setoid::category_setoid_tests::*."
}