Transpositions of standard finite types

{-# OPTIONS --lossy-unification #-}
module finite-group-theory.transpositions-standard-finite-types where
Imports
open import univalent-combinatorics.standard-finite-types
open import univalent-combinatorics.equality-standard-finite-types

open import elementary-number-theory.natural-numbers
open import elementary-number-theory.inequality-natural-numbers

open import foundation.automorphisms
open import foundation.universe-levels
open import foundation.dependent-pair-types
open import foundation.coproduct-types
open import foundation.unit-type
open import foundation.equivalences
open import foundation.identity-types
open import foundation.negation
open import foundation.homotopies
open import foundation.functions
open import foundation.empty-types
open import foundation.functoriality-coproduct-types
open import foundation.equivalence-extensionality
open import foundation.propositions

open import lists.lists
open import lists.functoriality-lists
open import lists.flattening-lists

open import finite-group-theory.permutations-standard-finite-types
open import finite-group-theory.transpositions

Idea

Given i and j in Fin n, the transposition associated to i and j swap these two elements.

Definitions

Transpositions on Fin n

This definition uses the standard-transposition in finite-group-theory.transposition.

module _
  (n : ) (i j : Fin n) (neq : ¬ (i  j))
  where

  transposition-Fin : Permutation n
  transposition-Fin = standard-transposition (has-decidable-equality-Fin n) neq

  map-transposition-Fin : Fin n  Fin n
  map-transposition-Fin =
    map-standard-transposition (has-decidable-equality-Fin n) neq

  left-computation-transposition-Fin :
    map-standard-transposition (has-decidable-equality-Fin n) neq i  j
  left-computation-transposition-Fin =
    left-computation-standard-transposition (has-decidable-equality-Fin n) neq

  right-computation-transposition-Fin :
    map-standard-transposition (has-decidable-equality-Fin n) neq j  i
  right-computation-transposition-Fin =
    right-computation-standard-transposition (has-decidable-equality-Fin n) neq

  is-fixed-point-transposition-Fin :
    (z : Fin n) 
    ¬ (i  z) 
    ¬ (j  z) 
    map-standard-transposition (has-decidable-equality-Fin n) neq z  z
  is-fixed-point-transposition-Fin =
    is-fixed-point-standard-transposition (has-decidable-equality-Fin n) neq

The transposition that swaps the two last elements of Fin (succ-ℕ (succ-ℕ n))

We define directly the transposition of Fin (succ-ℕ (succ-ℕ n)) that exchanges the two elements associated to n and succ-ℕ n.

module _
  (n : )
  where

  map-swap-two-last-elements-transposition-Fin :
    Fin (succ-ℕ (succ-ℕ n))  Fin (succ-ℕ (succ-ℕ n))
  map-swap-two-last-elements-transposition-Fin (inl (inl x)) = inl (inl x)
  map-swap-two-last-elements-transposition-Fin (inl (inr star)) = inr star
  map-swap-two-last-elements-transposition-Fin (inr star) = inl (inr star)

  is-involution-map-swap-two-last-elements-transposition-Fin :
    ( map-swap-two-last-elements-transposition-Fin 
      map-swap-two-last-elements-transposition-Fin) ~
    id
  is-involution-map-swap-two-last-elements-transposition-Fin (inl (inl x)) =
    refl
  is-involution-map-swap-two-last-elements-transposition-Fin (inl (inr star)) =
    refl
  is-involution-map-swap-two-last-elements-transposition-Fin (inr star) = refl

  swap-two-last-elements-transposition-Fin : Permutation (succ-ℕ (succ-ℕ n))
  pr1 swap-two-last-elements-transposition-Fin =
    map-swap-two-last-elements-transposition-Fin
  pr2 swap-two-last-elements-transposition-Fin =
    is-equiv-has-inverse
      map-swap-two-last-elements-transposition-Fin
      is-involution-map-swap-two-last-elements-transposition-Fin
      is-involution-map-swap-two-last-elements-transposition-Fin

We show that this definiton is an instance of the previous one.

  cases-htpy-swap-two-last-elements-transposition-Fin :
    (x : Fin (succ-ℕ (succ-ℕ n))) 
    (x  neg-one-Fin (succ-ℕ n)) + (¬ (x  neg-one-Fin (succ-ℕ n))) 
    (x  neg-two-Fin (succ-ℕ n)) + (¬ (x  neg-two-Fin (succ-ℕ n))) 
    map-swap-two-last-elements-transposition-Fin x 
    map-transposition-Fin
      ( succ-ℕ (succ-ℕ n))
      ( neg-two-Fin (succ-ℕ n))
      ( neg-one-Fin (succ-ℕ n))
      ( neq-inl-inr)
      ( x)
  cases-htpy-swap-two-last-elements-transposition-Fin _ (inl refl) _ =
    inv
      ( right-computation-transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( neg-two-Fin (succ-ℕ n))
        ( neg-one-Fin (succ-ℕ n))
        ( neq-inl-inr))
  cases-htpy-swap-two-last-elements-transposition-Fin _ (inr p) (inl refl) =
    inv
      ( left-computation-transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( neg-two-Fin (succ-ℕ n))
        ( neg-one-Fin (succ-ℕ n))
        ( neq-inl-inr))
  cases-htpy-swap-two-last-elements-transposition-Fin
    ( inl (inl x))
    ( inr p)
    ( inr q) =
     inv
      ( is-fixed-point-transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( neg-two-Fin (succ-ℕ n))
        ( neg-one-Fin (succ-ℕ n))
        ( neq-inl-inr)
        ( inl (inl x))
        ( q  inv)
        ( p  inv))
  cases-htpy-swap-two-last-elements-transposition-Fin
    ( inl (inr star))
    ( inr p)
    ( inr q) = ex-falso (q refl)
  cases-htpy-swap-two-last-elements-transposition-Fin
    ( inr star)
    ( inr p)
    ( inr q) = ex-falso (p refl)

  htpy-swap-two-last-elements-transposition-Fin :
    htpy-equiv
      ( swap-two-last-elements-transposition-Fin)
      ( transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( neg-two-Fin (succ-ℕ n))
        ( neg-one-Fin (succ-ℕ n))
        ( neq-inl-inr))
  htpy-swap-two-last-elements-transposition-Fin x =
    cases-htpy-swap-two-last-elements-transposition-Fin
      ( x)
      ( has-decidable-equality-Fin
        ( succ-ℕ (succ-ℕ n))
        ( x)
        ( neg-one-Fin (succ-ℕ n)))
      ( has-decidable-equality-Fin
        ( succ-ℕ (succ-ℕ n))
        ( x)
        ( neg-two-Fin (succ-ℕ n)))

Transpositions of a pair of adjacent elements in Fin (succ-ℕ n)

Definition using swap-two-last-elements-transposition-Fin

adjacent-transposition-Fin :
  (n : )  (k : Fin n) 
  Permutation (succ-ℕ n)
adjacent-transposition-Fin (succ-ℕ n) (inl x) =
  equiv-coprod (adjacent-transposition-Fin n x) id-equiv
adjacent-transposition-Fin (succ-ℕ n) (inr x) =
  swap-two-last-elements-transposition-Fin n

map-adjacent-transposition-Fin :
  (n : )  (k : Fin n) 
  (Fin (succ-ℕ n)  Fin (succ-ℕ n))
map-adjacent-transposition-Fin n k = map-equiv (adjacent-transposition-Fin n k)

adjacent-transposition-Fin is an instance of the definiton transposition-Fin

cases-htpy-map-coprod-map-transposition-id-Fin :
  (n : )  (k l : Fin n)  (neq : ¬ (k  l)) 
  (x : Fin (succ-ℕ n)) 
  (x  inl-Fin n k) + ¬ (x  inl-Fin n k) 
  (x  inl-Fin n l) + ¬ (x  inl-Fin n l) 
  map-coprod (map-transposition-Fin n k l neq) id x 
  map-transposition-Fin
    ( succ-ℕ n)
    ( inl-Fin n k)
    ( inl-Fin n l)
    ( neq  is-injective-inl-Fin n)
    ( x)
cases-htpy-map-coprod-map-transposition-id-Fin n k l neq x (inl refl) _ =
  ( ( ap
      ( inl-Fin n)
      ( left-computation-transposition-Fin n k l neq)) 
    ( inv
      ( left-computation-transposition-Fin
        ( succ-ℕ n)
        ( inl-Fin n k)
        ( inl-Fin n l)
        ( neq  is-injective-inl-Fin n))))
cases-htpy-map-coprod-map-transposition-id-Fin
  ( n)
  ( k)
  ( l)
  ( neq)
  ( x)
  ( inr _)
  ( inl refl) =
  ( ( ap
      ( inl-Fin n)
      ( right-computation-transposition-Fin n k l neq)) 
    ( inv
       ( right-computation-transposition-Fin
         ( succ-ℕ n)
         ( inl-Fin n k)
         ( inl-Fin n l)
         ( neq  is-injective-inl-Fin n))))
cases-htpy-map-coprod-map-transposition-id-Fin
  ( n)
  ( k)
  ( l)
  ( neq)
  ( inl x)
  ( inr neqk)
  ( inr neql) =
  ( ( ap
      ( inl-Fin n)
      ( is-fixed-point-transposition-Fin
        ( n)
        ( k)
        ( l)
        ( neq)
        ( x)
        ( neqk  (inv  ap (inl-Fin n)))
        ( neql  (inv  ap (inl-Fin n))))) 
    ( inv
      ( is-fixed-point-transposition-Fin
        ( succ-ℕ n)
        ( inl-Fin n k)
        ( inl-Fin n l)
        ( neq  is-injective-inl-Fin n)
        ( inl x)
        ( neqk  inv)
        ( neql  inv))))
cases-htpy-map-coprod-map-transposition-id-Fin
  ( n)
  ( k)
  ( l)
  ( neq)
  ( inr star)
  ( inr neqk)
  ( inr neql) =
  inv
    ( is-fixed-point-transposition-Fin
      ( succ-ℕ n)
      ( inl-Fin n k)
      ( inl-Fin n l)
      ( neq  is-injective-inl-Fin n)
      ( inr star)
      ( neqk  inv)
      ( neql  inv))

htpy-map-coprod-map-transposition-id-Fin :
  (n : )  (k l : Fin n)  (neq : ¬ (k  l)) 
  htpy-equiv
    ( equiv-coprod (transposition-Fin n k l neq) id-equiv)
    ( transposition-Fin
      ( succ-ℕ n)
      ( inl-Fin n k)
      ( inl-Fin n l)
      ( neq  is-injective-inl-Fin n))
htpy-map-coprod-map-transposition-id-Fin n k l neq x =
  cases-htpy-map-coprod-map-transposition-id-Fin
    ( n)
    ( k)
    ( l)
    ( neq)
    ( x)
    ( has-decidable-equality-Fin (succ-ℕ n) x (inl-Fin n k))
    ( has-decidable-equality-Fin (succ-ℕ n) x (inl-Fin n l))

helper-htpy-same-transposition-Fin :
  (n : ) (k l : Fin n) (neq1 : ¬ (k  l)) (neq2 : ¬ (k  l)) 
  (neq1  neq2) 
  htpy-equiv
    ( transposition-Fin n k l neq1)
    ( transposition-Fin n k l neq2)
helper-htpy-same-transposition-Fin n k l neq1 .neq1 refl = refl-htpy

htpy-same-transposition-Fin :
  {n : } {k l : Fin n} {neq1 : ¬ (k  l)} {neq2 : ¬ (k  l)} 
  htpy-equiv
    ( transposition-Fin n k l neq1)
    ( transposition-Fin n k l neq2)
htpy-same-transposition-Fin {n} {k} {l} {neq1} {neq2} =
  helper-htpy-same-transposition-Fin n k l neq1 neq2 (eq-is-prop is-prop-neg)

htpy-adjacent-transposition-Fin :
  (n : )  (k : Fin n) 
  htpy-equiv
    ( adjacent-transposition-Fin n k)
    ( transposition-Fin
      ( succ-ℕ n)
      ( inl-Fin n k)
      ( inr-Fin n k)
      ( neq-inl-Fin-inr-Fin n k))
htpy-adjacent-transposition-Fin (succ-ℕ n) (inl x) =
  ( ( htpy-map-coprod (htpy-adjacent-transposition-Fin n x) refl-htpy) ∙h
    ( ( htpy-map-coprod-map-transposition-id-Fin
        ( succ-ℕ n)
        ( inl-Fin n x)
        ( inr-Fin n x)
        ( neq-inl-Fin-inr-Fin n x)) ∙h
      ( htpy-same-transposition-Fin)))
htpy-adjacent-transposition-Fin (succ-ℕ n) (inr star) =
  htpy-swap-two-last-elements-transposition-Fin n

Properties

The transposition associated to i and j is homotopic to the one associated with j and i

cases-htpy-transposition-Fin-transposition-swap-Fin :
  (n : )  (i j : Fin n)  (neq : ¬ (i  j))  (x : Fin n) 
  (x  i) + ¬ (x  i) 
  (x  j) + ¬ (x  j) 
  map-transposition-Fin n i j neq x 
  map-transposition-Fin n j i (neq  inv) x
cases-htpy-transposition-Fin-transposition-swap-Fin
  ( n)
  ( i)
  ( j)
  ( neq)
  ( .i)
  ( inl refl) _ =
  left-computation-transposition-Fin n i j neq 
  inv (right-computation-transposition-Fin n j i (neq  inv))
cases-htpy-transposition-Fin-transposition-swap-Fin
  ( n)
  ( i)
  ( j)
  ( neq)
  ( .j)
  ( inr _)
  ( inl refl) =
  right-computation-transposition-Fin n i j neq 
  inv (left-computation-transposition-Fin n j i (neq  inv))
cases-htpy-transposition-Fin-transposition-swap-Fin
  ( n)
  ( i)
  ( j)
  ( neq)
  ( x)
  ( inr neqi)
  ( inr neqj) =
  is-fixed-point-transposition-Fin
    ( n)
    ( i)
    ( j)
    ( neq)
    ( x)
    ( neqi  inv)
    ( neqj  inv) 
  inv
    (is-fixed-point-transposition-Fin
      ( n)
      ( j)
      ( i)
      ( neq  inv)
      ( x)
      ( neqj  inv)
      ( neqi  inv))

htpy-transposition-Fin-transposition-swap-Fin :
  (n : )  (i j : Fin n)  (neq : ¬ (i  j)) 
  htpy-equiv
    ( transposition-Fin n i j neq)
    ( transposition-Fin n j i (neq  inv))
htpy-transposition-Fin-transposition-swap-Fin n i j neq x =
  cases-htpy-transposition-Fin-transposition-swap-Fin
    ( n)
    ( i)
    ( j)
    ( neq)
    ( x)
    ( has-decidable-equality-Fin n x i)
    ( has-decidable-equality-Fin n x j)

The conjugate of a transposition is also a transposition

htpy-conjugate-transposition-Fin :
  (n : ) (x y z : Fin n)
  (neqxy : ¬ (x  y))
  (neqyz : ¬ (y  z))
  (neqxz : ¬ (x  z)) 
  htpy-equiv
    ( transposition-Fin n y z neqyz ∘e
      ( transposition-Fin n x y neqxy ∘e
        transposition-Fin n y z neqyz))
    ( transposition-Fin n x z neqxz)
htpy-conjugate-transposition-Fin n x y z neqxy neqyz neqxz =
  htpy-conjugate-transposition
   ( has-decidable-equality-Fin n)
   ( neqxy)
   ( neqyz)
   ( neqxz)

private
  htpy-whisk-conjugate :
    {l1 : Level} {A : UU l1} {f f' : A  A} (g : A  A) 
    (f ~ f')  (f  (g  f)) ~ (f'  (g  f'))
  htpy-whisk-conjugate {f = f} {f' = f'} g H x =
    H (g ( f x))  ap (f'  g) (H x)

  htpy-whisk :
    {l : Level} {A : UU l} (f : A  A) {g g' : A  A} 
    g ~ g'  (f  (g  f)) ~ (f  (g'  f))
  htpy-whisk f H x = ap f (H (f x))

htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin :
  (n : ) (x : Fin (succ-ℕ n)) (neq : ¬ (x  neg-one-Fin n)) 
  htpy-equiv
    ( swap-two-last-elements-transposition-Fin n ∘e
      ( transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( inl-Fin (succ-ℕ n) x)
        ( neg-two-Fin (succ-ℕ n))
        ( neq  is-injective-inl-Fin (succ-ℕ n)) ∘e
        swap-two-last-elements-transposition-Fin n))
    ( transposition-Fin
      ( succ-ℕ (succ-ℕ n))
      ( inl-Fin (succ-ℕ n) x)
      ( neg-one-Fin (succ-ℕ n))
      ( neq-inl-inr))
htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin n x neq =
  ( ( htpy-whisk-conjugate
        ( map-transposition-Fin
          ( succ-ℕ (succ-ℕ n))
          ( inl-Fin (succ-ℕ n) x)
          ( neg-two-Fin (succ-ℕ n))
          ( neq  is-injective-inl-Fin (succ-ℕ n)))
        ( htpy-swap-two-last-elements-transposition-Fin n)) ∙h
    ( ( htpy-conjugate-transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( inl-Fin (succ-ℕ n) x)
        ( neg-two-Fin (succ-ℕ n))
        ( neg-one-Fin (succ-ℕ n))
        ( neq  is-injective-inl-Fin (succ-ℕ n))
        ( neq-inl-inr)
        ( neq-inl-inr))))

htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin' :
  (n : ) (x : Fin (succ-ℕ n)) (neq : ¬ (x  neg-one-Fin n)) 
  htpy-equiv
    ( swap-two-last-elements-transposition-Fin n ∘e
      ( transposition-Fin
        ( succ-ℕ (succ-ℕ n))
        ( neg-two-Fin (succ-ℕ n))
        ( inl-Fin (succ-ℕ n) x)
        ( neq  (is-injective-inl-Fin (succ-ℕ n)  inv)) ∘e
        swap-two-last-elements-transposition-Fin n))
    ( transposition-Fin
      ( succ-ℕ (succ-ℕ n))
      ( neg-one-Fin (succ-ℕ n))
      ( inl-Fin (succ-ℕ n) x)
      ( neq-inr-inl))
htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin' n x neq =
  ( ( htpy-whisk
      ( map-swap-two-last-elements-transposition-Fin n)
      ( ( htpy-transposition-Fin-transposition-swap-Fin
          ( succ-ℕ (succ-ℕ n))
          ( neg-two-Fin (succ-ℕ n))
          ( inl-Fin (succ-ℕ n) x)
          ( neq  (is-injective-inl-Fin (succ-ℕ n)  inv))) ∙h
        htpy-same-transposition-Fin)) ∙h
      ( ( htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin
          ( n)
          ( x)
          ( neq) ∙h
        ( ( htpy-transposition-Fin-transposition-swap-Fin
            ( succ-ℕ (succ-ℕ n))
            ( inl-Fin (succ-ℕ n) x)
            ( neg-one-Fin (succ-ℕ n))
            ( neq-inl-inr)) ∙h
          htpy-same-transposition-Fin))))

Every transposition is the composition of a list of adjacent transpositions

list-adjacent-transpositions-transposition-Fin :
  (n : )  (i j : Fin (succ-ℕ n)) 
  list (Fin n)
list-adjacent-transpositions-transposition-Fin n (inr _) (inr _) = nil
list-adjacent-transpositions-transposition-Fin 0 (inl _) (inr _) = nil
list-adjacent-transpositions-transposition-Fin 0 (inl _) (inl _) = nil
list-adjacent-transpositions-transposition-Fin 0 (inr _) (inl _) = nil
list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inl i)
  ( inl j) =
  map-list (inl-Fin n) (list-adjacent-transpositions-transposition-Fin n i j)
list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inl (inr star))
  ( inr star) = cons (inr star) nil
list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inl (inl i))
  ( inr star) =
  snoc
    ( cons
      ( inr star)
      ( map-list
        ( inl-Fin n)
        ( list-adjacent-transpositions-transposition-Fin n (inl i) (inr star))))
    ( inr star)
list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inr star)
  ( inl (inl j)) =
  snoc
    ( cons
      ( inr star)
      ( map-list
        ( inl-Fin n)
        ( list-adjacent-transpositions-transposition-Fin n (inr star) (inl j))))
    ( inr star)
list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inr star)
  ( inl (inr star)) = cons (inr star) nil

permutation-list-adjacent-transpositions :
  (n : )  list (Fin n)  Permutation (succ-ℕ n)
permutation-list-adjacent-transpositions n nil = id-equiv
permutation-list-adjacent-transpositions n (cons x l) =
  adjacent-transposition-Fin n x ∘e
  permutation-list-adjacent-transpositions n l

map-permutation-list-adjacent-transpositions :
  (n : )  list (Fin n)  Fin (succ-ℕ n)  Fin (succ-ℕ n)
map-permutation-list-adjacent-transpositions n l =
  map-equiv (permutation-list-adjacent-transpositions n l)

htpy-permutation-inl-list-adjacent-transpositions :
  (n : )  (l : list (Fin n)) 
  htpy-equiv
    ( permutation-list-adjacent-transpositions
      ( succ-ℕ n)
      ( map-list (inl-Fin n) l))
    ( equiv-coprod
      ( permutation-list-adjacent-transpositions n l)
      ( id-equiv))
htpy-permutation-inl-list-adjacent-transpositions n nil =
  inv-htpy (id-map-coprod (Fin (succ-ℕ n)) unit)
htpy-permutation-inl-list-adjacent-transpositions n (cons x l) =
   ( ( map-coprod (map-adjacent-transposition-Fin n x) id ·l
       htpy-permutation-inl-list-adjacent-transpositions n l) ∙h
     ( ( inv-htpy
         ( preserves-comp-map-coprod
           ( map-permutation-list-adjacent-transpositions n l)
           ( map-adjacent-transposition-Fin n x)
           ( id)
           ( id)))))

htpy-permutation-snoc-list-adjacent-transpositions :
  (n : ) (l : list (Fin n)) (x : Fin n) 
  htpy-equiv
    ( permutation-list-adjacent-transpositions n (snoc l x))
    ( permutation-list-adjacent-transpositions n l ∘e
      adjacent-transposition-Fin n x)
htpy-permutation-snoc-list-adjacent-transpositions n nil x = refl-htpy
htpy-permutation-snoc-list-adjacent-transpositions n (cons y l) x =
  map-adjacent-transposition-Fin n y ·l
  htpy-permutation-snoc-list-adjacent-transpositions n l x

htpy-permutation-list-adjacent-transpositions-transposition-Fin :
  (n : ) (i j : Fin (succ-ℕ n)) (neq : ¬ (i  j))→
  htpy-equiv
    ( permutation-list-adjacent-transpositions
      ( n)
      ( list-adjacent-transpositions-transposition-Fin n i j))
    ( transposition-Fin (succ-ℕ n) i j neq)
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( 0)
  ( inr star)
  ( inr star)
  ( neq) = ex-falso (neq refl)
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inl i)
  ( inl j)
  ( neq) =
  ( ( htpy-permutation-inl-list-adjacent-transpositions
      ( n)
      ( list-adjacent-transpositions-transposition-Fin n i j)) ∙h
    ( ( htpy-map-coprod
        ( htpy-permutation-list-adjacent-transpositions-transposition-Fin
          ( n)
          ( i)
          ( j)
          ( neq  (ap (inl-Fin (succ-ℕ n)))))
        ( refl-htpy)) ∙h
      ( ( htpy-map-coprod-map-transposition-id-Fin
          ( succ-ℕ n)
          ( i)
          ( j)
          ( neq  ap (inl-Fin (succ-ℕ n)))) ∙h
        ( htpy-same-transposition-Fin))))
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inl (inl i))
  ( inr star)
  ( neq) =
  ( ( map-swap-two-last-elements-transposition-Fin n ·l
      htpy-permutation-snoc-list-adjacent-transpositions
        ( succ-ℕ n)
        ( map-list
          ( inl-Fin n)
          ( list-adjacent-transpositions-transposition-Fin
            ( n)
            ( inl i)
            ( inr star)))
        ( inr star)) ∙h
    ( ( htpy-whisk
        ( map-swap-two-last-elements-transposition-Fin n)
        ( ( htpy-permutation-inl-list-adjacent-transpositions
            ( n)
            ( list-adjacent-transpositions-transposition-Fin
              ( n)
              ( inl i)
              ( inr star))) ∙h
          ( htpy-map-coprod
            ( htpy-permutation-list-adjacent-transpositions-transposition-Fin
              ( n)
              ( inl i)
              ( inr star)
              ( neq-inl-inr))
            ( refl-htpy) ∙h
            htpy-map-coprod-map-transposition-id-Fin
              ( succ-ℕ n)
              ( inl i)
              ( inr star)
              ( neq-inl-inr)))) ∙h
        ( htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin
          ( n)
          ( inl i)
          ( neq-inl-inr) ∙h
          htpy-same-transposition-Fin)))
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inl (inr star))
  ( inr star)
  ( neq) =
  htpy-swap-two-last-elements-transposition-Fin n ∙h
  htpy-same-transposition-Fin
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inr star)
  ( inl (inl j))
  ( neq) =
  ( ( map-swap-two-last-elements-transposition-Fin n ·l
      htpy-permutation-snoc-list-adjacent-transpositions
        ( succ-ℕ n)
        ( map-list
          ( inl-Fin n)
          ( list-adjacent-transpositions-transposition-Fin
            ( n)
            ( inr star)
            ( inl j)))
        ( inr star)) ∙h
    ( ( htpy-whisk
        ( map-swap-two-last-elements-transposition-Fin n)
        ( ( htpy-permutation-inl-list-adjacent-transpositions
            ( n)
            ( list-adjacent-transpositions-transposition-Fin
              ( n)
              ( inr star)
              ( inl j))) ∙h
          ( ( htpy-map-coprod
              ( htpy-permutation-list-adjacent-transpositions-transposition-Fin
                ( n)
                ( inr star)
                ( inl j)
                ( neq-inr-inl))
              ( refl-htpy)) ∙h
            ( ( htpy-map-coprod-map-transposition-id-Fin
                ( succ-ℕ n)
                ( inr star)
                ( inl j)
                ( neq-inr-inl)) ∙h
              ( htpy-same-transposition-Fin))))) ∙h
      ( ( htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin'
          ( n)
          ( inl j)
          ( neq-inl-inr)) ∙h
        htpy-same-transposition-Fin)))
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inr star)
  ( inl (inr star))
  ( neq) =
  htpy-swap-two-last-elements-transposition-Fin n ∙h
  ( ( htpy-transposition-Fin-transposition-swap-Fin
      ( succ-ℕ (succ-ℕ n))
      ( neg-two-Fin (succ-ℕ n))
      ( neg-one-Fin (succ-ℕ n))
      ( neq-inl-inr)) ∙h
    htpy-same-transposition-Fin)
htpy-permutation-list-adjacent-transpositions-transposition-Fin
  ( succ-ℕ n)
  ( inr star)
  ( inr star)
  ( neq) = ex-falso (neq refl)