    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of operations on M-types
    ------------------------------------------------------------------------

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

    module Codata.Sized.M.Properties where

    open import Level using (_⊔_)
    open import Size using (Size; ∞)
    open import Codata.Sized.Thunk using (Thunk; force)
    open import Codata.Sized.M using (M; inf; map; unfold)
    open import Codata.Sized.M.Bisimilarity using (Bisim; inf)
    open import Data.Container.Core as C hiding (map)
    import Data.Container.Morphism as Mp using (id; _∘_)
    open import Data.Product.Base as Product using (_,_)
    open import Data.Product.Properties hiding (map-cong)
    open import Function.Base using (_$′_; _∘′_)
    import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; subst)
    import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
    open import Data.Container.Relation.Binary.Pointwise using (_,_)
    import Data.Container.Relation.Binary.Equality.Setoid as EqSetoid

    private module Eq {a} (A : Set a) = EqSetoid (≡.setoid A)
    open Eq using (Eq)

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

      map-id : ∀ {i} c → Bisim C i (map (Mp.id C) c) c
      map-id (inf (s , f)) = inf (≡.refl , λ where p .force → map-id (f p .force))

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

      map-cong : ∀ {i} {f g : C₁ ⇒ C₂} →
                 (∀ {X} t → Eq X C₂ (⟪ f ⟫ t) (⟪ g ⟫ t)) →
                 ∀ c₁ → Bisim C₂ i (map f c₁) (map g c₁)
      map-cong {f = f} {g} f≗g (inf t@(s , n)) with f≗g t
      ... | eqs , eqf = inf (eqs , λ where
         p .force {j} → ≡.subst (λ t → Bisim C₂ j (map f (n (position f p) .force))
                                                  (map g (t .force)))
                        (eqf p)
                        (map-cong f≗g (n (position f p) .force)))

    module _ {s₁ s₂ s₃ p₁ p₂ p₃} {C₁ : Container s₁ p₁}
             {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃} where

      map-∘ : ∀ {i} {g : C₂ ⇒ C₃} {f : C₁ ⇒ C₂} c₁ →
                    Bisim C₃ i (map (g Mp.∘ f) c₁) (map g $′ map f c₁)
      map-∘ (inf (s , f)) = inf (≡.refl , λ where p .force → map-∘ (f _ .force))

    module _ {s₁ s₂ p₁ p₂ s} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
             {S : Set s} {alg : S → ⟦ C₁ ⟧ S} {f : C₁ ⇒ C₂} where

      map-unfold : ∀ {i} s → Bisim C₂ i (map f (unfold alg s))
                                        (unfold (⟪ f ⟫ ∘′ alg) s)
      map-unfold s = inf (≡.refl , λ where p .force → map-unfold _)

    ------------------------------------------------------------------------
    -- 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."
    #-}