    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Lifting of two predicates
    ------------------------------------------------------------------------

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

    module Data.Product.Relation.Unary.All where

    open import Level using (Level; _⊔_)
    open import Data.Product.Base using (_×_; _,_)

    private
      variable
        a b p q : Level
        A : Set a
        B : Set b

    All : (A → Set p) → (B → Set q) → (A × B → Set (p ⊔ q))
    All P Q (a , b) = P a × Q b