------------------------------------------------------------------------
-- The Agda standard library
--
-- Container Morphisms
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Container.Morphism where
 
open import Data.Container.Core using (Container; ⟦_⟧; _⇒_; shape; position)
import Function.Base as F using (id; _∘′_)
 
module _ {s p} (C : Container s p) where
 
  id : C ⇒ C
  id .shape    = F.id
  id .position = F.id
 
module _ {s₁ s₂ s₃ p₁ p₂ p₃}
         {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃}
         where
 
  infixr  _∘_
  _∘_ : C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
  (f ∘ g) .shape    = shape    f F.∘′ shape    g
  (f ∘ g) .position = position g F.∘′ position f