dedekind::category::detail_natural::IsNaturalSquare Concept Reference

The naturality square at an arrow f, \(\alpha \circ F(f) = G(f) \circ \alpha\), for a component Ac of one type at every object (the single-species categories), decided by the arrow algebra and never by comparing the two composites' types, which differ for any component but an identity although the arrows they denote agree: More...

Concept definition

template<typename Α, typename F, typename G, typename Ff, typename Gf, typename Ac>
concept dedekind::category::detail_natural::IsNaturalSquare = 
    (std::same_as<F, G> && has_one_value_v<F> &&
     (IsIdentityArrow<Ac> ||
      (IsConstantFamily<Α> &&
       std::same_as<Ac, decltype(std::declval<const Α&>().component())> &&
       commutes_v<Ff, Ac>))) ||
    (IsIdentityArrow<Ac> && std::same_as<Ff, Gf> && has_one_value_v<Ff>)

Detailed Description

The naturality square at an arrow f, \(\alpha \circ F(f) = G(f) \circ \alpha\), for a component Ac of one type at every object (the single-species categories), decided by the arrow algebra and never by comparing the two composites' types, which differ for any component but an identity although the arrows they denote agree:

• one functor, of a type with one value (has_one_value), so that its two ends are one functor, and an identity component: the unit law;
• that one functor and one component at every object (IsConstantFamily), certified to commute with \(F(f)\) (commutes, :morphism): the square is that certificate;
• two functors and an identity component: the square is \(F(f) = G(f)\), which holds where both lift f to one arrow of a type with one value (has_one_value). Any other family is refused, natural or not: what is not certified is not claimed.

  Template Parameters

  Α	the family.
  F
  G	the functors.
  Ff
  Gf	their lifts of f.
  Ac	the component.