{-# OPTIONS --cubical-compatible #-} module Class.Traversable.Instances where open import Class.Prelude open import Class.Functor open import Class.Applicative open import Class.Monad open import Class.Traversable.Core instance TraversableA-Maybe : TraversableA Maybe TraversableA-Maybe .sequenceA = λ where nothing → ⦇ nothing ⦈ (just x) → ⦇ just x ⦈ TraversableM-Maybe : Traversable Maybe TraversableM-Maybe .sequence = sequenceA TraversableA-List : TraversableA List TraversableA-List .sequenceA = go where go = λ where [] → ⦇ [] ⦈ (m ∷ ms) → ⦇ m ∷ go ms ⦈ TraversableM-List : Traversable List TraversableM-List .sequence = sequenceA TraversableA-List⁺ : TraversableA List⁺ TraversableA-List⁺ .sequenceA (m ∷ ms) = ⦇ m ∷ sequenceA ms ⦈ TraversableM-List⁺ : Traversable List⁺ TraversableM-List⁺ .sequence = sequenceA