{-# OPTIONS --safe #-}
open import Multiset.Prelude
module Multiset.Equivalences.FCM-HeadPList {X : Type} where
open import Multiset.FCM as M
using (M ; _⊕_)
open import Cubical.Foundations.Equiv using (_≃_)
open import Cubical.Foundations.Isomorphism using (Iso ; isoToEquiv)
open import Cubical.Foundations.HLevels
open import Cubical.HITs.FiniteMultiset as HeadPList
using (_++_)
renaming (FMSet to HeadPList)
open Iso
MToHeadPList : M X → HeadPList X
MToHeadPList = M.rec HeadPList.trunc
HeadPList.[] HeadPList.[_] HeadPList._++_
(λ _ → refl) HeadPList.assoc-++ HeadPList.comm-++
HeadPListToM : HeadPList X → M X
HeadPListToM = HeadPList.Elim.f
M.ε
(λ x xs → x M.∷ xs)
(λ x y xs → M.∷-swap x y xs)
(λ _ → M.isSetM)
isMonoidHomHeadPListToM : ∀ xs ys
→ HeadPListToM (xs HeadPList.++ ys) ≡ HeadPListToM xs ⊕ HeadPListToM ys
isMonoidHomHeadPListToM = HeadPList.ElimProp.f (isPropΠ (λ ys → M.isSetM _ _))
(λ ys → sym (M.unit (HeadPListToM ys)))
λ x {xs} indH ys →
HeadPListToM (x HeadPList.∷ (xs ++ ys)) ≡⟨⟩
x M.∷ HeadPListToM (xs ++ ys) ≡⟨ cong (x M.∷_) (indH ys) ⟩
x M.∷ (HeadPListToM xs ⊕ HeadPListToM ys) ≡⟨ M.assoc _ _ _ ⟩
(M.η x ⊕ HeadPListToM xs) ⊕ HeadPListToM ys ≡⟨⟩
HeadPListToM (x HeadPList.∷ xs) ⊕ HeadPListToM ys ∎
M-HeadPList-Iso : Iso (M X) (HeadPList X)
M-HeadPList-Iso .fun = MToHeadPList
M-HeadPList-Iso .inv = HeadPListToM
M-HeadPList-Iso .leftInv = M.ind (λ xs → M.isSetM _ xs) refl (λ x → M.unit' (M.η x)) goal where
goal : ∀ {xs ys : M X} →
HeadPListToM (MToHeadPList xs) ≡ xs →
HeadPListToM (MToHeadPList ys) ≡ ys →
HeadPListToM (MToHeadPList (xs ⊕ ys)) ≡ xs ⊕ ys
goal {xs} {ys} indH-xs indH-ys =
HeadPListToM (MToHeadPList (xs ⊕ ys)) ≡⟨⟩
HeadPListToM (MToHeadPList xs ++ MToHeadPList ys ) ≡⟨ isMonoidHomHeadPListToM (MToHeadPList xs) (MToHeadPList ys) ⟩
HeadPListToM (MToHeadPList xs) ⊕ HeadPListToM (MToHeadPList ys) ≡⟨ cong₂ _⊕_ indH-xs indH-ys ⟩
xs ⊕ ys ∎
M-HeadPList-Iso .rightInv = HeadPList.ElimProp.f (HeadPList.trunc _ _) refl goal where
goal : ∀ x {xs}
→ MToHeadPList (HeadPListToM xs) ≡ xs
→ MToHeadPList (HeadPListToM (x HeadPList.∷ xs)) ≡ x HeadPList.∷ xs
goal x {xs} indH-xs =
HeadPList.[ x ] ++ MToHeadPList (HeadPListToM xs) ≡⟨ cong (HeadPList.[ x ] ++_) indH-xs ⟩
x HeadPList.∷ xs ∎
M≃HeadPList : M X ≃ HeadPList X
M≃HeadPList = isoToEquiv M-HeadPList-Iso