module Ornament.List where

open import Stdlib
open import Ornament
open import Signature
open import Signature.Nat

τList : Set  COrn ΣNat  id
τList A = record { extend = extendList 
                 ; refine = refineList 
                 ; coh = cohList }
      where open Sig ΣNat

            extendList : (tt : )  Op tt  Set
            extendList tt (inj₁ tt) = 
            extendList tt (inj₂ tt) = A

            refineList : (tt : )(op : Op tt)  extendList tt op  Ar op  
            refineList _ _ _ _ = tt

            cohList : (tt : )(op : Op tt)(ext : extendList tt op)
                (ar : Ar op)  tt  Ty ar
            cohList tt op ext arr = refl