premonoidal category Type Theory for unbiased monoidal categories References Higher Operads, Higher Categories (Leinster) note
