    ------------------------------------------------------------------------
    -- 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 using (max)
    import Data.List.Properties as List
    open import Data.Nat.Base using (ℕ; zero; suc)
    open import Data.Tree.Rose using (Rose; node; map; depth; foldr)
    open import Function.Base using (_∘′_; _$_; _∘_)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; _≗_; cong)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)
    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.
    Please use map-∘ instead."
    #-}