```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of rose trees
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --sized-types #-}

module Data.Tree.Rose.Properties where

open import Level using (Level)
open import Size
open import Data.List.Base as List using (List)
open import Data.List.Extrema.Nat
import Data.List.Properties as Listₚ
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Tree.Rose
open import Function.Base
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
i : Size

------------------------------------------------------------------------
-- map properties

map-∘ : (f : A → B) (g : B → C) →
map {i = i} (g ∘′ f) ≗ map {i = i} g ∘′ map {i = i} f
map-∘ f g (node a ts) = cong (node (g (f a))) \$ begin
List.map (map (g ∘′ f)) ts             ≡⟨ Listₚ.map-cong (map-∘ f g) ts ⟩
List.map (map g ∘ map f) ts            ≡⟨ Listₚ.map-∘ ts ⟩
List.map (map g) (List.map (map f) ts) ∎

depth-map : (f : A → B) (t : Rose A i) → depth {i = i} (map {i = i} f t) ≡ depth {i = i} t
depth-map f (node a ts) = cong (suc ∘′ max 0) \$ begin
List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩
List.map (depth ∘′ map f) ts         ≡⟨ Listₚ.map-cong (depth-map f) ts ⟩
List.map depth ts ∎

------------------------------------------------------------------------
-- foldr properties

foldr-map : (f : A → B) (n : B → List C → C) (ts : Rose A i) →
foldr {i = i} n (map {i = i} f ts) ≡ foldr {i = i} (n ∘′ f) ts
foldr-map f n (node a ts) = cong (n (f a)) \$ begin
List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩
List.map (foldr n ∘′ map f) ts           ≡⟨ Listₚ.map-cong (foldr-map f n) ts ⟩
List.map (foldr (n ∘′ f)) ts             ∎

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

map-compose = map-∘
{-# WARNING_ON_USAGE map-compose
"Warning: map-compose was deprecated in v2.0.