Boolean Starter Package: the algebra on the carrier bool and the canonical embedding 𝔹 ↪ 𝕂3. More...

#include <functional>
#include <utility>
import dedekind.algebra:universal;
import dedekind.sets;
import dedekind.order;
import dedekind.category;

Include dependency graph for boolean.cppm:

Namespaces
namespace	dedekind::category

Functions
template<typename S> requires requires(S&& s) { dedekind::sets::image(embed_𝔹_𝕂3_, std::forward<S>(s)); }
constexpr auto	dedekind::algebra::embed_𝔹_𝕂3 (S &&s)
	Set-level lift of `embed_𝔹_𝕂3_:` image of a Boolean set `S` under the canonical mono 𝔹 ↪ 𝕂3.

Variables
constexpr auto	dedekind::algebra::embed_𝔹_𝕂3_
	Canonical embedding `𝔹` `↪` `𝕂3:` bool → Ternary.
template<>
constexpr bool	dedekind::category::is_monic_arrow_v< std::decay_t< decltype(dedekind::algebra::embed_𝔹_𝕂3_)> >
template<>
constexpr bool	dedekind::category::is_embedding_functor_v< std::decay_t< decltype(dedekind::algebra::embed_𝔹_𝕂3_)> > = true
template<>
constexpr bool	dedekind::category::is_monotone_v< std::decay_t< decltype(dedekind::algebra::embed_𝔹_𝕂3_)>, std::less_equal<> >

Detailed Description

Boolean Starter Package: the algebra on the carrier bool and the canonical embedding 𝔹 ↪ 𝕂3.

@partition :boolean

Copyright: 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

algebra_boolean__Starter_Intent

This partition offers a small, explicit entry point for Boolean algebra in the set-builder DSL: the algebraic witnesses on the carrier bool and the mono 𝔹 ↪ 𝕂3. The universe itself is dedekind::sets::𝔹 (𝔸<bool>{}), defined once upstream in :sets:boundaries.

algebra_boolean__Notation

𝔹: the Boolean universe 𝔸<bool>{} over the carrier bool (dedekind::sets::𝔹); carrier-type positions use bool directly. static_assert(IsField<bool, bit_xor, bit_and>) carries the algebra on the carrier. Bool is the bottom of the algebraic tower, so the characteristic morphism of 𝔹-as-subobject coincides with the universe (no proper ambient super-object). Every other species symbol (ℕ, ℤ, ℚ, ℝ, ℂ, 𝔻) is likewise the universe over its carrier; a subobject such as ℕ ⊂ ℤ is an :order halfspace.

algebra_boolean__Paper_Alignment

In the paper's Feature Cube (bool row), logical (||, &&) and bitwise (|, &) operators over bool share the same lattice behavior (join/meet, identities, absorbers, and distributivity). The test suite validates this alignment explicitly.

Sets over 𝔹 = 𝔸<bool> are written point-free, 𝔹 | (π == true): no element variable is bound.

Note: "La matematica non e una collezione di trucchi: e grammatica delle forme." (Mathematics is not a bag of tricks; it is a grammar of forms.) — Emma Castelnuovo as quoted by B. L. van der Waerden (1975)

Function Documentation

◆ embed_𝔹_𝕂3()

template<typename S>
requires requires(S&& s) { dedekind::sets::image(embed_𝔹_𝕂3_, std::forward<S>(s)); }

auto dedekind::algebra::embed_𝔹_𝕂3 ( S && s )

constexprexport

Set-level lift of embed_𝔹_𝕂3_: image of a Boolean set S under the canonical mono 𝔹 ↪ 𝕂3.

Layer-1 entry per #602 (sister to embed_𝔹_ℕ in :numbers:natural, PR #624). Names the construction at the call site rather than re-spelling image(embed_𝔹_𝕂3_, S). Accepted input S is anything dedekind::sets::image already dispatches on — Singleton (:sets:singleton), std::set<bool> / std::unordered_set<bool> (:sets:extensional); lazy predicate sets join the dispatch table when #602's layer 2 lands.

Mathematically: the image of S under the canonical mono 𝔹 ↪ 𝕂3 is a subset of {Ternary::False, Ternary::True} ⊂ 𝕂3 containing whichever bool elements are in S. Ternary::Unknown is by construction not in the image — the structural reason the arrow is monic but not surjective.

Variable Documentation

◆ embed_𝔹_𝕂3_

auto dedekind::algebra::embed_𝔹_𝕂3_

inlineconstexprexport

Initial value:

=
    arrow<bool, dedekind::category::Ternary>(
        [](const bool& b) noexcept -> dedekind::category::Ternary {
          return b ? dedekind::category::Ternary::True
                   : dedekind::category::Ternary::False;
        })

Canonical embedding 𝔹 ↪ 𝕂3: bool → Ternary.

The two-valued-to-three-valued Kleene lift: false ↦ Ternary::False (-1), true ↦ Ternary::True (1). The Ternary::Unknown (0) value is not in the image — it represents the third truth-value that 𝔹 lacks. This is the canonical inclusion of two-valued classical logic into three- valued Kleene logic; structurally a monomorphism.

Namespaces

Functions

Variables