dedekind::category::IsCounitOfAdjunction Concept Reference

Structural shape: ε is the counit of an adjunction F ⊣ U — a natural transformation F ∘ U ⇒ id_𝒞. Dual of IsUnitOfAdjunction. More...

Concept definition

template<typename Epsilon, typename F, typename U>
concept dedekind::category::IsCounitOfAdjunction = 
    HasAdjunctionShape<F, U> &&
    IsNaturalTransformation<Epsilon, composite_functor<U, F>,
                            identity_functor<typename F::Τ_cat>>

Detailed Description

Structural shape: ε is the counit of an adjunction F ⊣ U — a natural transformation F ∘ U ⇒ id_𝒞. Dual of IsUnitOfAdjunction.