dedekind::morphologies::singleton_image_breadcrumb Namespace Reference

Classes
struct	Successor
	The successor \(S : N \to N\) as an arrow, over any carrier with the NNO step: the one spelling of the Peano successor where an IsArrow is needed (image, graph, the NNO witness), in place of a struct per site. More...

Variables
constexpr auto	s0 = η(0)
constexpr auto	s1 = image(Successor<int>{}, s0)

Detailed Description

archimedean__Formal_Verification

archimedean__Image_Of_Singleton_Under_Peano_Successor

Categorical breadcrumbs for image(f, Singleton) (#602 layer-1).

The witness arrow is the Peano successor S(x) = x + 1, the canonical carrier-level instance of the successor / generator vocabulary this partition already names (see the §archimedean__Vocabulary_Notes_388 block). We pin three structural claims so the type-checker carries the proof of image's behaviour on the cardinality-1 case:

(i) image is defined for IsArrow inputs. (ii) Tier preservation: cardinality 1 ↦ 1, IsExtensional preserved on the codomain side. (iii) Kleisli factoring: image(f, s) is the cardinality-1 instance of the powerset-monad bind s >>= (η ∘ f), witnessed by image(f, s) == singleton(f(origin(s))) and image(f, s) == (s >>= (η ∘ f)).

Placing the witness here rather than in :sets:singleton keeps the upstream partition free of its own assertion machinery; :archimedean is downstream of :sets and is the natural home for a Peano-successor test (per PR #604 review).