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)