------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the pointwise lifting of a predicate to a binary tree
------------------------------------------------------------------------

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

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

open import Level
open import Data.Tree.Binary as Tree using (Tree; leaf; node)
open import Data.Tree.Binary.Relation.Unary.All
open import Relation.Unary
open import Function.Base using (id)

private
  variable
    n l n₁ l₁ p q : Level
    N : Set n
    L : Set l
    N₁ : Set n₁
    L₁ : Set l₁
    P : N₁ → Set p
    Q : L₁ → Set q

map⁺ : (f : N → N₁) → (g : L → L₁) → All (f ⊢ P) (g ⊢ Q) ⊆ Tree.map f g ⊢ All P Q
map⁺ f g (leaf x)     = leaf x
map⁺ f g (node l m r) = node (map⁺ f g l) m (map⁺ f g r)

mapₙ⁺ : (f : N → N₁) → All (f ⊢ P) Q ⊆ Tree.mapₙ f ⊢ All P Q
mapₙ⁺ f = map⁺ f id

mapₗ⁺ : (g : L → L₁) → All P (g ⊢ Q) ⊆ Tree.mapₗ g ⊢ All P Q
mapₗ⁺ g = map⁺ id g