    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of operations on the Covec type
    ------------------------------------------------------------------------

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

    module Codata.Sized.Covec.Properties where

    open import Size using (Size; ∞)
    open import Codata.Sized.Thunk using (Thunk; force)
    open import Codata.Sized.Conat using (zero; suc)
    open import Codata.Sized.Covec using (Covec; _∷_; []; map)
    open import Codata.Sized.Covec.Bisimilarity
    open import Function.Base using (id; _∘_)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

    -- Functor laws

    module _ {a} {A : Set a} where

     map-id : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as
     map-id []       = []
     map-id (a ∷ as) = ≡.refl ∷ λ where .force → map-id (as .force)

    module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

     map-∘ : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as
     map-∘ f g []       = []
     map-∘ f g (a ∷ as) = ≡.refl ∷ λ where .force → map-∘ f g (as .force)

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

    -- Version 2.0

    map-identity = map-id
    {-# WARNING_ON_USAGE map-identity
    "Warning: map-identity was deprecated in v2.0.
    Please use map-id instead."
    #-}

    map-map-fusion = map-∘
    {-# WARNING_ON_USAGE map-map-fusion
    "Warning: map-map-fusion was deprecated in v2.0.
    Please use map-∘ instead."
    #-}