The injection ι_K : A → A + B as an arrow: monic (it is injective, and its image is disjoint from the other summand's), the ground of a sum's strength reduction (a set inside one injection's image pulls back along it without loss). More...

Public Types
using	Domain = std::conditional_t<K == 1, A, B>
using	Codomain = std::variant<A, B>
using	is_monic_arrow_tag = void

Public Member Functions
constexpr Codomain	operator() (const Domain &x) const

Detailed Description

template<std::size_t K, typename A, typename B>
requires (K == 1 || K == 2)
struct dedekind::relational::detail_hyperdoctrine_witness::Injection< K, A, B >

The injection ι_K : A → A + B as an arrow: monic (it is injective, and its image is disjoint from the other summand's), the ground of a sum's strength reduction (a set inside one injection's image pulls back along it without loss).

Template Parameters

K	the summand, 1 or 2.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/cartesian.cppm

Public Types

Public Member Functions

Detailed Description