------------------------------------------------------------------------
-- Sums of binary relations
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Relation.Binary.Sum where

open import Data.Sum as Sum
open import Data.Product
open import Data.Unit using ()
open import Data.Empty
open import Function
open import Function.Equality as F using (_⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalent; _⇔_; module Equivalent)
  renaming (_∘_ to _⟨∘⟩_)
open import Function.Inverse as Inv
  using (Inverse; _⇿_; module Inverse)
  renaming (_∘_ to _⟪∘⟫_)
open import Level
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

private
 module Dummy {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} where

  ----------------------------------------------------------------------
  -- Sums of relations

  infixr 1 _⊎-Rel_ _⊎-<_

  -- Generalised sum.

  data ⊎ʳ {ℓ₁ ℓ₂} (P : Set) (_∼₁_ : Rel A₁ ℓ₁) (_∼₂_ : Rel A₂ ℓ₂) :
          A₁  A₂  A₁  A₂  Set (a₁  a₂  ℓ₁  ℓ₂) where
    ₁∼₂ :  {x y} (