module Ornament.Fin where

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

τFin : COrn ΣNat   n  tt)
τFin = record { extend = extendFin 
              ; refine = refineFin
              ; coh = cohFin }
      where open Sig ΣNat

            extendFin : (n : )  Op tt  Set
            extendFin n _ =  λ n'  n  suc n'

            refineFin : (n : )(op : Op tt)  extendFin n op  Ar op  
            refineFin .(suc n) (inj₁ tt) (n , refl) ()
            refineFin .(suc n) (inj₂ tt) (n , refl) tt = n

            cohFin : (n : )(op : Op tt)(ext : extendFin n op)(ar : Ar op)  
                tt  Ty ar
            cohFin n op ext arr = refl