Constructions.Coproduct

module Constructions.Coproduct
  (C : Set1)(HomC : C -> C -> Set)
  (idC : (c : C) -> HomC c c)
  (_∘C_ : {a b c : C} -> HomC b c -> HomC a b -> HomC a c)
  where

open import Data.Bool

import posIR
open posIR C HomC idC _∘C_

infixl 3 _+IR_

_+IR_ : IR+ -> IR+ -> IR+
a +IR b = σ Bool (λ { true → a ; false → b })