{-# 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 9 _∘_
_∘_ : C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
(f ∘ g) .shape = shape f F.∘′ shape g
(f ∘ g) .position = position g F.∘′ position f