dedekind::relational::Dual< F, L > Struct Template Reference

\(\forall_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the dual image: \(a \mapsto \{y \mid \forall x.\ f(x) = y \Rightarrow x \in a\}\), which is \(\neg\,\exists_f\,\neg\) (De Morgan: the logic is an Ockham algebra), a composite of three arrows on presented objects. The right adjoint of Preimage; monotone, as anti∘co∘anti. More...

Public Types
using	Domain = dedekind::sets::Subobjects<dedekind::category::Dom<F>, L>
using	Codomain = dedekind::sets::Subobjects<dedekind::category::Cod<F>, L>
using	Composite

Public Member Functions
template<typename S> requires dedekind::category::Presents<S, Domain> && requires(const S& s) { Composite{}(s); }
constexpr auto	operator() (const S &s) const

Detailed Description

template<dedekind::category::IsArrow F, dedekind::category::IsOckhamAlgebra L>
requires std::default_initializable<F>
struct dedekind::relational::Dual< F, L >

\(\forall_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the dual image: \(a \mapsto \{y \mid \forall x.\ f(x) = y \Rightarrow x \in a\}\), which is \(\neg\,\exists_f\,\neg\) (De Morgan: the logic is an Ockham algebra), a composite of three arrows on presented objects. The right adjoint of Preimage; monotone, as anti∘co∘anti.

Template Parameters

F	the arrow, stateless.
L	the logic.

Member Typedef Documentation

Composite

template<dedekind::category::IsArrow F, dedekind::category::IsOckhamAlgebra L>

using dedekind::relational::Dual< F, L >::Composite

Initial value:

 dedekind::category::Compose<
      dedekind::category::Compose<
          dedekind::sets::Complement<dedekind::category::Dom<F>, L>,
          Image<F, L>>,
      dedekind::sets::Complement<dedekind::category::Cod<F>, L>>

---

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

• src/main/modules/dedekind/relational/graph.cppm