Martin Escardo, November 2019. The swap automorphism. \begin{code} {-# OPTIONS --safe --without-K #-} module Factorial.Swap where open import MLTT.Spartan open import UF.DiscreteAndSeparated open import UF.Equiv \end{code} We change the value of one isolated argument of a function, and no other value, with patch. Recall that a point x:X is called isolated if x=y is decidable for all y:X. \begin{code} module _ {𝓤 𝓥} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (a : X) (b : Y) (i : is-isolated a) (f : X → Y) where private φ : (x : X) → (a = x) + (a ≠ x) → Y φ x (inl p) = b φ x (inr u) = f x f' : X → Y f' x = φ x (i x) γ : (z : (a = a) + (a ≠ a)) → i a = z → φ a z = b γ (inl p) q = refl γ (inr u) q = 𝟘-elim (u refl) δ : (x : X) (u : a ≠ x) (z : (a = x) + (a ≠ x)) → i x = z → φ x z = f x δ x u (inl p) q = 𝟘-elim (u p) δ x u (inr v) q = refl patch : X → Y patch = f' patch-equation₀ : f' a = b patch-equation₀ = γ (i a) refl patch-equation₁ : (x : X) → a ≠ x → f' x = f x patch-equation₁ x u = δ x u (i x) refl \end{code} The (involutive) swap automorphism is obtained by patching the identity function twice: \begin{code} swap : {X : 𝓤 ̇ } (a b : X) → is-isolated a → is-isolated b → X → X swap a b i j = patch a b i (patch b a j id) swap-equation₀ : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → swap a b i j a = b swap-equation₀ a b i j = patch-equation₀ a b i (patch b a j id) swap-equation₁ : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → swap a b i j b = a swap-equation₁ a b i j = γ (j a) where γ : (b = a) + (b ≠ a) → swap a b i j b = a γ (inl r) = swap a b i j b =⟨ ap (swap a b i j) r ⟩ swap a b i j a =⟨ swap-equation₀ a b i j ⟩ b =⟨ r ⟩ a ∎ γ (inr n) = swap a b i j b =⟨ refl ⟩ patch a b i (patch b a j id) b =⟨ patch-equation₁ a b i (patch b a j id) b (≠-sym n) ⟩ patch b a j id b =⟨ patch-equation₀ b a j id ⟩ a ∎ swap-equation₂ : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → (x : X) → a ≠ x → b ≠ x → swap a b i j x = x swap-equation₂ a b i j x m n = swap a b i j x =⟨ refl ⟩ patch a b i (patch b a j id) x =⟨ patch-equation₁ a b i (patch b a j id) x m ⟩ patch b a j id x =⟨ patch-equation₁ b a j id x n ⟩ x ∎ swap-symmetric : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → swap a b i j ∼ swap b a j i swap-symmetric a b i j x = γ (i x) (j x) where γ : (a = x) + (a ≠ x) → (b = x) + (b ≠ x) → swap a b i j x = swap b a j i x γ (inl p) _ = swap a b i j x =⟨ ap (swap a b i j) (p ⁻¹) ⟩ swap a b i j a =⟨ swap-equation₀ a b i j ⟩ b =⟨ (swap-equation₁ b a j i)⁻¹ ⟩ swap b a j i a =⟨ ap (swap b a j i) p ⟩ swap b a j i x ∎ γ (inr _) (inl q) = swap a b i j x =⟨ ap (swap a b i j) (q ⁻¹) ⟩ swap a b i j b =⟨ swap-equation₁ a b i j ⟩ a =⟨ (swap-equation₀ b a j i)⁻¹ ⟩ swap b a j i b =⟨ ap (swap b a j i) q ⟩ swap b a j i x ∎ γ (inr m) (inr n) = swap a b i j x =⟨ swap-equation₂ a b i j x m n ⟩ x =⟨ (swap-equation₂ b a j i x n m)⁻¹ ⟩ swap b a j i x ∎ swap-involutive : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → swap a b i j ∘ swap a b i j ∼ id swap-involutive a b i j x = γ (i x) (j x) where γ : (a = x) + (a ≠ x) → (b = x) + (b ≠ x) → swap a b i j (swap a b i j x) = x γ (inl p) _ = swap a b i j (swap a b i j x) =⟨ ap (λ - → swap a b i j (swap a b i j -)) (p ⁻¹) ⟩ swap a b i j (swap a b i j a) =⟨ ap (swap a b i j) (swap-equation₀ a b i j) ⟩ swap a b i j b =⟨ swap-equation₁ a b i j ⟩ a =⟨ p ⟩ x ∎ γ (inr _) (inl q) = swap a b i j (swap a b i j x) =⟨ ap (λ - → swap a b i j (swap a b i j -)) (q ⁻¹) ⟩ swap a b i j (swap a b i j b) =⟨ ap (swap a b i j) (swap-equation₁ a b i j) ⟩ swap a b i j a =⟨ swap-equation₀ a b i j ⟩ b =⟨ q ⟩ x ∎ γ (inr m) (inr n) = swap a b i j (swap a b i j x) =⟨ ap (swap a b i j) (swap-equation₂ a b i j x m n) ⟩ swap a b i j x =⟨ swap-equation₂ a b i j x m n ⟩ x ∎ swap-is-equiv : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → is-equiv (swap a b i j) swap-is-equiv a b i j = qinvs-are-equivs (swap a b i j) (swap a b i j , (swap-involutive a b i j , swap-involutive a b i j)) ≃-swap : {X : 𝓤 ̇ } (a b : X) (i : is-isolated a) (j : is-isolated b) → X ≃ X ≃-swap a b i j = swap a b i j , swap-is-equiv a b i j \end{code}