{-# OPTIONS --cubical --exact-split #-}
module OnLengthOrder where
open import Agda.Primitive
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Everything
open import Cubical.Data.Nat.Order -- using (_<_ ; _≤_ ; zero-≤)
open import Cubical.Induction.WellFounded
open import Cubical.HITs.FiniteMultiset
open import FMSetUniv
open import Cubical.Data.Sum.Base

import Cubical.Data.Empty as ⊥

private
  variable
    ℓ : Level
    A : Type ℓ

private
  variable
    a b c d e : Level
    B : Set b
    C : Set c
    D : Set d
    E : Set e

infixl  _on_

_on_ : (B → B → C) → (D → B) → (D → D → C)
_*_ on f = \x y -> f x * f y

module _ (f : B → D) where
  accessible : ∀ {∼ : Rel D ℓ} {x} → Acc ∼ (f x) → Acc (∼ on f) x
  accessible (acc rs) = acc (λ y fy<fx → accessible (rs (f y) fy<fx))

  wellFounded : {∼ : Rel D ℓ} → WellFounded ∼ → WellFounded (∼ on f)
  wellFounded wf x = accessible (wf (f x))


module _ {A : Type ℓ} where
  open Length {A = A}
  _<l_ : FMSet A → FMSet A → Type
  _<l_ = _<_ on length

  <l-wellfounded : WellFounded _<l_
  <l-wellfounded = wellFounded length <-wellfounded