------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4