bijection-fin.agda

module bijection-fin where

  open import Type

  open import bijection
  open import Function.NP hiding (Cmp)
  open import Relation.Binary.PropositionalEquality

  open import Data.Empty
  open import Data.Nat.NP
  open import Data.Fin using (Fin ; zero ; suc ; fromℕ ; inject₁)
  open import Data.Vec hiding ([_])

  data `Syn : ℕ → ★ where
    `id   : ∀ {n} → `Syn n
    `swap : ∀ {n} → `Syn (2 + n)
    `tail : ∀ {n} → `Syn n → `Syn (1 + n)
    _`∘_  : ∀ {n} → `Syn n → `Syn n → `Syn n

  `Rep = Fin

  `Ix = ℕ

  `Tree : ★ → `Ix → ★
  `Tree X = Vec X

  `fromFun : ∀ {i X} → (`Rep i → X) → `Tree X i
  `fromFun = tabulate

  `toFun : ∀ {i X} → `Tree X i → (`Rep i → X)
  `toFun T zero    = head T
  `toFun T (suc i) = `toFun (tail T) i

  `toFun∘fromFun : ∀ {i X}(f : `Rep i → X) → f ≗ `toFun (`fromFun f)
  `toFun∘fromFun f zero = refl
  `toFun∘fromFun f (suc i) = `toFun∘fromFun (f ∘ suc) i

  fin-swap : ∀ {n} → Endo (Fin (2 + n))
  fin-swap zero = suc zero
  fin-swap (suc zero) = zero
  fin-swap (suc (suc i)) = suc (suc i)

  fin-tail : ∀ {n} → Endo (Fin n) → Endo (Fin (1 + n))
  fin-tail f zero = zero
  fin-tail f (suc i) = suc (f i)

  `evalArg : ∀ {i} → `Syn i → Endo (`Rep i)
  `evalArg `id       = id
  `evalArg `swap     = fin-swap
  `evalArg (`tail f) = fin-tail (`evalArg f)
  `evalArg (S `∘ S₁) = `evalArg S ∘ `evalArg S₁

  vec-swap : ∀ {n}{X : ★} → Endo (Vec X (2 + n))
  vec-swap xs = head (tail xs) ∷ head xs ∷ tail (tail xs)

  vec-tail : ∀ {n}{X : ★} → Endo (Vec X n) → Endo (Vec X (1 + n))
  vec-tail f xs = head xs ∷ f (tail xs)

  `evalTree : ∀ {i X} → `Syn i → Endo (`Tree X i)
  `evalTree `id       = id
  `evalTree `swap     = vec-swap
  `evalTree (`tail f) = vec-tail (`evalTree f)
  `evalTree (S `∘ S₁) = `evalTree S ∘ `evalTree S₁

  `eval-proof : ∀ {i X} S (T : `Tree X i) → `toFun T ≗ `toFun (`evalTree S T) ∘ `evalArg S
  `eval-proof `id       T i = refl
  `eval-proof `swap T zero = refl
  `eval-proof `swap T (suc zero) = refl
  `eval-proof `swap T (suc (suc i)) = refl
  `eval-proof (`tail S) T zero = refl
  `eval-proof (`tail S) T (suc i) = `eval-proof S (tail T) i
  `eval-proof (S `∘ S₁) T i rewrite
    `eval-proof S₁ T i |
    `eval-proof S (`evalTree S₁ T) (`evalArg S₁ i) = refl

  `inv : ∀ {i} → Endo (`Syn i)
  `inv `id       = `id
  `inv `swap     = `swap
  `inv (`tail S) = `tail (`inv S)
  `inv (S `∘ S₁) = `inv S₁ `∘ `inv S

  `inv-proof : ∀ {i} → (S : `Syn i) → `evalArg S ∘ `evalArg (`inv S) ≗ id
  `inv-proof `id x       = refl
  `inv-proof `swap zero          = refl
  `inv-proof `swap (suc zero)    = refl
  `inv-proof `swap (suc (suc x)) = refl
  `inv-proof (`tail S) zero = refl
  `inv-proof (`tail S) (suc x) rewrite `inv-proof S x = refl
  `inv-proof (S `∘ S₁) x rewrite 
    `inv-proof S₁ (`evalArg (`inv S) x) |
    `inv-proof S x = refl

  `RC : ∀ {i} → Cmp (`Rep i)
  `RC zero zero = eq
  `RC zero (suc j) = lt
  `RC (suc i) zero = gt
  `RC (suc i) (suc j) = `RC i j

  insert : ∀ {n X} → Cmp X → X → Vec X n → Vec X (1 + n)
  insert X-cmp x [] = x ∷ []
  insert X-cmp x (x₁ ∷ xs) with X-cmp x x₁
  insert X-cmp x (x₁ ∷ xs) | lt = x ∷ x₁ ∷ xs
  insert X-cmp x (x₁ ∷ xs) | eq = x ∷ x₁ ∷ xs
  insert X-cmp x (x₁ ∷ xs) | gt = x₁ ∷ insert X-cmp x xs

  `sort : ∀ {i X} → Cmp X → Endo (`Tree X i)
  `sort X-cmp [] = []
  `sort X-cmp (x ∷ xs) = insert X-cmp x (`sort X-cmp xs)

  insert-syn : ∀ {n X} → Cmp X → X → Vec X n → `Syn (1 + n)
  insert-syn X-cmp x [] = `id
  insert-syn X-cmp x (x₁ ∷ xs) with X-cmp x x₁
  insert-syn X-cmp x (x₁ ∷ xs) | lt = `id
  insert-syn X-cmp x (x₁ ∷ xs) | eq = `id
  insert-syn X-cmp x (x₁ ∷ xs) | gt = `tail (insert-syn X-cmp x xs) `∘ `swap

  `sort-syn : ∀ {i X} → Cmp X → `Tree X i → `Syn i
  `sort-syn X-cmp []       = `id
  `sort-syn X-cmp (x ∷ xs) = insert-syn X-cmp x (`sort X-cmp xs) `∘ `tail (`sort-syn X-cmp xs)

  insert-proof : ∀ {n X}(X-cmp : Cmp X) x (T : Vec X n) → insert X-cmp x T ≡ `evalTree (insert-syn X-cmp x T) (x ∷ T)
  insert-proof X-cmp x [] = refl
  insert-proof X-cmp x (x₁ ∷ T) with X-cmp x x₁
  insert-proof X-cmp x (x₁ ∷ T) | lt = refl
  insert-proof X-cmp x (x₁ ∷ T) | eq = refl
  insert-proof X-cmp x (x₁ ∷ T) | gt rewrite insert-proof X-cmp x T = refl

  `sort-proof : ∀ {i X}(X-cmp : Cmp X)(T : `Tree X i) → `sort X-cmp T ≡ `evalTree (`sort-syn X-cmp T) T
  `sort-proof X-cmp [] = refl
  `sort-proof X-cmp (x ∷ T) rewrite 
    sym (`sort-proof X-cmp T)= insert-proof X-cmp x (`sort X-cmp T)

  module Alt-Syn where

    data ``Syn : ℕ → ★ where
      `id : ∀ {n} → ``Syn n
      _`∘_ : ∀ {n} → ``Syn n → ``Syn n → ``Syn n
      `swap : ∀ {n} m → ``Syn (m + 2 + n)

    swap-fin : ∀ {n} m → Endo (Fin (m + 2 + n))
    swap-fin zero zero = suc zero
    swap-fin zero (suc zero) = zero
    swap-fin zero (suc (suc i)) = suc (suc i)
    swap-fin (suc m) zero = zero
    swap-fin (suc m) (suc i) = suc (swap-fin m i)

    ``evalArg : ∀ {n} → ``Syn n → Endo (`Rep n)
    ``evalArg `id       = id
    ``evalArg (S `∘ S₁) = ``evalArg S ∘ ``evalArg S₁
    ``evalArg (`swap m) = swap-fin m

    _``∘_ : ∀ {n} → ``Syn n → ``Syn n → ``Syn n
    `id ``∘ y = y
    (x `∘ x₁) ``∘ `id = x `∘ x₁
    (x `∘ x₁) ``∘ (y `∘ y₁) = x `∘ (x₁ `∘ (y `∘ y₁))
    (x `∘ x₁) ``∘ `swap m = x `∘ (x₁ ``∘ `swap m)
    `swap m ``∘ y = `swap m `∘ y

    ``tail : ∀ {n} → ``Syn n → ``Syn (suc n)
    ``tail `id = `id
    ``tail (S `∘ S₁) = ``tail S ``∘ ``tail S₁
    ``tail (`swap m) = `swap (suc m)

    translate : ∀ {n} → `Syn n → ``Syn n
    translate `id = `id
    translate `swap = `swap 0
    translate (`tail S) = ``tail (translate S)
    translate (S `∘ S₁) = translate S ``∘ translate S₁

    ``∘-p : ∀ {n}(A B : ``Syn n) → ``evalArg (A ``∘ B) ≗ ``evalArg (A `∘ B)
    ``∘-p `id B x = refl
    ``∘-p (A `∘ A₁) `id x = refl
    ``∘-p (A `∘ A₁) (B `∘ B₁) x = refl
    ``∘-p (A `∘ A₁) (`swap m) x rewrite ``∘-p A₁ (`swap m) x = refl
    ``∘-p (`swap m) B x = refl

    ``tail-p : ∀ {n} (S : ``Syn n) → fin-tail (``evalArg S) ≗ ``evalArg (``tail S)
    ``tail-p `id zero = refl
    ``tail-p `id (suc x) = refl
    ``tail-p (S `∘ S₁) zero rewrite ``∘-p (``tail S) (``tail S₁) zero
                                  | sym (``tail-p S₁ zero) = ``tail-p S zero
    ``tail-p (S `∘ S₁) (suc x) rewrite ``∘-p (``tail S) (``tail S₁) (suc x)
                                     | sym (``tail-p S₁ (suc x)) = ``tail-p S (suc (``evalArg S₁ x))
    ``tail-p (`swap m) zero = refl
    ``tail-p (`swap m) (suc x) = refl

    `eval`` : ∀ {n} (S : `Syn n) → `evalArg S ≗ ``evalArg (translate S)
    `eval`` `id       x = refl
    `eval`` `swap zero = refl
    `eval`` `swap (suc zero) = refl
    `eval`` `swap (suc (suc x)) = refl
    `eval`` (`tail S) zero = ``tail-p (translate S) zero
    `eval`` (`tail S) (suc x) rewrite `eval`` S x = ``tail-p (translate S) (suc x)
    `eval`` (S `∘ S₁) x rewrite ``∘-p (translate S) (translate S₁) x | sym (`eval`` S₁ x) | `eval`` S (`evalArg S₁ x) = refl


  data Fin-View : ∀ {n} → Fin n → ★ where
    max : ∀ {n} → Fin-View (fromℕ n)
    inject : ∀ {n} → (i : Fin n) → Fin-View (inject₁ i)

  data _≤F_ : ∀ {n} → Fin n → Fin n → ★ where
    z≤i : {n : ℕ}{i : Fin (suc n)} → zero ≤F i
    s≤s : {n : ℕ}{i j : Fin n} → i ≤F j → suc i ≤F suc j

  ≤F-refl : ∀ {n} (x : Fin n) → x ≤F x
  ≤F-refl zero = z≤i
  ≤F-refl (suc i) = s≤s (≤F-refl i)

  _<F_ : ∀ {n} → Fin n → Fin n → ★
  i <F j = suc i ≤F inject₁ j

  nsuc-inj : ∀ {x y} → Data.Nat.NP.suc x ≡ suc y → x ≡ y
  nsuc-inj refl = refl

  suc-inj : ∀ {n}{i j : Fin n} → Data.Fin.suc i ≡ suc j → i ≡ j
  suc-inj refl = refl 

  data Sorted {X}(XC : Cmp X) : ∀ {l} → Vec X l  → ★ where
    []  : Sorted XC []
    sing : ∀ x → Sorted XC (x ∷ [])
    dbl-lt  : ∀ {l} x y {xs : Vec X l} → lt ≡ XC x y → Sorted XC (y ∷ xs) → Sorted XC (x ∷ y ∷ xs)
    dbl-eq  : ∀ {l} x {xs : Vec X l} → Sorted XC (x ∷ xs) → Sorted XC (x ∷ x ∷ xs)

  opposite : Ord → Ord
  opposite lt = gt
  opposite eq = eq
  opposite gt = lt

  flip-RC : ∀ {n}(x y : Fin n) → opposite (`RC x y) ≡ `RC y x
  flip-RC zero zero = refl
  flip-RC zero (suc y) = refl
  flip-RC (suc x) zero = refl
  flip-RC (suc x) (suc y) = flip-RC x y

  eq=>≡ : ∀ {i} (x y : Fin i) → eq ≡ `RC x y → x ≡ y
  eq=>≡ zero zero p = refl
  eq=>≡ zero (suc y) ()
  eq=>≡ (suc x) zero ()
  eq=>≡ (suc x) (suc y) p rewrite eq=>≡ x y p = refl

  insert-Sorted : ∀ {n l}{V : Vec (Fin n) l}(x : Fin n) → Sorted {Fin n} `RC V → Sorted {Fin n} `RC (insert `RC x V)
  insert-Sorted x [] = sing x
  insert-Sorted x (sing x₁) with `RC x x₁ | dbl-lt {XC = `RC} x x₁ {[]} | eq=>≡ x x₁ | flip-RC x x₁
  insert-Sorted x (sing x₁) | lt | b | _ | _ = b refl (sing x₁)
  insert-Sorted x (sing x₁) | eq | _ | p | _ rewrite p refl = dbl-eq x₁ (sing x₁)
  insert-Sorted x (sing x₁) | gt | b | _ | l = dbl-lt x₁ x l (sing x)
  insert-Sorted x (dbl-lt y y' {xs} prf xs₁) with `RC x y | dbl-lt {XC = `RC} x y {y' ∷ xs} | eq=>≡ x y | flip-RC x y
  insert-Sorted x (dbl-lt y y' prf xs₁) | lt | b | p | l₁ = b refl (dbl-lt y y' prf xs₁)
  insert-Sorted x (dbl-lt y y' prf xs₁) | eq | b | p | l₁ rewrite p refl = dbl-eq y (dbl-lt y y' prf xs₁)
  insert-Sorted x (dbl-lt y y' {xs} prf xs₁) | gt | b | p | l₁ with `RC x y' | insert-Sorted x xs₁
  insert-Sorted x (dbl-lt y y' prf xs₁) | gt | b | p | l₁ | lt | xs' = dbl-lt y x l₁ xs'
  insert-Sorted x (dbl-lt y y' prf xs₁) | gt | b | p | l₁ | eq | xs' = dbl-lt y x l₁ xs'
  insert-Sorted x (dbl-lt y y' prf xs₁) | gt | b | p | l₁ | gt | xs' = dbl-lt y y' prf xs'
  insert-Sorted x (dbl-eq y {xs} xs₁) with `RC x y | inspect (`RC x) y | dbl-lt {XC = `RC} x y {y ∷ xs} | eq=>≡ x y | flip-RC x y | insert-Sorted x xs₁
  insert-Sorted x (dbl-eq y xs₁) | lt | _ | b | p | l | _ = b refl (dbl-eq y xs₁)
  insert-Sorted x (dbl-eq y xs₁) | eq | _ | b | p | l | _ rewrite p refl = dbl-eq y (dbl-eq y xs₁)
  insert-Sorted x (dbl-eq y xs₁) | gt | [ prf ] | b | p | l | ss  rewrite prf = dbl-eq y ss 

  sort-Sorted : ∀ {n l}(V : Vec (Fin n) l) → Sorted `RC (`sort `RC V)
  sort-Sorted [] = []
  sort-Sorted (x ∷ V) = insert-Sorted x (sort-Sorted V)

  RC-refl : ∀ {i}(x : Fin i) → `RC x x ≡ eq
  RC-refl zero = refl
  RC-refl (suc x) = RC-refl x

  STail : ∀ {X l}{XC : Cmp X}{xs : Vec X (suc l)} → Sorted XC xs → Sorted XC (tail xs)
  STail (sing x) = []
  STail (dbl-lt x y x₁ T) = T
  STail (dbl-eq x T) = T

  module sproof {X}(XC : Cmp X)(XC-refl : ∀ x → XC x x ≡ eq)
     (eq≡ : ∀ x y → XC x y ≡ eq → x ≡ y)
     (lt-trans : ∀ x y z → XC x y ≡ lt → XC y z ≡ lt → XC x z ≡ lt)
     (XC-flip : ∀ x y → opposite (XC x y) ≡ XC y x)
     where

    open import Data.Sum

    _≤X_ : X → X → ★
    x ≤X y = XC x y ≡ lt ⊎ XC x y ≡ eq

    ≤X-trans : ∀ {x y z} → x ≤X y → y ≤X z → x ≤X z
    ≤X-trans (inj₁ x₁) (inj₁ x₂) = inj₁ (lt-trans _ _ _ x₁ x₂)
    ≤X-trans {_}{y}{z}(inj₁ x₁) (inj₂ y₁) rewrite eq≡ y z y₁ = inj₁ x₁
    ≤X-trans {x}{y} (inj₂ y₁) y≤z rewrite eq≡ x y y₁ = y≤z

    h≤t : ∀ {n}{T : `Tree X (2 + n)} → Sorted XC T → head T ≤X head (tail T)
    h≤t (dbl-lt x y x₁ ST) = inj₁ (sym x₁)
    h≤t (dbl-eq x ST) rewrite XC-refl x = inj₂ refl

    head-p : ∀ {n}{T : `Tree X (suc n)} i → Sorted XC T → head T ≤X `toFun T i
    head-p {T = T} zero ST rewrite XC-refl (head T) = inj₂ refl
    head-p {zero} (suc ()) ST
    head-p {suc n} (suc i) ST = ≤X-trans (h≤t ST) (head-p i (STail ST))

    toFun-p : ∀ {n}{T : `Tree X n}{i j : Fin n} → i ≤F j → Sorted XC T → `toFun T i ≤X `toFun T j
    toFun-p {j = j} z≤i ST = head-p j ST
    toFun-p (s≤s i≤Fj) ST = toFun-p i≤Fj (STail ST)

    sort-proof : ∀ {i}{T : `Tree X i} → Sorted XC T → Is-Mono `RC XC (`toFun T)
    sort-proof {T = T} T₁ zero zero rewrite XC-refl (head T) = _
    sort-proof T₁ zero (suc y) with toFun-p (z≤i {i = suc y}) T₁
    sort-proof T zero (suc y) | inj₁ x rewrite x = _
    sort-proof T zero (suc y) | inj₂ y₁ rewrite y₁ = _
    sort-proof {T = T} T₁ (suc x) zero with toFun-p (z≤i {i = suc x}) T₁ | XC-flip (head T) (`toFun (tail T) x)
    sort-proof T (suc x) zero | inj₁ x₁ | l rewrite x₁ | sym l = _
    sort-proof T (suc x) zero | inj₂ y | l rewrite y | sym l = _
    sort-proof T₁ (suc x) (suc y) = sort-proof (STail T₁) x y

  lt-trans-RC : ∀ {i} (x y z : Fin i) → `RC x y ≡ lt → `RC y z ≡ lt → `RC x z ≡ lt
  lt-trans-RC zero zero zero x<y y<z = y<z
  lt-trans-RC zero zero (suc z) x<y y<z = refl
  lt-trans-RC zero (suc y) zero x<y ()
  lt-trans-RC zero (suc y) (suc z) x<y y<z = refl
  lt-trans-RC (suc x) zero zero x<y y<z = x<y
  lt-trans-RC (suc x) zero (suc z) () y<z
  lt-trans-RC (suc x) (suc y) zero x<y y<z = y<z
  lt-trans-RC (suc x) (suc y) (suc z) x<y y<z = lt-trans-RC x y z x<y y<z

  `sort-mono : ∀ {i}(T : `Tree (`Rep i) i) → Is-Mono `RC `RC (`toFun (`sort `RC T))
  `sort-mono T x y = sproof.sort-proof `RC RC-refl (λ x₁ y₁ x₂ → eq=>≡ x₁ y₁ (sym x₂)) lt-trans-RC flip-RC (sort-Sorted T) x y



  module toNat n (f : Endo (Fin (suc n)))(f-inj : Is-Inj f)(f-mono : Is-Mono `RC `RC f) where
  
    import prefect-bintree-sorting
    open prefect-bintree-sorting.MM
    open import Data.Sum

    move-to-RC : ∀ {n}{x y : Fin n} → x ≤F y → `RC x y ≡ lt ⊎ `RC x y ≡ eq
    move-to-RC {y = zero} z≤i = inj₂ refl
    move-to-RC {y = suc y} z≤i = inj₁ refl
    move-to-RC (s≤s x≤Fy) = move-to-RC x≤Fy

    move-from-RC : ∀ {n}(x y : Fin n) → lt ≡ `RC x y ⊎ eq ≡ `RC x y → x ≤F y
    move-from-RC zero zero prf = z≤i
    move-from-RC zero (suc y) prf = z≤i
    move-from-RC (suc x) zero (inj₁ ())
    move-from-RC (suc x) zero (inj₂ ())
    move-from-RC (suc x) (suc y) prf = s≤s (move-from-RC x y prf)

    proper-mono : ∀ {x y} → x ≤F y → f x ≤F f y
    proper-mono {x} {y} x≤Fy with `RC x y | `RC (f x) (f y) | move-to-RC x≤Fy | f-mono x y | move-from-RC (f x) (f y)
    proper-mono x≤Fy | .lt | lt | inj₁ refl | r4 | r5 = r5 (inj₁ refl)
    proper-mono x≤Fy | .lt | eq | inj₁ refl | r4 | r5 = r5 (inj₂ refl)
    proper-mono x≤Fy | .lt | gt | inj₁ refl | () | r5
    proper-mono x≤Fy | .eq | lt | inj₂ refl | () | r5
    proper-mono x≤Fy | .eq | eq | inj₂ refl | r4 | r5 = r5 (inj₂ refl)
    proper-mono x≤Fy | .eq | gt | inj₂ refl | () | r5

    getFrom : ∀ n → ℕ → Fin (suc n)
    getFrom zero i = zero
    getFrom (suc n₁) zero = zero
    getFrom (suc n₁) (suc i) = suc (getFrom n₁ i)

    getInj : {n x y : ℕ} → x ≤ n → y ≤ n → getFrom n x ≡ getFrom n y → x ≡ y
    getInj z≤n z≤n prf = refl
    getInj z≤n (s≤s y≤n) ()
    getInj (s≤s x≤n) z≤n ()
    getInj (s≤s x≤n) (s≤s y≤n) prf rewrite (getInj x≤n y≤n (suc-inj prf)) = refl

    getMono : {n x y : ℕ} → x ≤ y → y ≤ n → getFrom n x ≤F getFrom n y
    getMono z≤n z≤n = ≤F-refl _
    getMono z≤n (s≤s y≤n) = z≤i
    getMono (s≤s x≤y) (s≤s y≤n) = s≤s (getMono x≤y y≤n)

    forget : ∀ {n} → Fin n → ℕ
    forget zero = zero
    forget (suc i) = suc (forget i)

    forgetInj : ∀ {n}{i j : Fin n} → forget i ≡ forget j → i ≡ j
    forgetInj {.(suc _)} {zero} {zero} prf = refl
    forgetInj {.(suc _)} {zero} {suc j} ()
    forgetInj {.(suc _)} {suc i} {zero} ()
    forgetInj {.(suc _)} {suc i} {suc j} prf rewrite forgetInj (nsuc-inj prf) = refl

    getForget : ∀ {n}(i : Fin (suc n)) → getFrom n (forget i) ≡ i
    getForget {zero} zero = refl
    getForget {zero} (suc ())
    getForget {suc n₁} zero = refl
    getForget {suc n₁} (suc i) rewrite getForget i = refl


    forget< : ∀ {n} → (i : Fin n) → forget i < n
    forget< {zero} ()
    forget< {suc n₁} zero = s≤s z≤n
    forget< {suc n₁} (suc i) = s≤s (forget< i)

    forget-mono : ∀ {n}{i j : Fin n} → i ≤F j → forget i ≤ forget j
    forget-mono z≤i = z≤n
    forget-mono (s≤s i≤F) = s≤s (forget-mono i≤F)

    fn : Endo ℕ
    fn = forget ∘ f ∘ getFrom n

    return : f ≗ getFrom n ∘ fn ∘ forget
    return x rewrite getForget x | getForget (f x) = refl

    fn-monotone : Monotone (suc n) fn
    fn-monotone {x} {y} x≤y (s≤s y≤n) = forget-mono (proper-mono (getMono x≤y y≤n))

    fn-inj : IsInj (suc n) fn
    fn-inj {x}{y} (s≤s sx≤sn) (s≤s sy≤sn) prf = getInj sx≤sn sy≤sn (f-inj (getFrom n x) (getFrom n y) (forgetInj prf))

    fn-bounded : Bounded (suc n) fn
    fn-bounded x _ = forget< (f (getFrom n x))

    fn≗id : ∀ x → x < (suc n) → fn x ≡ x
    fn≗id = M.is-id fn fn-monotone fn-inj fn-bounded 

    f≗id : f ≗ id
    f≗id x rewrite return x | fn≗id (forget x) (forget< x) = getForget x

  fin-view : ∀ {n} → (i : Fin (suc n)) → Fin-View i
  fin-view {zero} zero = max
  fin-view {zero} (suc ())
  fin-view {suc n} zero = inject _
  fin-view {suc n} (suc i) with fin-view i
  fin-view {suc n} (suc .(fromℕ n)) | max = max
  fin-view {suc n} (suc .(inject₁ i)) | inject i = inject _

  absurd : {X : ★} → .⊥ → X
  absurd ()

  drop₁ : ∀ {n} → (i : Fin (suc n)) → .(i ≢ fromℕ n) → Fin n
  drop₁ i neq with fin-view i
  drop₁ {n} .(fromℕ n) neq | max = absurd (neq refl)
  drop₁ .(inject₁ i) neq | inject i = i

  drop₁→inject₁ : ∀ {n}(i : Fin (suc n))(j : Fin n).(p : i ≢ fromℕ n) → drop₁ i p ≡ j → i ≡ inject₁ j
  drop₁→inject₁ i j p q with fin-view i
  drop₁→inject₁ {n} .(fromℕ n) j p q | max = absurd (p refl)
  drop₁→inject₁ .(inject₁ i) j p q | inject i = cong inject₁ q


  `mono-inj→id : ∀{i}(f : Endo (`Rep i)) → Is-Inj f → Is-Mono `RC `RC f → f ≗ id
  `mono-inj→id {zero}  = λ f x x₁ ()
  `mono-inj→id {suc i} = toNat.f≗id i 


  interface : Interface
  interface = record 
    { Ix            = `Ix
    ; Rep           = `Rep
    ; Syn           = `Syn
    ; Tree          = `Tree
    ; fromFun       = `fromFun
    ; toFun         = `toFun
    ; toFun∘fromFun = `toFun∘fromFun
    ; evalArg       = `evalArg
    ; evalTree      = `evalTree
    ; eval-proof    = `eval-proof
    ; inv           = `inv
    ; inv-proof     = `inv-proof
    ; RC            = `RC
    ; sort          = `sort
    ; sort-syn      = `sort-syn
    ; sort-proof    = `sort-proof
    ; sort-mono     = `sort-mono
    ; mono-inj→id   = `mono-inj→id
    }

  open import Data.Bool.NP

  count : ∀ {n} → (Fin n → ℕ) → ℕ
  count {n} f = sum (tabulate f)

  count-ext : ∀ {n} → (f g : Fin n → ℕ) → f ≗ g → count f ≡ count g
  count-ext {zero} f g f≗g = refl
  count-ext {suc n} f g f≗g rewrite f≗g zero | count-ext (f ∘ suc) (g ∘ suc) (f≗g ∘ suc) = refl

  #⟨_⟩ : ∀ {n} → (Fin n → Bool) → ℕ
  #⟨ f ⟩ = count (λ x → if f x then 1 else 0)

  #-ext : ∀ {n} → (f g : Fin n → Bool) → f ≗ g → #⟨ f ⟩ ≡ #⟨ g ⟩
  #-ext f g f≗g = count-ext (toℕ ∘ f) (toℕ ∘ g) (cong toℕ ∘ f≗g)

  com-assoc : ∀ x y z → x + (y + z) ≡ y + (x + z)
  com-assoc x y z rewrite 
    sym (ℕ°.+-assoc x y z) |
    ℕ°.+-comm x y    |
    ℕ°.+-assoc y x z = refl
    
  syn-pres : ∀ {n}(f : Fin n → ℕ)(S : `Syn n)
           → count f ≡ count (f ∘ `evalArg S)
  syn-pres f `id = refl
  syn-pres f `swap = com-assoc (f zero) (f (suc zero)) (count (λ i → f (suc (suc i))))
  syn-pres f (`tail S) rewrite syn-pres (f ∘ suc) S = refl
  syn-pres f (S `∘ S₁) rewrite syn-pres f S = syn-pres (f ∘ `evalArg S) S₁

  count-perm : ∀ {n}(f : Fin n → ℕ)(p : Endo (Fin n)) → Is-Inj p
         → count f ≡ count (f ∘ p)
  count-perm f p p-inj = trans (syn-pres f (sort-bij p)) (count-ext _ _ f∘eval≗f∘p)
   where
     open abs interface
     f∘eval≗f∘p : f ∘ `evalArg (sort-bij p) ≗ f ∘ p
     f∘eval≗f∘p x rewrite thm p p-inj x = refl


  #-perm : ∀ {n}(f : Fin n → Bool)(p : Endo (Fin n)) → Is-Inj p
         → #⟨ f ⟩ ≡ #⟨ f ∘ p ⟩
  #-perm f p p-inj = count-perm (toℕ ∘ f) p p-inj

  test : `Syn 8
  test = abs.sort-bij interface (λ x → `evalArg (`tail `swap) x)