Between two deloopings of a monoid map a natural transformation is exactly an intertwiner

Identifier: F:cats-isnat-ofmonoid
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any Sort 1 object type A, any two AlgS.Monoid records M and N, any two functions h, h' : M.carrier -> N.carrier, and any n : N.carrier such that N.equiv (N.op n (h x)) (N.op (h' x) n) for every x, the family constantly equal to n is a natural transformation from the delooping functor induced by h to the one induced by h' (CatS.IsNat over CatS.ofMonoid A M and CatS.ofMonoid A N). CatS.ofMonoid deloops a monoid into a category whose hom-family is M.carrier, whose composition is M.op and whose hom-equivalence is M.equiv; under that reading the naturality square IS the intertwining condition, so the theorem is the hypothesis applied. The direction matters: the square reads comp (eta b) (Fm f) ~ comp (Gm f) (eta a), which under comp = op is n . h x ~ h' x . n and not its converse.

Formal statement

theorem CatS.isNat_ofMonoid : ((x0 : Sort (1)) -> ((x1 : AlgS.Monoid) -> ((x2 : AlgS.Monoid) -> ((x3 : ((x3 : AlgS.Monoid.carrier x1) -> AlgS.Monoid.carrier x2)) -> ((x4 : ((x4 : AlgS.Monoid.carrier x1) -> AlgS.Monoid.carrier x2)) -> ((x5 : AlgS.Monoid.carrier x2) -> ((x6 : ((x6 : AlgS.Monoid.carrier x1) -> AlgS.Monoid.equiv x2 (AlgS.Monoid.op x2 x5 (x3 x6)) (AlgS.Monoid.op x2 (x4 x6) x5))) -> CatS.IsNat (CatS.ofMonoid x0 x1) (CatS.ofMonoid x0 x2) (fun (x7 : x0) => x7) (fun (x7 : x0) => x7) (fun (x7 : x0) => fun (x8 : x0) => fun (x9 : AlgS.Monoid.carrier x1) => x3 x9) (fun (x7 : x0) => fun (x8 : x0) => fun (x9 : AlgS.Monoid.carrier x1) => x4 x9) (fun (x7 : x0) => x5))))))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

cats-isnat-ofmonoid-1

Kind: kernel-term
Status: checked

Supports: CatS.isNat_ofMonoid admits through Kernel::add_declaration with an empty Kernel::axiom_footprint. The evaluation test the_delooping_reduces_to_the_monoids_own_fields reads the delooping's selectors out of the kernel -- hom reduces to M.carrier, id to M.e, comp g f to M.op g f and homEquiv to M.equiv -- and refuses each SWAPPED twin (M.op f g, the swapped M.equiv), so the composition order this theorem depends on is pinned rather than asserted. m3_the_naturality_square_is_indexed refuses a square with the wrong right-hand side, with its positive twin 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).

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_nat_of_monoid, declared as CatS.isNat_ofMonoid); tests nat_prelude::category_setoid::category_setoid_tests::*."
}