{-# OPTIONS --cubical --exact-split #-}

module Cubical.Structures.Set.CMon.SList.Count where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as 
open import Cubical.Induction.WellFounded
import Cubical.Data.List as L
open import Cubical.Functions.Logic as L
open import Cubical.HITs.PropositionalTruncation as P
open import Cubical.Data.Sum as 
open import Cubical.Relation.Nullary

open import Cubical.Structures.Prelude
import Cubical.Structures.Set.Mon.Desc as M
import Cubical.Structures.Set.CMon.Desc as M
import Cubical.Structures.Free as F
open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq
open import Cubical.Structures.Arity
open import Cubical.Structures.Set.Mon.List

open import Cubical.Structures.Set.CMon.SList.Base as SList

private
  variable
     : Level
    A : Type 

module Count* {} {A : Type } (discA : Discrete A) where
  open SList.Free {A = A} isSetℕ M.ℕ-CMonStr-MonSEq

   : A -> A -> 
   x = λ y -> decElim  x≡y -> 1)  x≠y -> 0) (discA x y)

  よ-β :  x ->  x x  1
  よ-β x  with discA x x
  ... | yes p = refl
  ... | no ¬p = ⊥.rec (¬p refl)

  ∈*ℕ : A -> SList A -> 
  ∈*ℕ x = ( x) 

  _∈*_ : A -> SList A -> 
  _∈*_ x = ( x) 

  x∈*[] :  x -> x ∈* []  0
  x∈*[] x = refl

  x∈*x∷xs :  x xs -> x ∈* (x  xs)  1 + x ∈* xs
  x∈*x∷xs x xs = ♯-∷ ( x) x xs  congS (_+ (x ∈* xs)) (よ-β x)