Source code on Github
{-# OPTIONS --cubical-compatible #-}
module Class.Pointed.Instances where

open import Class.Prelude
open import Class.Pointed.Core
open import Class.Applicative.Instances

instance
  P-Maybe = Applicative⇒Pointed {F = Maybe}
  P-List  = Applicative⇒Pointed {F = List}
  P-List⁺ = Applicative⇒Pointed {F = List⁺}
  P-TC    = Applicative⇒Pointed {F = TC}
  P-Vec   = λ {n}  Applicative⇒Pointed {F = flip Vec n}