------------------------------------------------------------------------
-- 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