-- 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
open import Codata.Sized.Thunk using (Thunk; force)
open import Codata.Sized.Conat
open import Codata.Sized.Covec
open import Codata.Sized.Covec.Bisimilarity
open import Function.Base using (id; _∘_)
open import Relation.Binary.PropositionalEquality as Eq

-- 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) = Eq.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) = Eq.refl  λ where .force  map-∘ f g (as .force)

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