    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of operations on containers
    ------------------------------------------------------------------------

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

    module Data.Container.Properties where

    open import Data.Container.Core using (Container; map)
    open import Data.Container.Relation.Binary.Equality.Setoid using (Eq; refl)
    import Function.Base as F using (id; _∘′_)
    open import Relation.Binary.Bundles using (Setoid)

    module _ {s p} {C : Container s p} where

      map-identity : ∀ {x e} (X : Setoid x e) xs →
                     Eq X C (map F.id xs) xs
      map-identity X xs = refl X C

      map-compose : ∀ {x y z e} {X : Set x} {Y : Set y} (Z : Setoid z e) g (f : X → Y) xs →
                    Eq Z C (map g (map f xs)) (map (g F.∘′ f) xs)
      map-compose Z g f xs = refl Z C