module Cubical.Structures.Set.CMon.Bag.Free where
open import Cubical.Structures.Prelude
import Cubical.Data.Empty as ⊥
open import Cubical.Data.Fin
open import Cubical.Data.List renaming (_∷_ to _∷ₗ_)
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎
import Cubical.Structures.Set.CMon.Desc as M
import Cubical.Structures.Set.Mon.Desc as M
import Cubical.Structures.Free as F
open import Cubical.Structures.Set.Mon.Array as A
open import Cubical.Structures.Set.Mon.List as L
open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq
open import Cubical.Structures.Arity hiding (_/_)
open import Cubical.Structures.Set.CMon.QFreeMon
open import Cubical.Structures.Set.CMon.Bag.Base
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base
open Iso
private
variable
ℓ ℓ' ℓ'' : Level
A : Type ℓ
Bag≈ = _≈_
refl≈ : {as : Array A} -> as ≈ as
refl≈ {as = as} = idIso , refl
sym≈ : {as bs : Array A} -> as ≈ bs -> bs ≈ as
sym≈ {as = (n , f)} {bs = (m , g)} (σ , p) =
invIso σ , congS (g ∘_) (sym (funExt (σ .rightInv)))
∙ congS (_∘ σ .inv) (sym p)
trans≈ : {as bs cs : Array A} -> as ≈ bs -> bs ≈ cs -> as ≈ cs
trans≈ {as = (n , f)} {bs = (m , g)} {cs = (o , h)} (σ , p) (τ , q) =
compIso σ τ , sym
((h ∘ τ .fun) ∘ σ .fun ≡⟨ congS (_∘ σ .fun) (sym q) ⟩
g ∘ σ .fun ≡⟨ sym p ⟩
f ∎)
isEquiv≈ : ∀ {A : Type ℓ} -> BinaryRelation.isEquivRel {A = Array A} _≈_
isEquiv≈ .BinaryRelation.isEquivRel.reflexive as = refl≈
isEquiv≈ .BinaryRelation.isEquivRel.symmetric as bs = sym≈
isEquiv≈ .BinaryRelation.isEquivRel.transitive as bs cs = trans≈ {cs = cs}
Fin+-cong : {n m n' m' : ℕ} -> Iso (Fin n) (Fin n') -> Iso (Fin m) (Fin m') -> Iso (Fin (n + m)) (Fin (n' + m'))
Fin+-cong {n} {m} {n'} {m'} σ τ =
compIso (Fin≅Fin+Fin n m) (compIso (⊎Iso σ τ) (invIso (Fin≅Fin+Fin n' m')))
⊎IsoEta : {A B A' B' : Type ℓ} {C : Type ℓ'} (f : A' -> C) (g : B' -> C)
-> (σ : Iso A A') (τ : Iso B B')
-> ⊎.rec (f ∘ σ .fun) (g ∘ τ .fun) ≡ ⊎.rec f g ∘ ⊎Iso σ τ .fun
⊎IsoEta f g σ τ = ⊎E (⊎.rec f g ∘ ⊎Iso σ τ .fun) refl refl
⊎SwapEta : {A B : Type ℓ} {C : Type ℓ'} (f : A -> C) (g : B -> C)
-> ⊎.rec f g ≡ ⊎.rec g f ∘ ⊎-swap-Iso .fun
⊎SwapEta f g = ⊎E (⊎.rec g f ∘ ⊎-swap-Iso .fun) refl refl
cong≈ : {as bs cs ds : Array A} -> as ≈ bs -> cs ≈ ds -> (as ⊕ cs) ≈ (bs ⊕ ds)
cong≈ {as = n , f} {bs = n' , f'} {m , g} {m' , g'} (σ , p) (τ , q) =
Fin+-cong σ τ ,
(
combine n m f g
≡⟨ cong₂ (combine n m) p q ⟩
combine n m (f' ∘ σ .fun) (g' ∘ τ .fun)
≡⟨⟩
⊎.rec (f' ∘ σ .fun) (g' ∘ τ .fun) ∘ finSplit n m
≡⟨ congS (_∘ finSplit n m) (⊎IsoEta f' g' σ τ) ⟩
⊎.rec f' g' ∘ ⊎Iso σ τ .fun ∘ finSplit n m
≡⟨⟩
⊎.rec f' g' ∘ idfun _ ∘ ⊎Iso σ τ .fun ∘ finSplit n m
≡⟨ congS (\h -> ⊎.rec f' g' ∘ h ∘ ⊎Iso σ τ .fun ∘ finSplit n m) (sym (funExt (Fin≅Fin+Fin n' m' .rightInv))) ⟩
⊎.rec f' g' ∘ (Fin≅Fin+Fin n' m' .fun ∘ Fin≅Fin+Fin n' m' .inv) ∘ ⊎Iso σ τ .fun ∘ finSplit n m
≡⟨⟩
(⊎.rec f' g' ∘ Fin≅Fin+Fin n' m' .fun) ∘ (Fin≅Fin+Fin n' m' .inv ∘ ⊎Iso σ τ .fun ∘ finSplit n m)
≡⟨⟩
combine n' m' f' g' ∘ Fin+-cong σ τ .fun
∎)
Fin+-comm : (n m : ℕ) -> Iso (Fin (n + m)) (Fin (m + n))
Fin+-comm n m = compIso (Fin≅Fin+Fin n m) (compIso ⊎-swap-Iso (invIso (Fin≅Fin+Fin m n)))
comm≈ : {as bs : Array A} -> (as ⊕ bs) ≈ (bs ⊕ as)
comm≈ {as = n , f} {bs = m , g} =
Fin+-comm n m , sym
(
⊎.rec g f ∘ finSplit m n ∘ Fin≅Fin+Fin m n .inv ∘ ⊎-swap-Iso .fun ∘ Fin≅Fin+Fin n m .fun
≡⟨⟩
⊎.rec g f ∘ (Fin≅Fin+Fin m n .fun ∘ Fin≅Fin+Fin m n .inv) ∘ ⊎-swap-Iso .fun ∘ Fin≅Fin+Fin n m .fun
≡⟨ congS (λ h -> ⊎.rec g f ∘ h ∘ ⊎-swap-Iso .fun ∘ Fin≅Fin+Fin n m .fun) (funExt (Fin≅Fin+Fin m n .rightInv)) ⟩
⊎.rec g f ∘ ⊎-swap-Iso .fun ∘ Fin≅Fin+Fin n m .fun
≡⟨ congS (_∘ Fin≅Fin+Fin n m .fun) (sym (⊎SwapEta f g)) ⟩
⊎.rec f g ∘ Fin≅Fin+Fin n m .fun
∎)
fpred' : ∀ {n} -> (x : Fin (suc n)) -> ¬ x ≡ fzero -> Fin n
fpred' (zero , p) q = ⊥.rec (q (Fin-fst-≡ refl))
fpred' (suc w , p) q = w , pred-≤-pred p
fpred : ∀ {n} -> Fin (suc (suc n)) -> Fin (suc n)
fpred (zero , p) = fzero
fpred (suc w , p) = w , pred-≤-pred p
fsuc∘fpred : ∀ {n} -> (x : Fin (suc (suc n))) -> ¬ x ≡ fzero -> fsuc (fpred x) ≡ x
fsuc∘fpred (zero , p) q = ⊥.rec (q (Fin-fst-≡ refl))
fsuc∘fpred (suc k , p) q = Fin-fst-≡ refl
fpred∘fsuc : ∀ {n} -> (x : Fin (suc n)) -> fpred (fsuc x) ≡ x
fpred∘fsuc (k , p) = Fin-fst-≡ refl
isoFunInv : ∀ {A B : Type ℓ} {x y} -> (σ : Iso A B) -> σ .fun x ≡ y -> σ .inv y ≡ x
isoFunInv σ p = congS (σ .inv) (sym p) ∙ σ .leftInv _
isoFunInvContra : ∀ {A B : Type ℓ} {x y z} -> (σ : Iso A B) -> σ .fun x ≡ y -> ¬ (z ≡ y) -> ¬ (σ .inv z ≡ x)
isoFunInvContra σ p z≠y q = z≠y (sym (σ .rightInv _) ∙ congS (σ .fun) q ∙ p)
autInvIs0 : ∀ {n} -> (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n))))
-> σ .fun fzero ≡ fzero -> σ .inv fzero ≡ fzero
autInvIs0 = isoFunInv
autSucNot0 : ∀ {n} -> (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n))))
-> (x : Fin (suc n)) -> σ .fun fzero ≡ fzero -> ¬ σ .fun (fsuc x) ≡ fzero
autSucNot0 σ x p = isoFunInvContra (invIso σ) (isoFunInv σ p) (snotz ∘ congS fst)
punchOutZero : ∀ {n} (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n)))) -> σ .fun fzero ≡ fzero
-> Iso (Fin (suc n)) (Fin (suc n))
punchOutZero {n = n} σ p =
iso (punch σ) (punch (invIso σ)) (punch∘punch σ p) (punch∘punch (invIso σ) (autInvIs0 σ p))
where
punch : Iso (Fin (suc (suc n))) (Fin (suc (suc n))) -> Fin (suc n) -> Fin (suc n)
punch σ = fpred ∘ σ .fun ∘ fsuc
punch∘punch : (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n))))
-> σ .fun fzero ≡ fzero
-> (x : Fin (suc n))
-> punch σ (punch (invIso σ) x) ≡ x
punch∘punch σ p x =
punch σ (punch (invIso σ) x)
≡⟨⟩
fpred (σ .fun ((fsuc ∘ fpred) (σ .inv (fsuc x))))
≡⟨ congS (fpred ∘ σ .fun) (fsuc∘fpred (σ .inv (fsuc x)) (autSucNot0 (invIso σ) x (autInvIs0 σ p))) ⟩
fpred (σ .fun (σ .inv (fsuc x)))
≡⟨ congS fpred (σ .rightInv (fsuc x)) ⟩
fpred (fsuc x)
≡⟨ fpred∘fsuc x ⟩
x ∎
punchOutZero≡fsuc : ∀ {n} (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n)))) -> (σ-0≡0 : σ .fun fzero ≡ fzero)
-> (w : Fin (suc n)) -> σ .fun (fsuc w) ≡ fsuc (punchOutZero σ σ-0≡0 .fun w)
punchOutZero≡fsuc σ σ-0≡0 w = sym (fsuc∘fpred _ (autSucNot0 σ w σ-0≡0))
finSubst : ∀ {n m} -> n ≡ m -> Fin n -> Fin m
finSubst {n = n} {m = m} p (k , q) = k , (subst (k <_) p q)
Fin≅ : ∀ {n m} -> n ≡ m -> Iso (Fin n) (Fin m)
Fin≅ {n = n} {m = m} p = iso
(finSubst p)
(finSubst (sym p))
(λ (k , q) -> Fin-fst-≡ refl)
(λ (k , q) -> Fin-fst-≡ refl)
Fin≅-inj : {n m : ℕ} -> Iso (Fin n) (Fin m) -> n ≡ m
Fin≅-inj {n = n} {m = m} σ = Fin-inj n m (isoToPath σ)
≈-length : {n m : ℕ} -> Iso (Fin n) (Fin m) -> n ≡ m
≈-length {n = n} {m = m} σ = Fin-inj n m (isoToPath σ)
module _ {n} (σ : Iso (Fin (suc n)) (Fin (suc n))) where
private
m : ℕ
m = suc n
cutoff : ℕ
cutoff = (σ .inv fzero) .fst
cutoff< : cutoff < m
cutoff< = (σ .inv fzero) .snd
cutoff+- : cutoff + (m ∸ cutoff) ≡ m
cutoff+- = ∸-lemma (<-weaken cutoff<)
0<m-cutoff : 0 < m ∸ cutoff
0<m-cutoff = n∸l>0 m cutoff cutoff<
swapAut : Iso (Fin (suc n)) (Fin (suc n))
swapAut = compIso (Fin≅ (sym cutoff+- ∙ +-comm cutoff _)) (compIso (Fin+-comm (m ∸ cutoff) cutoff) (compIso (Fin≅ cutoff+-) σ))
swapAut0≡0 : swapAut .fun fzero ≡ fzero
swapAut0≡0 =
σ .fun (finSubst cutoff+- (⊎.rec finCombine-inl finCombine-inr (fun ⊎-swap-Iso (finSplit (m ∸ cutoff) cutoff (0 , _)))))
≡⟨ congS (λ z -> σ .fun (finSubst cutoff+- (⊎.rec (finCombine-inl {m = cutoff}) (finCombine-inr {m = cutoff}) (fun ⊎-swap-Iso z)))) (finSplit-beta-inl 0 0<m-cutoff _) ⟩
σ .fun (σ .inv fzero .fst + 0 , _)
≡⟨ congS (σ .fun) (Fin-fst-≡ (+-zero (σ .inv (0 , suc-≤-suc zero-≤) .fst) ∙ congS (fst ∘ σ .inv) (Fin-fst-≡ refl))) ⟩
σ .fun (σ .inv fzero)
≡⟨ σ .rightInv fzero ⟩
fzero ∎
module _ {ℓA ℓB} {A : Type ℓA} {𝔜 : struct ℓB M.MonSig} (isSet𝔜 : isSet (𝔜 .car)) (𝔜-cmon : 𝔜 ⊨ M.CMonSEq) (f : A -> 𝔜 .car) where
module 𝔜 = M.CMonSEq 𝔜 𝔜-cmon
f♯Hom = ArrayDef.Free.ext arrayDef isSet𝔜 (M.cmonSatMon 𝔜-cmon) f
f♯ : Array A -> 𝔜 .car
f♯ = f♯Hom .fst
f♯Eta : (a : A) -> f♯ (η a) ≡ f a
f♯Eta a i = ArrayDef.Free.ext-η arrayDef isSet𝔜 (M.cmonSatMon 𝔜-cmon) f i a
f♯HomOplus : (as bs : Array A) -> f♯ (as ⊕ bs) ≡ f♯ as 𝔜.⊕ f♯ bs
f♯HomOplus as bs =
f♯ (as ⊕ bs) ≡⟨ sym ((f♯Hom .snd) M.`⊕ ⟪ as ⨾ bs ⟫) ⟩
𝔜 .alg (M.`⊕ , (λ w -> f♯ (⟪ as ⨾ bs ⟫ w))) ≡⟨ 𝔜.⊕Eta ⟪ as ⨾ bs ⟫ f♯ ⟩
f♯ as 𝔜.⊕ f♯ bs ∎
f♯Comm : (as bs : Array A) -> f♯ (as ⊕ bs) ≡ f♯ (bs ⊕ as)
f♯Comm as bs =
f♯ (as ⊕ bs) ≡⟨ f♯HomOplus as bs ⟩
f♯ as 𝔜.⊕ f♯ bs ≡⟨ 𝔜.comm (f♯ as) (f♯ bs) ⟩
f♯ bs 𝔜.⊕ f♯ as ≡⟨ sym (f♯HomOplus bs as) ⟩
f♯ (bs ⊕ as) ∎
swapAutToAut : ∀ {n} (zs : Fin (suc (suc n)) -> A) (σ : Iso (Fin (suc (suc n))) (Fin (suc (suc n))))
-> f♯ (suc (suc n) , zs ∘ swapAut σ .fun) ≡ f♯ (suc (suc n) , zs ∘ σ .fun)
swapAutToAut {n = n} zs σ =
f♯ (m , zs ∘ swapAut σ .fun)
≡⟨ congS f♯ lemma-α ⟩
f♯ (((m ∸ cutoff) , (zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff _ ∘ inr))
⊕ (cutoff , (zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff _ ∘ inl)))
≡⟨ f♯Comm ((m ∸ cutoff) , (zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff _ ∘ inr)) _ ⟩
f♯ ((cutoff , (zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff _ ∘ inl))
⊕ ((m ∸ cutoff) , (zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff _ ∘ inr)))
≡⟨ congS f♯ lemma-β ⟩
f♯ (m , zs ∘ σ .fun) ∎
where
m : ℕ
m = suc (suc n)
cutoff : ℕ
cutoff = (σ .inv fzero) .fst
cutoff< : cutoff < m
cutoff< = (σ .inv fzero) .snd
cutoff+- : cutoff + (m ∸ cutoff) ≡ m
cutoff+- = ∸-lemma (<-weaken cutoff<)
lemma-α : Path (Array A) (m , zs ∘ swapAut σ .fun) ((m ∸ cutoff) + cutoff , _)
lemma-α = Array≡ (sym cutoff+- ∙ +-comm cutoff _) λ k k<m∸cutoff+cutoff -> ⊎.rec
(λ k<m∸cutoff ->
zs (σ .fun (finSubst cutoff+- (⊎.rec finCombine-inl finCombine-inr (fun ⊎-swap-Iso (finSplit (m ∸ cutoff) cutoff (k , _))))))
≡⟨ congS (λ z -> zs (σ .fun (finSubst cutoff+- (⊎.rec (finCombine-inl {m = cutoff}) finCombine-inr (fun ⊎-swap-Iso z))))) (finSplit-beta-inl k k<m∸cutoff _) ⟩
zs (σ .fun (cutoff + k , _))
≡⟨ congS (zs ∘ σ .fun) (Fin-fst-≡ refl) ⟩
zs (σ .fun (finSubst cutoff+- (finCombine cutoff (m ∸ cutoff) (inr (k , k<m∸cutoff)))))
≡⟨⟩
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(inl (k , k<m∸cutoff))
≡⟨ congS (⊎.rec _ _) (sym (finSplit-beta-inl k k<m∸cutoff k<m∸cutoff+cutoff)) ⟩
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(finSplit (m ∸ cutoff) cutoff (k , k<m∸cutoff+cutoff))
∎)
(λ m∸cutoff≤k ->
zs (σ .fun (finSubst cutoff+- (⊎.rec finCombine-inl finCombine-inr (fun ⊎-swap-Iso (finSplit (m ∸ cutoff) cutoff (k , _))))))
≡⟨ congS (λ z -> zs (σ .fun (finSubst cutoff+- (⊎.rec (finCombine-inl {m = cutoff}) finCombine-inr (fun ⊎-swap-Iso z))))) (finSplit-beta-inr k _ m∸cutoff≤k (∸-<-lemma (m ∸ cutoff) cutoff k k<m∸cutoff+cutoff m∸cutoff≤k)) ⟩
zs (σ .fun (finSubst cutoff+- (finCombine-inl (k ∸ (m ∸ cutoff) , ∸-<-lemma (m ∸ cutoff) cutoff k k<m∸cutoff+cutoff m∸cutoff≤k))))
≡⟨ congS (zs ∘ σ .fun ∘ finSubst cutoff+-) (Fin-fst-≡ refl) ⟩
zs (σ .fun (finSubst cutoff+- (finCombine cutoff (m ∸ cutoff) (inl (k ∸ (m ∸ cutoff) , ∸-<-lemma (m ∸ cutoff) cutoff k k<m∸cutoff+cutoff m∸cutoff≤k)))))
≡⟨ congS (⊎.rec _ _) (sym (finSplit-beta-inr k k<m∸cutoff+cutoff m∸cutoff≤k (∸-<-lemma (m ∸ cutoff) cutoff k k<m∸cutoff+cutoff m∸cutoff≤k))) ⟩
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(finSplit (m ∸ cutoff) cutoff (k , k<m∸cutoff+cutoff))
∎)
(k ≤? (m ∸ cutoff))
lemma-β : Path (Array A) (cutoff + (m ∸ cutoff) , _) (m , zs ∘ σ .fun)
lemma-β = Array≡ cutoff+- λ k k<m -> ⊎.rec
(λ k<cutoff ->
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(finSplit cutoff (m ∸ cutoff) (k , _))
≡⟨ congS (⊎.rec _ _) (finSplit-beta-inl k k<cutoff _) ⟩
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(inl (k , _))
≡⟨⟩
zs (σ .fun (finSubst cutoff+- (finCombine cutoff (m ∸ cutoff) (inl (k , _)))))
≡⟨ congS (zs ∘ σ .fun) (Fin-fst-≡ refl) ⟩
zs (σ .fun (k , k<m))
∎)
(λ cutoff≤k ->
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(finSplit cutoff (m ∸ cutoff) (k , _))
≡⟨ congS (⊎.rec _ _) (finSplit-beta-inr k _ cutoff≤k (<-∸-< k m cutoff k<m cutoff<)) ⟩
⊎.rec
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inl)
(zs ∘ σ .fun ∘ finSubst cutoff+- ∘ finCombine cutoff (m ∸ cutoff) ∘ inr)
(inr (k ∸ cutoff , _))
≡⟨⟩
zs (σ .fun (finSubst cutoff+- (finCombine cutoff (m ∸ cutoff) (inr (k ∸ cutoff , _)))))
≡⟨ congS (zs ∘ σ .fun) (Fin-fst-≡ (+-comm cutoff (k ∸ cutoff) ∙ ≤-∸-+-cancel cutoff≤k)) ⟩
zs (σ .fun (k , k<m))
∎)
(k ≤? cutoff)
permuteInvariant : ∀ n (zs : Fin n -> A) (σ : Iso (Fin n) (Fin n)) -> f♯ (n , zs ∘ σ .fun) ≡ f♯ (n , zs)
permuteInvariant zero zs σ =
congS f♯ (Array≡ {f = zs ∘ σ .fun} {g = zs} refl \k k<0 -> ⊥.rec (¬-<-zero k<0))
permuteInvariant (suc zero) zs σ =
congS f♯ (Array≡ {f = zs ∘ σ .fun} {g = zs} refl \k k<1 -> congS zs (isContr→isProp isContrFin1 _ _))
permuteInvariant (suc (suc n)) zs σ =
let τ = swapAut σ ; τ-0≡0 = swapAut0≡0 σ
IH = permuteInvariant (suc n) (zs ∘ fsuc) (punchOutZero τ τ-0≡0)
in
f♯ (suc (suc n) , zs ∘ σ .fun)
≡⟨ sym (swapAutToAut zs σ) ⟩
f♯ (suc (suc n) , zs ∘ τ .fun)
≡⟨ permuteInvariantOnZero τ τ-0≡0 IH ⟩
f♯ (suc (suc n) , zs) ∎
where
permuteInvariantOnZero : (τ : Iso (Fin (suc (suc n))) (Fin (suc (suc n)))) (τ-0≡0 : τ .fun fzero ≡ fzero) -> (IH : _)
-> f♯ (suc (suc n) , zs ∘ τ .fun) ≡ f♯ (suc (suc n) , zs)
permuteInvariantOnZero τ τ-0≡0 IH =
f♯ (suc (suc n) , zs ∘ τ .fun)
≡⟨⟩
f (zs (τ .fun fzero)) 𝔜.⊕ f♯ (suc n , zs ∘ τ .fun ∘ fsuc)
≡⟨ congS (\z -> f (zs z) 𝔜.⊕ f♯ (suc n , zs ∘ τ .fun ∘ fsuc)) (Fin-fst-≡ (congS fst τ-0≡0)) ⟩
f (zs fzero) 𝔜.⊕ f♯ (suc n , zs ∘ τ .fun ∘ fsuc)
≡⟨ congS (\z -> f (zs fzero) 𝔜.⊕ f♯ z)
(Array≡ {f = zs ∘ τ .fun ∘ fsuc} refl \k k≤n ->
congS (zs ∘ τ .fun ∘ fsuc) (Fin-fst-≡ refl) ∙ congS zs (punchOutZero≡fsuc τ τ-0≡0 (k , k≤n))) ⟩
f (zs fzero) 𝔜.⊕ f♯ (suc n , zs ∘ fsuc ∘ punchOutZero τ τ-0≡0 .fun)
≡⟨ cong₂ 𝔜._⊕_ (sym (f♯Eta (zs fzero))) IH ⟩
f♯ (η (zs fzero)) 𝔜.⊕ f♯ (suc n , zs ∘ fsuc)
≡⟨ sym (f♯HomOplus (η (zs fzero)) (suc n , zs ∘ fsuc)) ⟩
f♯ (η (zs fzero) ⊕ (suc n , zs ∘ fsuc))
≡⟨ congS f♯ (η+fsuc zs) ⟩
f♯ (suc (suc n) , zs)
∎
≈Respf♯ : {as bs : Array A} -> as ≈ bs -> f♯ as ≡ f♯ bs
≈Respf♯ {as = n , g} {bs = m , h} (σ , p) =
f♯ (n , g)
≡⟨ congS (λ z -> f♯ (n , z)) p ⟩
f♯ (n , h ∘ σ .fun)
≡⟨ congS f♯ (Array≡ n≡m λ _ _ -> refl) ⟩
f♯ (m , h ∘ σ .fun ∘ (Fin≅ (sym n≡m)) .fun)
≡⟨⟩
f♯ (m , h ∘ (compIso (Fin≅ (sym n≡m)) σ) .fun)
≡⟨ permuteInvariant m h (compIso (Fin≅ (sym n≡m)) σ) ⟩
f♯ (m , h) ∎
where
n≡m : n ≡ m
n≡m = Fin≅-inj σ
module _ {ℓ} (A : Type ℓ) where
open import Cubical.Relation.Binary
module P = BinaryRelation {A = Array A} _≈_
module R = isPermRel
isPermRelPerm : isPermRel arrayDef (_≈_ {A = A})
P.isEquivRel.reflexive (R.isEquivRel isPermRelPerm) _ = refl≈
P.isEquivRel.symmetric (R.isEquivRel isPermRelPerm) _ _ = sym≈
P.isEquivRel.transitive (R.isEquivRel isPermRelPerm) _ _ cs = trans≈ {cs = cs}
R.isCongruence isPermRelPerm {as} {bs} {cs} {ds} p q = cong≈ p q
R.isCommutative isPermRelPerm = comm≈
R.respSharp isPermRelPerm {isSet𝔜 = isSet𝔜} 𝔜-cmon f p = ≈Respf♯ isSet𝔜 𝔜-cmon f p
PermRel : PermRelation arrayDef A
PermRel = _≈_ , isPermRelPerm
module BagDef = F.Definition M.MonSig M.CMonEqSig M.CMonSEq
bagFreeDef : ∀ {ℓ} -> BagDef.Free ℓ ℓ 2
bagFreeDef = qFreeMonDef (PermRel _)