dedekind::category::DaggerFunctor< Dagger, T, Op > Struct Template Reference

A dagger as a functor: from the delooping of (T, Op) to that of its opposite, each element to its dagger. The functor laws are the dagger's, \((a b)^\dagger = b^\dagger a^\dagger\), the composition law into the opposite category, and \(1^\dagger = 1\), which an involutive anti-homomorphism keeps; so they are derived from IsDagger and not declared again. Contravariant on the one object, and its own inverse. More...

Collaboration diagram for dedekind::category::DaggerFunctor< Dagger, T, Op >:

Public Types
using	Σ_cat = Delooping<T, Op>
using	Τ_cat = Delooping<T, Opposite<Op>>
using	Domain = Σ_cat
using	Codomain = Τ_cat
template<typename U>
using	Shape = One

Public Member Functions
constexpr Codomain	operator() (const Domain &) const
constexpr Element< T, Opposite< Op > >	operator() (const Element< T, Op > &a) const
constexpr IdentityIn< Τ_cat >	operator() (const IdentityIn< Σ_cat > &) const

Public Attributes
Dagger	dagger {}

Detailed Description

template<std::semiregular Dagger, std::semiregular T, std::semiregular Op>
requires IsMonoid<T, Op> && IsMonoid<T, Opposite<Op>> && IsDagger<Dagger, T, Op>
struct dedekind::category::DaggerFunctor< Dagger, T, Op >

A dagger as a functor: from the delooping of (T, Op) to that of its opposite, each element to its dagger. The functor laws are the dagger's, \((a b)^\dagger = b^\dagger a^\dagger\), the composition law into the opposite category, and \(1^\dagger = 1\), which an involutive anti-homomorphism keeps; so they are derived from IsDagger and not declared again. Contravariant on the one object, and its own inverse.

Template Parameters

Dagger	the dagger.
T	the arrows.
Op	their composition.

---

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

• src/main/modules/dedekind/category/functor.cppm