DepthComonads.List

{-# OPTIONS --safe #-}

module DepthComonads.List where

open import Agda.Builtin.List public
open import DepthComonads.Level

infixr 4 _,_
data ListSyntax (A : Type a) : Type a where
  singleton : A → ListSyntax A
  _,_ : A → ListSyntax A → ListSyntax A

infixl 6 _]
_] : A → ListSyntax A
_] = singleton

infixr 4 [_
[_ : ListSyntax A → List A
[ singleton x = x ∷ []
[ x , xs = x ∷ ([ xs)