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}