Transpositions

module finite-group-theory.transpositions where
Imports
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.well-ordering-principle-standard-finite-types

open import foundation.automorphisms
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-propositions
open import foundation.decidable-subtypes
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.equivalences-maybe
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.involutions
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type
open import foundation.univalence
open import foundation.universe-levels

open import lists.concatenation-lists
open import lists.functoriality-lists
open import lists.lists

open import univalent-combinatorics.2-element-decidable-subtypes
open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

Transpositions are permutations that swap two elements.

Definitions

Transpositions

module _
  {l1 l2 : Level} {X : UU l1} (P : 2-Element-Decidable-Subtype l2 X)
  where

  map-transposition'' :
    Σ X  x  is-decidable (is-in-2-Element-Decidable-Subtype P x)) 
    Σ X  x  is-decidable (is-in-2-Element-Decidable-Subtype P x))
  pr1 (map-transposition'' (pair x (inl p))) =
    pr1 (map-swap-2-Element-Decidable-Subtype P (pair x p))
  pr2 (map-transposition'' (pair x (inl p))) =
    inl (pr2 (map-swap-2-Element-Decidable-Subtype P (pair x p)))
  pr1 (map-transposition'' (pair x (inr np))) = x
  pr2 (map-transposition'' (pair x (inr np))) = inr np

  map-transposition' :
    (x : X) (d : is-decidable (is-in-2-Element-Decidable-Subtype P x))  X
  map-transposition' x (inl p) =
    pr1 (map-swap-2-Element-Decidable-Subtype P (pair x p))
  map-transposition' x (inr np) = x

  map-transposition : X  X
  map-transposition x =
    map-transposition' x
      ( is-decidable-subtype-subtype-2-Element-Decidable-Subtype P x)

  preserves-subtype-map-transposition :
    (x : X)  is-in-2-Element-Decidable-Subtype P x 
    is-in-2-Element-Decidable-Subtype P (map-transposition x)
  preserves-subtype-map-transposition x p =
    tr
      ( λ R  is-in-2-Element-Decidable-Subtype P (map-transposition' x R))
      { x = inl p}
      { y = is-decidable-subtype-subtype-2-Element-Decidable-Subtype P x}
      ( eq-is-prop
        ( is-prop-is-decidable
          ( is-prop-is-in-2-Element-Decidable-Subtype P x)))
      ( pr2
        ( map-swap-2-Element-Type
          ( 2-element-type-2-Element-Decidable-Subtype P)
          ( pair x p)))

  is-involution-map-transposition' :
    (x : X) (d : is-decidable (is-in-2-Element-Decidable-Subtype P x))
    (d' : is-decidable
          ( is-in-2-Element-Decidable-Subtype P (map-transposition' x d))) 
    Id (map-transposition' (map-transposition' x d) d') x
  is-involution-map-transposition' x (inl p) (inl p') =
    ( ap
      ( λ y  map-transposition' (map-transposition' x (inl p)) (inl y))
      ( eq-is-in-2-Element-Decidable-Subtype P)) 
    ( ap
      ( pr1)
      ( is-involution-aut-2-element-type
        ( 2-element-type-2-Element-Decidable-Subtype P)
        ( swap-2-Element-Decidable-Subtype P)
        ( pair x p)))
  is-involution-map-transposition' x (inl p) (inr np') =
    ex-falso (np' (pr2 (map-swap-2-Element-Decidable-Subtype P (pair x p))))
  is-involution-map-transposition' x (inr np) (inl p') = ex-falso (np p')
  is-involution-map-transposition' x (inr np) (inr np') = refl

  is-involution-map-transposition : is-involution map-transposition
  is-involution-map-transposition x =
    is-involution-map-transposition' x
      ( is-decidable-subtype-subtype-2-Element-Decidable-Subtype P x)
      ( is-decidable-subtype-subtype-2-Element-Decidable-Subtype P
        ( map-transposition' x
          ( is-decidable-subtype-subtype-2-Element-Decidable-Subtype P x)))

  is-equiv-map-transposition : is-equiv map-transposition
  is-equiv-map-transposition =
    is-equiv-is-involution is-involution-map-transposition

  transposition : X  X
  pr1 transposition = map-transposition
  pr2 transposition = is-equiv-map-transposition

module _
  {l1 l2 : Level} {X : UU l1}
  where

  is-transposition-permutation-Prop : X  X  Prop (l1  lsuc l2)
  is-transposition-permutation-Prop f =
    trunc-Prop (fib (transposition {l2 = l2}) f)

  is-transposition-permutation : X  X  UU (l1  lsuc l2)
  is-transposition-permutation f =
    type-Prop (is-transposition-permutation-Prop f)

  is-prop-is-transposition-permutation :
    (f : X  X)  is-prop (is-transposition-permutation f)
  is-prop-is-transposition-permutation f =
    is-prop-type-Prop (is-transposition-permutation-Prop f)

The standard transposition obtained from a pair of distinct points

module _
  {l : Level} {X : UU l} (H : has-decidable-equality X)
  {x y : X} (p : ¬ (Id x y))
  where

  standard-transposition : Aut X
  standard-transposition =
    transposition (standard-2-Element-Decidable-Subtype H p)

  map-standard-transposition : X  X
  map-standard-transposition = map-equiv standard-transposition

  abstract
    left-computation-standard-transposition :
      Id (map-standard-transposition x) y
    left-computation-standard-transposition
      with is-decidable-type-prop-standard-2-Element-Decidable-Subtype H p x
    ... | inl pp =
      ap
        pr1
        ( compute-swap-2-Element-Type
          ( 2-element-type-standard-2-Element-Decidable-Subtype H p)
          ( pair x pp)
          ( pair y (inr refl))
          ( λ q  p (ap pr1 q)))
    ... | inr np = ex-falso (np (inl refl))

  abstract
    right-computation-standard-transposition :
      Id (map-standard-transposition y) x
    right-computation-standard-transposition
      with is-decidable-type-prop-standard-2-Element-Decidable-Subtype H p y
    ... | inl pp =
      ap
        pr1
        ( compute-swap-2-Element-Type
          ( 2-element-type-standard-2-Element-Decidable-Subtype H p)
          ( pair y pp)
          ( pair x (inl refl))
          ( λ q  p (ap pr1 (inv q))))
    ... | inr np = ex-falso (np (inr refl))

  abstract
    is-fixed-point-standard-transposition :
      (z : X)  ¬ (Id x z)  ¬ (Id y z) 
      Id (map-standard-transposition z) z
    is-fixed-point-standard-transposition z q r
      with is-decidable-type-prop-standard-2-Element-Decidable-Subtype H p z
    ... | inl (inl h) = ex-falso (q h)
    ... | inl (inr h) = ex-falso (r h)
    ... | inr np = refl

The permutation obtained from a list of transpositions

module _
  {l1 l2 : Level} {X : UU l1}
  where

  permutation-list-transpositions :
    ( list (2-Element-Decidable-Subtype l2 X))  Aut X
  permutation-list-transpositions =
    fold-list id-equiv  P e  (transposition P) ∘e e)

  -- !! Why not a homotopy?
  eq-concat-permutation-list-transpositions :
    (l l' : list (2-Element-Decidable-Subtype l2 X)) 
    Id ( ( permutation-list-transpositions l) ∘e
         ( permutation-list-transpositions l'))
       ( permutation-list-transpositions (concat-list l l'))
  eq-concat-permutation-list-transpositions nil l' = eq-htpy-equiv refl-htpy
  eq-concat-permutation-list-transpositions (cons P l) l' =
    eq-htpy-equiv
      ( λ x 
        ap ( map-equiv (transposition P))
           ( htpy-eq-equiv (eq-concat-permutation-list-transpositions l l') x))

Properties

A transposition is not the identity equivalence

module _
  {l1 l2 : Level} {X : UU l1} (P : 2-Element-Decidable-Subtype l2 X)
  where

  abstract
    is-not-identity-map-transposition : Id (map-transposition P) id  empty
    is-not-identity-map-transposition f =
      is-not-identity-swap-2-Element-Type
        ( 2-element-type-2-Element-Decidable-Subtype P)
        ( eq-htpy-equiv
          ( λ { (pair x p) 
                eq-pair-Σ
                  ( ( ap
                      ( map-transposition' P x)
                      ( eq-is-prop
                        ( is-prop-is-decidable
                          ( is-prop-is-in-2-Element-Decidable-Subtype P x))
                          { y =
                            is-decidable-subtype-subtype-2-Element-Decidable-Subtype
                              ( P)
                              ( x)})) 
                    ( htpy-eq f x))
                  ( eq-is-in-2-Element-Decidable-Subtype P)}))

Any transposition on a type equipped with a counting is a standard transposition

module _
  {l : Level} {X : UU l} (eX : count X)
  (Y : 2-Element-Decidable-Subtype l X)
  where

  element-is-not-identity-map-transposition :
    Σ X  x  ¬ (Id (map-transposition Y x) x))
  element-is-not-identity-map-transposition =
    exists-not-not-forall-count
      ( λ z  Id (map-transposition Y z) z)
      ( λ x  has-decidable-equality-count eX (map-transposition Y x) x)
      ( eX)
      ( λ H  is-not-identity-map-transposition Y (eq-htpy H))

  two-elements-transposition :
    Σ ( X)
      ( λ x 
        Σ ( X)
          ( λ y 
            Σ ( ¬ (Id x y))
              ( λ np 
                Id ( standard-2-Element-Decidable-Subtype
                     ( has-decidable-equality-count eX)
                     ( np))
                   ( Y))))
  pr1 two-elements-transposition =
    pr1 element-is-not-identity-map-transposition
  pr1 (pr2 two-elements-transposition) =
    map-transposition Y (pr1 element-is-not-identity-map-transposition)
  pr1 (pr2 (pr2 two-elements-transposition)) p =
    pr2 element-is-not-identity-map-transposition (inv p)
  pr2 (pr2 (pr2 two-elements-transposition)) =
    eq-pair-Σ
      ( eq-htpy
        ( λ x  eq-pair-Σ
          ( ap pr1
            { x =
              subtype-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( pr1 (pr2 (pr2 two-elements-transposition)))
              ( x)}
            { y = subtype-2-Element-Decidable-Subtype Y x}
            ( eq-iff
              (type-t-coprod-id x)
              (coprod-id-type-t x)))
          ( eq-pair-Σ
            ( eq-is-prop (is-prop-is-prop (pr1 (pr1 Y x))))
            ( eq-is-prop (is-prop-is-decidable (pr1 (pr2 (pr1 Y x))))))))
      ( eq-is-prop
        ( pr2
          ( has-cardinality-Prop 2
            ( Σ X  x  type-Decidable-Prop (pr1 Y x))))))
    where
    type-decidable-prop-pr1-two-elements-transposition :
      is-in-2-Element-Decidable-Subtype Y (pr1 two-elements-transposition)
    type-decidable-prop-pr1-two-elements-transposition =
      cases-type-decidable-prop-pr1-two-elements-transposition
        ( is-decidable-subtype-subtype-2-Element-Decidable-Subtype Y
          ( pr1 two-elements-transposition))
      where
      cases-type-decidable-prop-pr1-two-elements-transposition :
        is-decidable
          ( is-in-2-Element-Decidable-Subtype Y
            ( pr1 two-elements-transposition)) 
        is-in-2-Element-Decidable-Subtype Y (pr1 two-elements-transposition)
      cases-type-decidable-prop-pr1-two-elements-transposition (inl Q) = Q
      cases-type-decidable-prop-pr1-two-elements-transposition (inr NQ) =
        ex-falso
          ( pr2 element-is-not-identity-map-transposition
            ( ap
              ( λ R 
                map-transposition' Y (pr1 (two-elements-transposition)) R)
            { x =
              is-decidable-subtype-subtype-2-Element-Decidable-Subtype Y
                ( pr1 two-elements-transposition)}
            { y = inr NQ}
            ( eq-is-prop
              ( is-prop-is-decidable
                ( is-prop-is-in-2-Element-Decidable-Subtype Y
                  ( pr1 two-elements-transposition))))))
    type-decidable-prop-pr1-pr2-two-elements-transposition :
      is-in-2-Element-Decidable-Subtype Y (pr1 (pr2 two-elements-transposition))
    type-decidable-prop-pr1-pr2-two-elements-transposition =
      preserves-subtype-map-transposition Y (pr1 two-elements-transposition)
        ( type-decidable-prop-pr1-two-elements-transposition)
    type-t-coprod-id :
      (x : X) 
      ( Id (pr1 two-elements-transposition) x) +
      ( Id (pr1 (pr2 two-elements-transposition)) x) 
      type-Decidable-Prop (pr1 Y x)
    type-t-coprod-id x (inl Q) =
      tr
        ( is-in-2-Element-Decidable-Subtype Y)
        ( Q)
        ( type-decidable-prop-pr1-two-elements-transposition)
    type-t-coprod-id x (inr Q) =
      tr
        ( is-in-2-Element-Decidable-Subtype Y)
        ( Q)
        ( type-decidable-prop-pr1-pr2-two-elements-transposition)
    cases-coprod-id-type-t :
      (x : X) (p : is-in-2-Element-Decidable-Subtype Y x) 
      (h : Fin 2  type-2-Element-Decidable-Subtype Y) 
      (k1 k2 k3 : Fin 2) 
      Id ( map-inv-equiv h (pair x p)) k1 
      Id ( map-inv-equiv h
           ( pair
             ( pr1 two-elements-transposition)
             ( type-decidable-prop-pr1-two-elements-transposition)))
         ( k2) 
      Id ( map-inv-equiv h
           ( pair
             ( pr1 (pr2 two-elements-transposition))
             ( type-decidable-prop-pr1-pr2-two-elements-transposition)))
         ( k3) 
      ( Id (pr1 two-elements-transposition) x) +
      ( Id (pr1 (pr2 two-elements-transposition)) x)
    cases-coprod-id-type-t x p h (inl (inr star)) (inl (inr star)) k3 K1 K2 K3 =
      inl (ap pr1 (is-injective-map-equiv (inv-equiv h) (K2  inv K1)))
    cases-coprod-id-type-t x p h
      (inl (inr star)) (inr star) (inl (inr star)) K1 K2 K3 =
      inr (ap pr1 (is-injective-map-equiv (inv-equiv h) (K3  inv K1)))
    cases-coprod-id-type-t x p h
      (inl (inr star)) (inr star) (inr star) K1 K2 K3 =
      ex-falso
        ( pr2 element-is-not-identity-map-transposition
        ( inv
          ( ap pr1
            ( is-injective-map-equiv (inv-equiv h) (K2  inv K3)))))
    cases-coprod-id-type-t x p h
      (inr star) (inl (inr star)) (inl (inr star)) K1 K2 K3 =
      ex-falso
        ( pr2 element-is-not-identity-map-transposition
        ( inv
          ( ap pr1
            ( is-injective-map-equiv (inv-equiv h) (K2  inv K3)))))
    cases-coprod-id-type-t x p h
      (inr star) (inl (inr star)) (inr star) K1 K2 K3 =
      inr (ap pr1 (is-injective-map-equiv (inv-equiv h) (K3  inv K1)))
    cases-coprod-id-type-t x p h (inr star) (inr star) k3 K1 K2 K3 =
      inl (ap pr1 (is-injective-map-equiv (inv-equiv h) (K2  inv K1)))
    coprod-id-type-t :
      (x : X)  type-Decidable-Prop (pr1 Y x) 
      ( Id (pr1 two-elements-transposition) x) +
      ( Id (pr1 (pr2 two-elements-transposition)) x)
    coprod-id-type-t x p =
      apply-universal-property-trunc-Prop (pr2 Y)
        ( coprod-Prop
          ( Id-Prop
            ( pair X (is-set-count eX))
            ( pr1 two-elements-transposition)
            ( x))
          ( Id-Prop
            ( pair X (is-set-count eX))
            ( pr1 (pr2 two-elements-transposition))
            ( x))
          ( λ q r 
            pr2 element-is-not-identity-map-transposition (inv (q  inv r))))
        ( λ h 
          cases-coprod-id-type-t x p h
            ( map-inv-equiv h (pair x p))
            ( map-inv-equiv h
              ( pair
                ( pr1 two-elements-transposition)
                ( type-decidable-prop-pr1-two-elements-transposition)))
            ( map-inv-equiv h
              ( pair
                ( pr1 (pr2 two-elements-transposition))
                ( type-decidable-prop-pr1-pr2-two-elements-transposition)))
            ( refl)
            ( refl)
            ( refl))

  element-two-elements-transposition : X
  element-two-elements-transposition =
    pr1 (two-elements-transposition)

  other-element-two-elements-transposition : X
  other-element-two-elements-transposition =
    pr1 (pr2 two-elements-transposition)

  neq-elements-two-elements-transposition :
    ¬ ( element-two-elements-transposition 
        other-element-two-elements-transposition)
  neq-elements-two-elements-transposition =
    pr1 (pr2 (pr2 two-elements-transposition))

  abstract
    cases-eq-two-elements-transposition :
      (x y : X) (np : ¬ (Id x y)) 
      (type-Decidable-Prop (pr1 Y x)) 
      (type-Decidable-Prop (pr1 Y y)) 
      is-decidable (Id (pr1 two-elements-transposition) x) 
      is-decidable (Id (pr1 (pr2 two-elements-transposition)) x) 
      is-decidable (Id (pr1 two-elements-transposition) y) 
      is-decidable (Id (pr1 (pr2 two-elements-transposition)) y) 
      ( ( Id (pr1 two-elements-transposition) x) ×
        ( Id (pr1 (pr2 two-elements-transposition)) y)) +
      ( ( Id (pr1 two-elements-transposition) y) ×
        ( Id (pr1 (pr2 two-elements-transposition)) x))
    cases-eq-two-elements-transposition x y np p1 p2 (inl q) r s (inl u) =
      inl (pair q u)
    cases-eq-two-elements-transposition x y np p1 p2 (inl q) r s (inr nu) =
      ex-falso
        ( contradiction-3-distinct-element-2-Element-Type
          ( 2-element-type-2-Element-Decidable-Subtype
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( pr1 (pr2 (pr2 two-elements-transposition)))))
          ( pair (pr1 two-elements-transposition) (inl refl))
          ( pair (pr1 (pr2 two-elements-transposition)) (inr refl))
          ( pair
            ( y)
            ( tr
              ( λ Y  type-Decidable-Prop (pr1 Y y))
              ( inv (pr2 (pr2 (pr2 two-elements-transposition))))
              ( p2)))
          ( λ p 
            pr1
              ( pr2 (pr2 two-elements-transposition))
              ( pr1 (pair-eq-Σ p)))
          ( λ p  nu (pr1 (pair-eq-Σ p)))
          ( λ p  np (inv q  pr1 (pair-eq-Σ p))))
    cases-eq-two-elements-transposition
      x y np p1 p2 (inr nq) (inl r) (inl s) u =
      inr (pair s r)
    cases-eq-two-elements-transposition
      x y np p1 p2 (inr nq) (inl r) (inr ns) u =
      ex-falso
        ( contradiction-3-distinct-element-2-Element-Type
          ( 2-element-type-2-Element-Decidable-Subtype
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( pr1 (pr2 (pr2 two-elements-transposition)))))
          ( pair (pr1 two-elements-transposition) (inl refl))
          ( pair (pr1 (pr2 two-elements-transposition)) (inr refl))
          ( pair
            ( y)
            ( tr
              ( λ Y  type-Decidable-Prop (pr1 Y y))
              ( inv (pr2 (pr2 (pr2 two-elements-transposition))))
              ( p2)))
          ( λ p 
            pr1
              ( pr2 (pr2 two-elements-transposition))
              ( pr1 (pair-eq-Σ p)))
          ( λ p  np (inv r  pr1 (pair-eq-Σ p)))
          ( λ p  ns (pr1 (pair-eq-Σ p))))
    cases-eq-two-elements-transposition x y np p1 p2 (inr nq) (inr nr) s u =
      ex-falso
        ( contradiction-3-distinct-element-2-Element-Type
          ( 2-element-type-2-Element-Decidable-Subtype
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( pr1 (pr2 (pr2 two-elements-transposition)))))
          ( pair (pr1 two-elements-transposition) (inl refl))
          ( pair (pr1 (pr2 two-elements-transposition)) (inr refl))
          ( pair
            ( x)
            ( tr
              ( λ Y  type-Decidable-Prop (pr1 Y x))
              ( inv (pr2 (pr2 (pr2 two-elements-transposition))))
              ( p1)))
          ( λ p 
            pr1
              ( pr2 (pr2 two-elements-transposition))
              ( pr1 (pair-eq-Σ p)))
          ( λ p  nr (pr1 (pair-eq-Σ p)))
          ( λ p  nq (pr1 (pair-eq-Σ p))))

    eq-two-elements-transposition :
      (x y : X) (np : ¬ (Id x y)) 
      (type-Decidable-Prop (pr1 Y x)) 
      (type-Decidable-Prop (pr1 Y y)) 
      ( ( Id (pr1 two-elements-transposition) x) ×
        ( Id (pr1 (pr2 two-elements-transposition)) y)) +
      ( ( Id (pr1 two-elements-transposition) y) ×
        ( Id (pr1 (pr2 two-elements-transposition)) x))
    eq-two-elements-transposition x y np p1 p2 =
      cases-eq-two-elements-transposition x y np p1 p2
        ( has-decidable-equality-count eX (pr1 two-elements-transposition) x)
        ( has-decidable-equality-count
          ( eX)
          ( pr1 (pr2 two-elements-transposition))
          ( x))
        ( has-decidable-equality-count eX (pr1 two-elements-transposition) y)
        ( has-decidable-equality-count
          ( eX)
          ( pr1 (pr2 two-elements-transposition))
          ( y))

The case of Fin n

module _
  {n : }
  (Y : 2-Element-Decidable-Subtype (lzero) (Fin n))
  where

  two-elements-transposition-Fin :
    Σ ( Fin n)
      ( λ x 
        Σ ( Fin n)
          ( λ y 
            Σ ( ¬ (Id x y))
              ( λ np 
                Id ( standard-2-Element-Decidable-Subtype
                     ( has-decidable-equality-Fin n)
                     ( np))
                   ( Y))))
  two-elements-transposition-Fin =
    tr
      ( λ p 
        Σ ( Fin n)
          ( λ x 
            Σ ( Fin n)
              ( λ y 
                Σ ( ¬ (Id x y))
                  ( λ np 
                    Id
                      ( standard-2-Element-Decidable-Subtype
                        ( p)
                        ( np))
                     ( Y)))))
      ( eq-is-prop (is-prop-has-decidable-equality))
      ( two-elements-transposition (count-Fin n) Y)

  element-two-elements-transposition-Fin : Fin n
  element-two-elements-transposition-Fin =
    pr1 (two-elements-transposition-Fin)

  other-element-two-elements-transposition-Fin : Fin n
  other-element-two-elements-transposition-Fin =
    pr1 (pr2 two-elements-transposition-Fin)

  neq-elements-two-elements-transposition-Fin :
    ¬ ( element-two-elements-transposition-Fin 
        other-element-two-elements-transposition-Fin)
  neq-elements-two-elements-transposition-Fin =
    pr1 (pr2 (pr2 two-elements-transposition-Fin))

  eq-standard-2-element-decidable-subtype-two-elements-transposition-Fin :
    standard-2-Element-Decidable-Subtype
      ( has-decidable-equality-Fin n)
      ( neq-elements-two-elements-transposition-Fin) 
    Y
  eq-standard-2-element-decidable-subtype-two-elements-transposition-Fin =
    pr2 (pr2 (pr2 two-elements-transposition-Fin))

  htpy-two-elements-transpositon-Fin :
    htpy-equiv
      ( standard-transposition
        ( has-decidable-equality-Fin n)
        ( neq-elements-two-elements-transposition-Fin))
      ( transposition Y)
  htpy-two-elements-transpositon-Fin =
    htpy-eq
      ( ap
        map-transposition
        eq-standard-2-element-decidable-subtype-two-elements-transposition-Fin)

Transpositions can be transported along equivalences

module _
  {l1 l2 l3 l4 : Level} (X : UU l1) (Y : UU l2) (e : X  Y)
  where

  transposition-conjugation-equiv :
    ( Σ
      ( X  Decidable-Prop l3)
      ( λ P 
        has-cardinality
          ( 2)
          ( Σ X (type-Decidable-Prop  P)))) 
      ( Σ
        ( Y  Decidable-Prop (l3  l4))
        ( λ P 
          has-cardinality 2
            ( Σ Y (type-Decidable-Prop  P))))
  pr1 (pr1 (transposition-conjugation-equiv (pair P H)) x) =
    raise l4 (type-Decidable-Prop (P (map-inv-equiv e x)))
  pr1 (pr2 (pr1 (transposition-conjugation-equiv (pair P H)) x)) =
    is-prop-all-elements-equal
       p1 p2 
        is-injective-map-equiv
          ( inv-equiv
            ( compute-raise l4 (type-Decidable-Prop (P (map-inv-equiv e x)))))
          ( eq-is-prop (is-prop-type-Decidable-Prop (P (map-inv-equiv e x)))))
  pr2 (pr2 (pr1 (transposition-conjugation-equiv (pair P H)) x)) =
    is-decidable-raise l4
      ( type-Decidable-Prop (P (map-inv-equiv e x)))
      ( is-decidable-Decidable-Prop (P (map-inv-equiv e x)))
  pr2 (transposition-conjugation-equiv (pair P H)) =
    apply-universal-property-trunc-Prop
      ( H)
      ( has-cardinality-Prop 2
        ( Σ Y  x  raise l4 (type-Decidable-Prop (P (map-inv-equiv e x))))))
       λ h 
        unit-trunc-Prop
          ( pair
            ( λ x 
              pair
                ( map-equiv e (pr1 (map-equiv h x)))
                ( tr
                  ( λ g 
                    raise l4
                      ( type-Decidable-Prop
                        ( P (map-equiv g (pr1 (map-equiv h x))))))
                  ( inv (left-inverse-law-equiv e))
                  ( map-raise (pr2 (map-equiv h x)))))
            ( is-equiv-has-inverse
              ( λ (pair x p) 
                map-inv-equiv h ( pair (map-inv-equiv e x) (map-inv-raise p)))
              ( λ (pair x p) 
                eq-pair-Σ
                  ( ( ap
                      ( λ g 
                        map-equiv
                          ( e)
                          ( pr1
                            ( map-equiv
                              ( g)
                              ( pair (map-inv-equiv e x) (map-inv-raise p)))))
                      ( right-inverse-law-equiv h)) 
                    ( ap  g  map-equiv g x) (right-inverse-law-equiv e)))
                  ( eq-is-prop
                    ( pr1
                      ( pr2
                        ( pr1
                          ( transposition-conjugation-equiv (pair P H))
                          ( x))))))
              ( λ b 
                ( ap
                  ( λ w 
                    map-inv-equiv
                      ( h)
                      ( pair (map-equiv (pr1 w) (pr1 (map-equiv h b))) (pr2 w)))
                  { y = pair id-equiv (pr2 (map-equiv h b))}
                  ( eq-pair-Σ
                    ( left-inverse-law-equiv e)
                    ( eq-is-prop
                      ( is-prop-type-Decidable-Prop
                        ( P (pr1 (map-equiv h b)))))) 
                  ( ap  g  map-equiv g b) (left-inverse-law-equiv h))))))

  abstract
    correct-transposition-conjugation-equiv :
      (t : Σ
        ( X  Decidable-Prop l3)
        ( λ P  has-cardinality 2 (Σ X (type-Decidable-Prop  P)))) 
      htpy-equiv
        ( transposition
          (transposition-conjugation-equiv t))
        ( (e ∘e (transposition t)) ∘e (inv-equiv e))
    correct-transposition-conjugation-equiv t x =
      cases-correct-transposition-conjugation-equiv
        ( is-decidable-Decidable-Prop (pr1 t (map-inv-equiv e x)))
      where
      cases-correct-transposition-conjugation-equiv :
        (Q : is-decidable (type-Decidable-Prop (pr1 t (map-inv-equiv e x)))) 
        Id
          ( map-transposition'
            (transposition-conjugation-equiv t)
            ( x)
            ( is-decidable-raise
              ( l4)
              ( type-Decidable-Prop (pr1 t (map-inv-equiv e x)))
              ( Q)))
          ( map-equiv e
            ( map-transposition' t (map-inv-equiv e x) Q))
      cases-correct-transposition-conjugation-equiv (inl p) =
        ap
          ( pr1)
          ( compute-swap-2-Element-Type
            ( pair
              ( Σ Y  y  pr1 (pr1 (transposition-conjugation-equiv t) y)))
              ( pr2 (transposition-conjugation-equiv t)))
            ( pair x (map-raise p))
            ( pair
              ( map-equiv e (pr1 second-pair-X))
              ( map-raise
                ( tr
                  ( λ g 
                    type-Decidable-Prop
                      ( pr1 t (map-equiv g (pr1 second-pair-X))))
                  ( inv (left-inverse-law-equiv e))
                  ( pr2 second-pair-X))))
            λ q 
              has-no-fixed-points-swap-2-Element-Type
                ( pair (Σ X  y  type-Decidable-Prop (pr1 t y))) (pr2 t))
                { pair (map-inv-equiv e x) p}
                ( eq-pair-Σ
                  ( is-injective-map-equiv
                    ( e)
                    ( inv (pr1 (pair-eq-Σ q)) 
                      ap
                        ( λ g  map-equiv g x)
                        ( inv (right-inverse-law-equiv e))))
                  ( eq-is-prop
                    ( is-prop-type-Decidable-Prop
                      ( pr1 t (map-inv-equiv e x))))))
        where
        second-pair-X : Σ X  y  type-Decidable-Prop (pr1 t y))
        second-pair-X =
          map-swap-2-Element-Type
            (pair (Σ X  y  type-Decidable-Prop (pr1 t y))) (pr2 t))
            (pair (map-inv-equiv e x) p)
      cases-correct-transposition-conjugation-equiv (inr np) =
        ap  g  map-equiv g x) (inv (right-inverse-law-equiv e))

    correct-transposition-conjugation-equiv-list :
      (li : list
        ( Σ
          ( X  Decidable-Prop l3)
          ( λ P 
            has-cardinality 2 (Σ X (type-Decidable-Prop  P))))) 
      htpy-equiv
        ( permutation-list-transpositions
          ( map-list transposition-conjugation-equiv li))
        ( (e ∘e (permutation-list-transpositions li)) ∘e (inv-equiv e))
    correct-transposition-conjugation-equiv-list nil x =
      ap  g  map-equiv g x) (inv (right-inverse-law-equiv e))
    correct-transposition-conjugation-equiv-list (cons t li) x =
      ( correct-transposition-conjugation-equiv
        ( t)
        (map-equiv
          ( permutation-list-transpositions
            ( map-list transposition-conjugation-equiv li))
          ( x))) 
        ( ( ap
          ( map-equiv ((e ∘e transposition t) ∘e inv-equiv e))
          ( correct-transposition-conjugation-equiv-list li x)) 
          ( ap
            ( λ g 
              map-equiv
                ( ( ( (e ∘e transposition t) ∘e g) ∘e
                    ( permutation-list-transpositions li)) ∘e
                  ( inv-equiv e))
                ( x))
            ( left-inverse-law-equiv e)))

For all n : ℕ and for each transposition of Fin n, there exists a matching transposition in Fin (succ-ℕ n)

Fin-succ-Fin-transposition :
  (n : ) 
  ( Σ
    ( Fin n  Decidable-Prop lzero)
    ( λ P  has-cardinality 2 (Σ (Fin n) (type-Decidable-Prop  P)))) 
    ( Σ
      ( Fin (succ-ℕ n)  Decidable-Prop lzero)
      ( λ P 
        has-cardinality 2
          ( Σ (Fin (succ-ℕ n)) (type-Decidable-Prop  P))))
pr1 (Fin-succ-Fin-transposition n (pair P H)) (inl x) = P x
pr1 (Fin-succ-Fin-transposition n (pair P H)) (inr x) =
  pair empty (pair is-prop-empty is-decidable-empty)
pr2 (Fin-succ-Fin-transposition n (pair P H)) =
  apply-universal-property-trunc-Prop
    ( H)
    ( has-cardinality-Prop 2
      ( Σ
        ( Fin (succ-ℕ n))
        ( type-Decidable-Prop  pr1 (Fin-succ-Fin-transposition n (pair P H)))))
    ( λ h 
      unit-trunc-Prop
        ( ( pair f (is-equiv-has-inverse inv-f retr-f sec-f)) ∘e
          ( ( inv-right-unit-law-coprod-is-empty
              ( Σ
                ( Fin n)
                ( type-Decidable-Prop  P))
              ( Σ unit  _  empty))
              ( map-right-absorption-prod)) ∘e
            ( h))))
  where
  f :
    ( Σ (Fin n) (type-Decidable-Prop  P)) + (Σ unit  _  empty)) 
    Σ (Fin (succ-ℕ n))
     x 
       type-Decidable-Prop
       (pr1 (Fin-succ-Fin-transposition n (pair P H)) x))
  f (inl (pair x p)) = pair (inl x) p
  inv-f :
    Σ ( Fin (succ-ℕ n))
      ( λ x 
        type-Decidable-Prop
        (pr1 (Fin-succ-Fin-transposition n (pair P H)) x)) 
    (Σ (Fin n) (type-Decidable-Prop  P)) + (Σ unit  _  empty))
  inv-f (pair (inl x) p) = inl (pair x p)
  retr-f : (f  inv-f) ~ id
  retr-f (pair (inl x) p) = refl
  sec-f : (inv-f  f) ~ id
  sec-f (inl (pair x p)) = refl

correct-Fin-succ-Fin-transposition :
  (n : ) 
  (t : Σ
    ( Fin n  Decidable-Prop lzero)
    ( λ P  has-cardinality 2 (Σ (Fin n) (type-Decidable-Prop  P)))) 
  htpy-equiv
    ( transposition (Fin-succ-Fin-transposition n t))
    ( pr1
      ( map-equiv
        ( extend-equiv-Maybe (Fin-Set n))
        ( transposition t)))
correct-Fin-succ-Fin-transposition n t (inl x) with
  is-decidable-Decidable-Prop (pr1 t x)
correct-Fin-succ-Fin-transposition n t (inl x) | inl p =
    ap
      ( pr1)
      ( compute-swap-2-Element-Type
        ( pair
          ( Σ
            ( Fin (succ-ℕ n))
            ( type-Decidable-Prop  pr1 (Fin-succ-Fin-transposition n t)))
          ( pr2 (Fin-succ-Fin-transposition n t)))
        ( pair (inl x) p)
        ( pair
          ( inl
            ( pr1
              ( map-swap-2-Element-Type
                ( pair
                  ( Σ (Fin n) (type-Decidable-Prop  pr1 t))
                  ( pr2 t))
                ( pair x p))))
          ( pr2
            ( map-swap-2-Element-Type
              ( pair
                ( Σ (Fin n) (type-Decidable-Prop  pr1 t))
                ( pr2 t))
              ( pair x p))))
        ( λ eq 
          has-no-fixed-points-swap-2-Element-Type
            ( pair (Σ (Fin n) (type-Decidable-Prop  pr1 t)) (pr2 t))
            { pair x p}
            ( eq-pair-Σ
              ( is-injective-inl (inv (pr1 (pair-eq-Σ eq))))
              ( eq-is-prop (is-prop-type-Decidable-Prop (pr1 t x))))))
correct-Fin-succ-Fin-transposition n t (inl x) | inr np = refl
correct-Fin-succ-Fin-transposition n t (inr star) = refl

correct-Fin-succ-Fin-transposition-list :
  (n : )
  (l : list
    ( Σ
      ( Fin n  Decidable-Prop lzero)
      ( λ P 
        has-cardinality 2 (Σ (Fin n) (type-Decidable-Prop  P))))) 
  htpy-equiv
    ( permutation-list-transpositions
      ( map-list (Fin-succ-Fin-transposition n) l))
    ( pr1
      ( map-equiv
        ( extend-equiv-Maybe (Fin-Set n))
        ( permutation-list-transpositions l)))
correct-Fin-succ-Fin-transposition-list n nil =
  inv-htpy (id-map-coprod (Fin n) unit)
correct-Fin-succ-Fin-transposition-list n (cons t l) x =
  correct-Fin-succ-Fin-transposition
    ( n)
    ( t)
    ( map-equiv
      ( permutation-list-transpositions
        ( map-list (Fin-succ-Fin-transposition n) l))
      ( x)) 
      ( (ap
        ( map-equiv
          ( pr1
            ( map-equiv (extend-equiv-Maybe (Fin-Set n)) (transposition t))))
        ( correct-Fin-succ-Fin-transposition-list n l x)) 
        ( inv
          ( comp-extend-equiv-Maybe
            ( Fin-Set n)
            ( transposition t)
            ( permutation-list-transpositions l)
            ( x))))
eq-transposition-precomp-standard-2-Element-Decidable-Subtype :
  {l : Level} {X : UU l} (H : has-decidable-equality X) 
  {x y : X} (np : ¬ (Id x y)) 
  Id
    ( precomp-equiv-2-Element-Decidable-Subtype
      ( standard-transposition H np)
      ( standard-2-Element-Decidable-Subtype H np))
    ( standard-2-Element-Decidable-Subtype H np)
eq-transposition-precomp-standard-2-Element-Decidable-Subtype
  {l} {X} H {x} {y} np =
  eq-pair-Σ
    ( eq-htpy
      ( λ z 
        eq-pair-Σ
          ( eq-equiv
            ( pr1
              ( pr1
                ( precomp-equiv-2-Element-Decidable-Subtype
                  ( standard-transposition H np)
                  ( standard-2-Element-Decidable-Subtype H np))
                ( z)))
            ( pr1 (pr1 (standard-2-Element-Decidable-Subtype H np) z))
            ( equiv-iff
              ( subtype-standard-2-Element-Decidable-Subtype H np
                ( map-inv-equiv (standard-transposition H np) z))
              ( subtype-standard-2-Element-Decidable-Subtype H np z)
              ( f z)
              ( g z)))
          ( eq-pair-Σ
            ( eq-is-prop
              ( is-prop-is-prop
                ( pr1 (pr1 (standard-2-Element-Decidable-Subtype H np) z))))
            ( eq-is-prop
              ( is-prop-is-decidable
                ( pr1
                  ( pr2
                    ( pr1
                      ( standard-2-Element-Decidable-Subtype H np)
                      ( z)))))))))
    ( eq-is-prop is-prop-type-trunc-Prop)
  where
  f :
    (z : X) 
    pr1
      ( pr1
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( standard-transposition H np)
          ( standard-2-Element-Decidable-Subtype H np)) z) 
    pr1 (pr1 (standard-2-Element-Decidable-Subtype H np) z)
  f z (inl p) =
    inr
      ( is-injective-map-equiv
        ( standard-transposition H np)
        ( ( right-computation-standard-transposition H np) 
          ( p)))
  f z (inr p) =
    inl
      ( is-injective-map-equiv
        ( standard-transposition H np)
        ( ( left-computation-standard-transposition H np) 
          ( p)))
  g :
    (z : X) 
    pr1 (pr1 (standard-2-Element-Decidable-Subtype H np) z) 
    pr1
      ( pr1
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( standard-transposition H np)
          ( standard-2-Element-Decidable-Subtype H np)) z)
  g z (inl p) =
    inr
      ( ( inv
        ( left-computation-standard-transposition H np)) 
        ( ap (map-standard-transposition H np) p))
  g z (inr p) =
    inl
      ( ( inv
        ( right-computation-standard-transposition H np)) 
        ( ap (map-standard-transposition H np) p))

eq-transposition-precomp-ineq-standard-2-Element-Decidable-Subtype :
  {l : Level} {X : UU l} (H : has-decidable-equality X) 
  {x y z w : X} (np : ¬ (Id x y)) (np' : ¬ (Id z w)) 
  ¬ (Id x z)  ¬ (Id x w)  ¬ (Id y z)  ¬ (Id y w) 
  Id
    ( precomp-equiv-2-Element-Decidable-Subtype
      ( standard-transposition H np)
      ( standard-2-Element-Decidable-Subtype H np'))
    ( standard-2-Element-Decidable-Subtype H np')
eq-transposition-precomp-ineq-standard-2-Element-Decidable-Subtype
  {l} {X} H {x} {y} {z} {w} np np' nq1 nq2 nq3 nq4 =
  eq-pair-Σ
    ( eq-htpy
      ( λ u 
        eq-pair-Σ
          ( eq-equiv
            ( pr1
              ( pr1
                ( precomp-equiv-2-Element-Decidable-Subtype
                  ( standard-transposition H np)
                  ( standard-2-Element-Decidable-Subtype H np'))
                ( u)))
            ( pr1 (pr1 (standard-2-Element-Decidable-Subtype H np') u))
            ( equiv-iff
              ( subtype-standard-2-Element-Decidable-Subtype H np'
                ( map-inv-equiv (standard-transposition H np) u))
              ( subtype-standard-2-Element-Decidable-Subtype H np' u)
              ( f u)
              ( g u)))
          ( eq-pair-Σ
            ( eq-is-prop
              ( is-prop-is-prop
                ( pr1 (pr1 (standard-2-Element-Decidable-Subtype H np') u))))
            ( eq-is-prop
              ( is-prop-is-decidable
                ( pr1
                  ( pr2
                    ( pr1
                      ( standard-2-Element-Decidable-Subtype H np')
                      ( u)))))))))
    ( eq-is-prop is-prop-type-trunc-Prop)
  where
  f :
    (u : X) 
    pr1
      ( pr1
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( standard-transposition H np)
          ( standard-2-Element-Decidable-Subtype H np')) u) 
    pr1 (pr1 (standard-2-Element-Decidable-Subtype H np') u)
  f u (inl p) =
    inl
      ( is-injective-map-equiv
        ( standard-transposition H np)
        ( ( is-fixed-point-standard-transposition H np z nq1 nq3) 
          ( p)))
  f u (inr p) =
    inr
      ( is-injective-map-equiv
        ( standard-transposition H np)
        ( ( is-fixed-point-standard-transposition H np w nq2 nq4) 
          ( p)))
  g :
    (u : X) 
    pr1 (pr1 (standard-2-Element-Decidable-Subtype H np') u) 
    pr1
      ( pr1
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( standard-transposition H np)
          ( standard-2-Element-Decidable-Subtype H np')) u)
  g u (inl p) =
    inl
      ( ( inv
        ( is-fixed-point-standard-transposition H np z nq1 nq3)) 
        ( ap (map-standard-transposition H np) p))
  g u (inr p) =
    inr
      ( ( inv
        ( is-fixed-point-standard-transposition H np w nq2 nq4)) 
        ( ap (map-standard-transposition H np) p))
module _
  {l1 : Level} (X : UU l1) (l l' : Level)
  where

  cases-eq-equiv-universes-transposition :
    ( P : 2-Element-Decidable-Subtype l X) (x : X) 
    ( d : is-decidable (is-in-2-Element-Decidable-Subtype P x)) 
    Id
      ( map-transposition' P x d)
      ( map-transposition
        ( map-equiv (equiv-universes-2-Element-Decidable-Subtype X l l') P)
        ( x))
  cases-eq-equiv-universes-transposition P x (inl p) =
    ( ap pr1
      ( inv
        ( compute-swap-2-Element-Decidable-Subtype
          ( map-equiv (equiv-universes-2-Element-Decidable-Subtype X l l') P)
          ( pair x (pr1 (iff-universes-decidable-subtype X l l' (pr1 P) x) p))
          ( pair
            ( pr1 (map-swap-2-Element-Decidable-Subtype P (pair x p)))
            ( pr1
              ( iff-universes-decidable-subtype X l l' (pr1 P)
                ( pr1 (map-swap-2-Element-Decidable-Subtype P (pair x p))))
              ( pr2 (map-swap-2-Element-Decidable-Subtype P (pair x p)))))
          ( λ q 
            has-no-fixed-points-swap-2-Element-Type
              ( 2-element-type-2-Element-Decidable-Subtype P)
              ( eq-pair-Σ
                ( pr1 (pair-eq-Σ (inv q)))
                ( eq-is-prop (is-prop-type-Decidable-Prop (pr1 P x)))))))) 
      ap
      ( λ d' 
        map-transposition'
          ( map-equiv
            ( equiv-universes-2-Element-Decidable-Subtype X l l')
            ( P))
          ( x)
          ( d'))
      { x = inl (pr1 (iff-universes-decidable-subtype X l l' (pr1 P) x) p)}
      { y =
        is-decidable-Decidable-Prop
          ( map-equiv (equiv-universes-decidable-subtype X l l') (pr1 P) x)}
      ( eq-is-prop
        ( is-prop-is-decidable
          ( is-prop-type-Decidable-Prop
            (map-equiv (equiv-universes-decidable-subtype X l l') (pr1 P) x))))
  cases-eq-equiv-universes-transposition P x (inr np) =
    ap
      ( λ d' 
        map-transposition'
          ( map-equiv
            ( equiv-universes-2-Element-Decidable-Subtype X l l')
            ( P))
          ( x)
          ( d'))
      { x = inr (np  pr2 (iff-universes-decidable-subtype X l l' (pr1 P) x))}
      { y =
        is-decidable-Decidable-Prop
          ( map-equiv (equiv-universes-decidable-subtype X l l') (pr1 P) x)}
      ( eq-is-prop
        ( is-prop-is-decidable
          ( is-prop-type-Decidable-Prop
            (map-equiv (equiv-universes-decidable-subtype X l l') (pr1 P) x))))

  eq-equiv-universes-transposition :
    ( P : 2-Element-Decidable-Subtype l X) 
    Id
      ( transposition P)
      ( transposition
        ( map-equiv (equiv-universes-2-Element-Decidable-Subtype X l l') P))
  eq-equiv-universes-transposition P =
    eq-htpy-equiv
      ( λ x 
        cases-eq-equiv-universes-transposition P x
          ( is-decidable-Decidable-Prop (pr1 P x)))

  eq-equiv-universes-transposition-list :
    ( li : list (2-Element-Decidable-Subtype l X)) 
    Id
      ( permutation-list-transpositions li)
      ( permutation-list-transpositions
        ( map-list
          ( map-equiv (equiv-universes-2-Element-Decidable-Subtype X l l'))
          ( li)))
  eq-equiv-universes-transposition-list nil = refl
  eq-equiv-universes-transposition-list (cons P li) =
    ap-binary
      ( _∘e_)
      ( eq-equiv-universes-transposition P)
      ( eq-equiv-universes-transposition-list li)

Conjugate of a transposition is also a transposition

module _
  {l1 : Level}
  {X : UU l1}
  (H : has-decidable-equality X)
  {x y z : X}
  (npxy : ¬ (x  y))
  (npyz : ¬ (y  z))
  (npxz : ¬ (x  z))
  where

  cases-htpy-conjugate-transposition :
    (w : X) 
    ((w  x) + ¬ (w  x)) 
    ((w  y) + ¬ (w  y)) 
    ((w  z) + ¬ (w  z)) 
    Id
      ( map-equiv
        ( standard-transposition H npyz ∘e
          ( standard-transposition H npxy ∘e standard-transposition H npyz))
        w)
      ( map-equiv ( standard-transposition H npxz) w)
  cases-htpy-conjugate-transposition x (inl refl) _ _ =
    ( ( ap
        ( λ w 
          map-equiv
            ( standard-transposition H npyz ∘e standard-transposition H npxy)
            ( w))
        ( is-fixed-point-standard-transposition
          ( H)
          ( npyz)
          ( x)
          ( npxy  inv)
          ( npxz  inv))) 
      ( ( ap
          ( λ w  map-equiv (standard-transposition H npyz) w)
          ( left-computation-standard-transposition H npxy)) 
        ( ( left-computation-standard-transposition H npyz) 
          ( ( inv (left-computation-standard-transposition H npxz))))))
  cases-htpy-conjugate-transposition y (inr neqx) (inl refl) _ =
    ( ( ap
        ( λ w 
          map-equiv
            ( standard-transposition H npyz ∘e standard-transposition H npxy)
            ( w))
        ( left-computation-standard-transposition H npyz)) 
      ( ( ap
          ( λ w  map-equiv (standard-transposition H npyz) w)
          ( is-fixed-point-standard-transposition H npxy z npxz npyz)) 
        ( ( right-computation-standard-transposition H npyz) 
          ( inv
            ( is-fixed-point-standard-transposition
              ( H)
              ( npxz)
              ( y)
              ( npxy)
              ( npyz  inv))))))
  cases-htpy-conjugate-transposition z (inr neqx) (inr neqy) (inl refl) =
    ( ( ap
        ( λ w 
          map-equiv
            ( standard-transposition H npyz ∘e standard-transposition H npxy)
            ( w))
        ( right-computation-standard-transposition H npyz)) 
      ( ( ap
          ( λ w  map-equiv (standard-transposition H npyz) w)
          ( right-computation-standard-transposition H npxy)) 
        ( ( is-fixed-point-standard-transposition
            ( H)
            ( npyz)
            ( x)
            ( npxy  inv)
            ( npxz  inv)) 
          ( inv (right-computation-standard-transposition H npxz)))))
  cases-htpy-conjugate-transposition w (inr neqx) (inr neqy) (inr neqz) =
    ( ( ap
        ( λ w 
          map-equiv
            ( standard-transposition H npyz ∘e standard-transposition H npxy)
            ( w))
        ( is-fixed-point-standard-transposition
          ( H)
          ( npyz)
          ( w)
          ( neqy  inv)
          ( neqz  inv))) 
      ( ( ap
          ( λ w  map-equiv (standard-transposition H npyz) w)
          ( is-fixed-point-standard-transposition
            ( H)
            ( npxy)
            ( w)
            ( neqx  inv)
            ( neqy  inv))) 
        ( ( is-fixed-point-standard-transposition
            ( H)
            ( npyz)
            ( w)
            ( neqy  inv)
            ( neqz  inv)) 
          ( inv
            ( is-fixed-point-standard-transposition
              ( H)
              ( npxz)
              ( w)
              ( neqx  inv)
              ( neqz  inv))))))

  htpy-conjugate-transposition :
    htpy-equiv
      ( standard-transposition H npyz ∘e
        ( standard-transposition H npxy ∘e
          standard-transposition H npyz))
      ( standard-transposition H npxz)
  htpy-conjugate-transposition w =
    cases-htpy-conjugate-transposition w ( H w x) ( H w y) ( H w z)