Function day_convolution_ty 

pub fn day_convolution_ty() -> Expr

DayConvolution : (Type → Type) → (Type → Type) → Type → Type

Day convolution of two functors: (Day F G) A = ∃ X Y, F X × G Y × (X × Y → A).