{-# OPTIONS --cubical #-}
module FMSetAll where
open import Cubical.Foundations.Everything
open import Cubical.Functions.Logic using (_⊓_; ⊤ ; ⊓-comm ; ⊓-assoc ; ⊓-identityˡ)
open import Cubical.HITs.FiniteMultiset
open import Cubical.Data.Unit.Base

module _ {n m : Level} {A : Type n} {P : A → hProp m} where
  private
    module P♯ = FMSetUniversal isSetHProp (⊤ {m}) _⊓_ ⊓-comm ⊓-assoc ⊓-identityˡ P

  opaque
    allI : FMSet A → hProp m
    allI = P♯.f-extend

    uncons-A : {x : A} {xs : FMSet A} → ⟨ allI (x ∷ xs) ⟩ → ⟨ P x ⊓ allI xs ⟩
    uncons-A {x = x} {xs = xs} = subst ⟨_⟩ $ P♯.f-extend-cons x xs

    infixr  _∷-A_
    _∷-A_ : {x : A} {xs : FMSet A} → ⟨ P x ⟩ → ⟨ allI xs ⟩ → ⟨ allI (x ∷ xs) ⟩
    _∷-A_ {x = x} {xs = xs} Px all-xs = subst ⟨_⟩ (sym $ P♯.f-extend-cons x xs) (Px , all-xs)

    []-A : ⟨ allI [] ⟩
    []-A = tt*

    infixr  _++-A_
    _++-A_ : {xs ys : FMSet A} → ⟨ allI xs ⟩ → ⟨ allI ys ⟩ → ⟨ allI (xs ++ ys) ⟩
    _++-A_ {xs = xs} {ys = ys} axs ays = subst ⟨_⟩ (sym (P♯.f-extend-++ xs ys)) (axs ,  ays)

All : {n m : Level} {A : Type n} (P : A → hProp m) → FMSet A → Type m
All P xs = ⟨ allI {P = P} xs ⟩


mapAll : {n m : Level} {A : Type n} (P : A → hProp m) (Q : A → hProp m) (P⇒Q : ∀ {x} → ⟨ P x ⟩ → ⟨ Q x ⟩) → ∀ {xs} → All P xs → All Q xs
mapAll P Q P→Q {xs = xs} = ElimProp.f
    {B = λ xs → All P xs → All Q xs}
    (λ {xs = xs1} → isPropΠ λ _ → snd $ allI {P = Q} xs1)
    (λ _ → []-A)
    (λ x {xs1} IH allx∷xs1 → let ( Px , allPxs1 ) = uncons-A allx∷xs1 in
    P→Q Px ∷-A IH allPxs1) xs