Operations

\import Data.Or

\class HasProduct (E : \Type)
  | Product \alias \infixl 7 ⨯ : E -> E -> E

\instance TypeHasProduct.{u} : HasProduct (\Type u)
  | Product A B => \Sigma A B

\instance SetHasProduct.{u} : HasProduct (\Set u)
  | Product A B => \Sigma A B

\class HasCoproduct (E : \Type)
  | Coproduct \alias \infixl 6 ⨿ : E -> E -> E

\instance TypeHasCoproduct.{u} : HasCoproduct (\Type u)
  | Coproduct A B => Or A B

\instance SetHasCoproduct.{u} : HasCoproduct (\Set u)
  | Coproduct A B => Or A B