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 = {! !} -}