This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Repetitions of values in sequences

module univalent-combinatorics.repetitions-of-values-sequences where
Imports 




Properties


is-decidable-is-ordered-repetition-of-values-ℕ-Fin :
  (k : ℕ) (f : ℕ → Fin k) (x : ℕ) →
  is-decidable (is-ordered-repetition-of-values-ℕ f x)
is-decidable-is-ordered-repetition-of-values-ℕ-Fin k f x = {!!}

{-
  is-decidable-strictly-bounded-Σ-ℕ' x
    ( λ y → Id (f y) (f x))
    ( λ y → has-decidable-equality-Fin k (f y) (f x))
-}

is-decidable-is-ordered-repetition-of-values-ℕ-count :
  {l : Level} {A : UU l} (e : count A) (f : ℕ → A) (x : ℕ) →
  is-decidable (is-ordered-repetition-of-values-ℕ f x)
is-decidable-is-ordered-repetition-of-values-ℕ-count e f x = {!!}

{-
  is-decidable-strictly-bounded-Σ-ℕ' x
    ( λ y → Id (f y) (f x))
    ( λ y → has-decidable-equality-count e (f y) (f x))
  -}