    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Pointwise lifting of a predicate to a binary tree
    ------------------------------------------------------------------------

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

    module Data.Tree.Binary.Relation.Unary.All where

    open import Level
    open import Data.Tree.Binary as Tree using (Tree; leaf; node)
    open import Relation.Unary
    open import Relation.Unary.Properties using (⊆-refl)

    private
      variable
        n l p q r s : Level
        N : Set n
        L : Set l
        P : N → Set p
        Q : L → Set q
        R : N → Set r
        S : L → Set s

    data All {N : Set n} {L : Set l} (P : N → Set p) (Q : L → Set q) : Tree N L → Set (n ⊔ l ⊔ p ⊔ q) where
      leaf : ∀ {x} → Q x → All P Q (leaf x)
      node : ∀ {l m r} → All P Q l → P m → All P Q r → All P Q (node l m r)

    map : ∀[ P ⇒ R ] → ∀[ Q ⇒ S ] → ∀[ All P Q ⇒ All R S ]
    map f g (leaf x)     = leaf (g x)
    map f g (node l m r) = node (map f g l) (f m) (map f g r)

    mapₙ : ∀[ P ⇒ R ] → ∀[ All P Q ⇒ All R Q ]
    mapₙ {Q = Q} f = map f (⊆-refl {x = Q})

    mapₗ : ∀[ Q ⇒ S ] → ∀[ All P Q ⇒ All P S ]
    mapₗ {P = P} f = map (⊆-refl {x = P}) f