------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous `All` predicate for disjoint sums
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Sum.Relation.Unary.All where

open import Data.Sum.Base  using (_⊎_; inj₁; inj₂)
open import Level          using (Level; _⊔_)
open import Relation.Unary using (Pred)

private
  variable
    a b c p q : Level
    A B : Set _
    P Q : Pred A p

------------------------------------------------------------------------
-- Definition

data All {A : Set a} {B : Set b} (P : Pred A p) (Q : Pred B q)
         : Pred (A ⊎ B) (a ⊔ b ⊔ p ⊔ q) where
  inj₁ : ∀ {a} → P a → All P Q (inj₁ a)
  inj₂ : ∀ {b} → Q b → All P Q (inj₂ b)

------------------------------------------------------------------------
-- Operations

-- Elimination

[_,_] : ∀ {C : (x : A ⊎ B) → All P Q x → Set c} →
        ((x : A) (y : P x) → C (inj₁ x) (inj₁ y)) →
        ((x : B) (y : Q x) → C (inj₂ x) (inj₂ y)) →
        (x : A ⊎ B) (y : All P Q x) → C x y
[ f , g ] (inj₁ x) (inj₁ y) = f x y
[ f , g ] (inj₂ x) (inj₂ y) = g x y