module wip.arity where
open import 1Lab.Prelude
open import Data.Fin.Closure
open import Data.Fin

{-
record Arity-class {ℓ s} (small : Type ℓ → Type s) : Type (lsuc ℓ ⊔ s) where
  field
    single : small (Lift ℓ ⊤)
    small-fibres : ∀ {I J : Type ℓ} → (f : I → J) → small J → (∀ j → small (fibre f j)) → small I
    fibres-small : ∀ {I J : Type ℓ} → (f : I → J) → small J → small I → (∀ j → small (fibre f j))
    down-closed : ∀ {I J : Type ℓ} → (f : I → J) → is-embedding f → small J → small I

is-finite : ∀ {ℓ} → Type ℓ → Type ℓ
is-finite T = Σ[ n ∈ Nat ] (T ≃ Fin n)

open Arity-class

finite : ∀ {ℓ} → Arity-class {ℓ} is-finite
finite .single = 1 , {!   !}
finite .small-fibres {I = I} {J} f ix-fin fib-fin = _ , t where
  t : I ≃ Fin _
  t =
    I
        ≃⟨ Total-equiv f ⟩
    Σ[ j ∈ J ] (fibre f j)
        ≃⟨ Σ-ap (ix-fin .snd)
                (λ x → fib-fin x .snd
                    ∙e path→equiv (ap (λ e → Fin (fib-fin e .fst))
                                      (sym (equiv→retraction (ix-fin .snd .snd) _)))) ⟩
    Σ[ j ∈ Fin (ix-fin .fst) ] Fin (fib-fin (equiv→inverse (ix-fin .snd .snd) j) .fst)
        ≃⟨ Finite-sum _ ⟩
    Fin _ ≃∎
finite .fibres-small f j-fin i-fin point = {!   !}
finite .down-closed f embed j-fin = {!   !}

sum-permute : ∀ {n} → (σ : Fin n → Fin n) → is-iso σ → (f : Fin n → Nat) → sum n (f ∘ σ) ≡ sum n f
sum-permute σ isom f = aux (σ , is-iso→is-equiv isom) f where
  aux : ∀ {n B} (σ : Fin n ≃ B) (f : B → Nat) → sum n (f ∘ σ .fst) ≡ sum n {!  f !}
  aux σ f = {!   !}
  -}