Orbits of permutations

{-# OPTIONS --lossy-unification #-}
module finite-group-theory.orbits-permutations where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.decidable-types
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.euclidean-division-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.lower-bounds-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers
open import elementary-number-theory.well-ordering-principle-natural-numbers

open import finite-group-theory.transpositions

open import foundation.automorphisms
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-equivalence-relations
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.double-negation
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalence-classes
open import foundation.equivalence-extensionality
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.functions
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.iterating-functions
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.repetitions-of-values
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels

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.image-of-maps
open import univalent-combinatorics.pigeonhole-principle
open import univalent-combinatorics.standard-finite-types

Idea

The orbit of a point x for a permutation f is the set of point obtained by iterating f on x.

Definition

The groupoid of iterative orbits of an automorphism on a finite set

module _
  {l : Level} (X : 𝔽 l) (e : type-𝔽 X  type-𝔽 X)
  where

  iso-iterative-groupoid-automorphism-𝔽 : (x y : type-𝔽 X)  UU l
  iso-iterative-groupoid-automorphism-𝔽 x y =
    Σ   n  Id (iterate n (map-equiv e) x) y)

  natural-isomorphism-iterative-groupoid-automorphism-𝔽 :
    (x y : type-𝔽 X) (f : iso-iterative-groupoid-automorphism-𝔽 x y)  
  natural-isomorphism-iterative-groupoid-automorphism-𝔽 x y = pr1

  id-iso-iterative-groupoid-automorphism-𝔽 :
    (x : type-𝔽 X)  iso-iterative-groupoid-automorphism-𝔽 x x
  pr1 (id-iso-iterative-groupoid-automorphism-𝔽 x) = 0
  pr2 (id-iso-iterative-groupoid-automorphism-𝔽 x) = refl

  comp-iso-iterative-groupoid-automorphism-𝔽 :
    {x y z : type-𝔽 X} 
    iso-iterative-groupoid-automorphism-𝔽 y z 
    iso-iterative-groupoid-automorphism-𝔽 x y 
    iso-iterative-groupoid-automorphism-𝔽 x z
  pr1 (comp-iso-iterative-groupoid-automorphism-𝔽 (pair n q) (pair m p)) =
    n +ℕ m
  pr2 (comp-iso-iterative-groupoid-automorphism-𝔽 (pair n q) (pair m p)) =
    iterate-add-ℕ n m (map-equiv e) _  (ap (iterate n (map-equiv e)) p  q)

Properties

For types equipped with a counting, orbits of permutations are finite

The map i ↦ eⁱ a repeats itself.

module _
  {l : Level} (X : UU l) (eX : count X) (f : Aut X) (a : X)
  where

  repetition-iterate-automorphism-Fin :
    repetition-of-values
      ( λ (k : Fin (succ-ℕ (number-of-elements-count eX))) 
        iterate
          ( nat-Fin (succ-ℕ (number-of-elements-count eX)) k)
          ( map-equiv f)
          ( a))
  repetition-iterate-automorphism-Fin =
    repetition-of-values-le-count
      ( count-Fin (succ-ℕ (number-of-elements-count eX)))
      ( eX)
      ( λ k 
        iterate
          ( nat-Fin (succ-ℕ (number-of-elements-count eX)) k)
          ( map-equiv f)
          ( a))
      ( succ-le-ℕ (number-of-elements-count eX))

  point1-iterate-ℕ : 
  point1-iterate-ℕ =
    nat-Fin
      ( succ-ℕ (number-of-elements-count eX))
      ( pr1 (pr1 repetition-iterate-automorphism-Fin))

  point2-iterate-ℕ : 
  point2-iterate-ℕ =
    nat-Fin
      ( succ-ℕ (number-of-elements-count eX))
      ( pr1 (pr2 (pr1 repetition-iterate-automorphism-Fin)))

  neq-points-iterate-ℕ : ¬ (Id point1-iterate-ℕ point2-iterate-ℕ)
  neq-points-iterate-ℕ p =
    pr2
      ( pr2 (pr1 repetition-iterate-automorphism-Fin))
      ( is-injective-nat-Fin (succ-ℕ (number-of-elements-count eX)) p)

  two-points-iterate-ordered-ℕ :
    ( point1-iterate-ℕ ≤-ℕ point2-iterate-ℕ) +
    ( point2-iterate-ℕ ≤-ℕ point1-iterate-ℕ) 
    Σ ( )
      ( λ n 
        Σ ( )
          ( λ m 
            ( le-ℕ m n) ×
            ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
  pr1 (two-points-iterate-ordered-ℕ (inl p)) = point2-iterate-ℕ
  pr1 (pr2 (two-points-iterate-ordered-ℕ (inl p))) = point1-iterate-ℕ
  pr1 (pr2 (pr2 (two-points-iterate-ordered-ℕ (inl p)))) =
    le-leq-neq-ℕ p neq-points-iterate-ℕ
  pr2 (pr2 (pr2 (two-points-iterate-ordered-ℕ (inl p)))) =
    inv (pr2 repetition-iterate-automorphism-Fin)
  pr1 (two-points-iterate-ordered-ℕ (inr p)) = point1-iterate-ℕ
  pr1 (pr2 (two-points-iterate-ordered-ℕ (inr p))) = point2-iterate-ℕ
  pr1 (pr2 (pr2 (two-points-iterate-ordered-ℕ (inr p)))) =
    le-leq-neq-ℕ p λ e  neq-points-iterate-ℕ (inv e)
  pr2 (pr2 (pr2 (two-points-iterate-ordered-ℕ (inr p)))) =
    pr2 repetition-iterate-automorphism-Fin

  leq-greater-point-number-elements :
    ( p :
      ( point1-iterate-ℕ ≤-ℕ point2-iterate-ℕ) +
      ( point2-iterate-ℕ ≤-ℕ point1-iterate-ℕ)) 
    pr1 (two-points-iterate-ordered-ℕ p) ≤-ℕ number-of-elements-count eX
  leq-greater-point-number-elements (inl p) =
    ( upper-bound-nat-Fin
      ( number-of-elements-count eX)
      ( pr1 (pr2 (pr1 repetition-iterate-automorphism-Fin))))
  leq-greater-point-number-elements (inr p) =
    ( upper-bound-nat-Fin
      ( number-of-elements-count eX)
      ( pr1 (pr1 repetition-iterate-automorphism-Fin)))

  abstract
    min-repeating :
      minimal-element-ℕ
        ( λ n 
          Σ ( )
            ( λ m 
              ( le-ℕ m n) ×
              ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
    min-repeating =
      well-ordering-principle-ℕ
        ( λ n 
          Σ ( )
            ( λ m 
              ( le-ℕ m n) ×
              ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
        ( λ n 
          is-decidable-bounded-Σ-ℕ n ( λ m  le-ℕ m n)
            ( λ m  Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))
            ( λ m  is-decidable-le-ℕ m n)
            ( λ m 
              has-decidable-equality-count eX
                ( iterate n (map-equiv f) a)
                ( iterate m (map-equiv f) a))
            ( λ m p  leq-le-ℕ m n p))
        ( two-points-iterate-ordered-ℕ
          ( linear-leq-ℕ point1-iterate-ℕ point2-iterate-ℕ))

    first-point-min-repeating : 
    first-point-min-repeating = pr1 min-repeating

    second-point-min-repeating : 
    second-point-min-repeating = pr1 (pr1 (pr2 min-repeating))

    le-min-reporting : le-ℕ second-point-min-repeating first-point-min-repeating
    le-min-reporting = pr1 (pr2 (pr1 (pr2 min-repeating)))

    is-lower-bound-min-reporting :
      is-lower-bound-ℕ
        ( λ n 
          Σ ( )
            ( λ m 
              ( le-ℕ m n) ×
              ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
        ( first-point-min-repeating)
    is-lower-bound-min-reporting = pr2 (pr2 min-repeating)

    same-image-iterate-min-reporting :
      Id ( iterate first-point-min-repeating (map-equiv f) a)
        ( iterate second-point-min-repeating (map-equiv f) a)
    same-image-iterate-min-reporting = pr2 (pr2 (pr1 (pr2 min-repeating)))

  leq-first-point-min-reporting-succ-number-elements :
    first-point-min-repeating ≤-ℕ (number-of-elements-count eX)
  leq-first-point-min-reporting-succ-number-elements =
    transitive-leq-ℕ
      ( first-point-min-repeating)
      ( pr1
        ( two-points-iterate-ordered-ℕ
          ( linear-leq-ℕ point1-iterate-ℕ point2-iterate-ℕ)))
      ( number-of-elements-count eX)
      ( leq-greater-point-number-elements
        ( linear-leq-ℕ point1-iterate-ℕ point2-iterate-ℕ))
      ( is-lower-bound-min-reporting
        ( pr1
          ( two-points-iterate-ordered-ℕ
            ( linear-leq-ℕ point1-iterate-ℕ point2-iterate-ℕ)))
        ( pr2
          ( two-points-iterate-ordered-ℕ
            ( linear-leq-ℕ point1-iterate-ℕ point2-iterate-ℕ))))

  abstract
    not-not-eq-second-point-zero-min-reporting :
      ¬¬ (Id second-point-min-repeating zero-ℕ)
    not-not-eq-second-point-zero-min-reporting np =
      contradiction-le-ℕ
        ( pred-first)
        ( first-point-min-repeating)
        ( tr
          ( λ x  le-ℕ pred-first x)
          ( inv equality-pred-first)
          ( succ-le-ℕ pred-first))
        ( is-lower-bound-min-reporting
          ( pred-first)
          ( pair
            ( pred-second)
            ( pair
              ( tr
                ( λ x  le-ℕ (succ-ℕ pred-second) x)
                ( equality-pred-first)
                ( tr
                  ( λ x  le-ℕ x first-point-min-repeating)
                  ( equality-pred-second)
                  ( le-min-reporting)))
              ( is-injective-map-equiv
                ( f)
                ( tr
                  ( λ x 
                    Id ( iterate x (map-equiv f) a)
                       ( iterate (succ-ℕ pred-second) (map-equiv f) a))
                  ( equality-pred-first)
                  ( tr
                    ( λ x 
                      Id ( iterate first-point-min-repeating (map-equiv f) a)
                         ( iterate x (map-equiv f) a))
                    ( equality-pred-second)
                    ( same-image-iterate-min-reporting)))))))
      where
      is-successor-first-point-min-repeating :
        is-successor-ℕ first-point-min-repeating
      is-successor-first-point-min-repeating =
        is-successor-is-nonzero-ℕ
          ( is-nonzero-le-ℕ
              second-point-min-repeating
              first-point-min-repeating
              le-min-reporting)
      pred-first : 
      pred-first = pr1 is-successor-first-point-min-repeating
      equality-pred-first : Id first-point-min-repeating (succ-ℕ pred-first)
      equality-pred-first = pr2 is-successor-first-point-min-repeating
      is-successor-second-point-min-repeating :
        is-successor-ℕ second-point-min-repeating
      is-successor-second-point-min-repeating = is-successor-is-nonzero-ℕ np
      pred-second : 
      pred-second = pr1 is-successor-second-point-min-repeating
      equality-pred-second : Id second-point-min-repeating (succ-ℕ pred-second)
      equality-pred-second = pr2 is-successor-second-point-min-repeating

  has-finite-orbits-permutation' :
    is-decidable (Id second-point-min-repeating zero-ℕ) 
    Σ   k  (is-nonzero-ℕ k) × Id (iterate k (map-equiv f) a) a)
  pr1 (has-finite-orbits-permutation' (inl p)) = first-point-min-repeating
  pr1 (pr2 (has-finite-orbits-permutation' (inl p))) =
    is-nonzero-le-ℕ
      second-point-min-repeating
      first-point-min-repeating
      le-min-reporting
  pr2 (pr2 (has-finite-orbits-permutation' (inl p))) =
    tr
      ( λ x 
        Id ( iterate first-point-min-repeating (map-equiv f) a)
           ( iterate x (map-equiv f) a))
      ( p)
      ( same-image-iterate-min-reporting)
  has-finite-orbits-permutation' (inr np) =
    ex-falso (not-not-eq-second-point-zero-min-reporting np)
    where
    is-successor-first-point-min-repeating :
      is-successor-ℕ first-point-min-repeating
    is-successor-first-point-min-repeating =
      is-successor-is-nonzero-ℕ
        ( is-nonzero-le-ℕ
            second-point-min-repeating
            first-point-min-repeating
            le-min-reporting)
    pred-first : 
    pred-first = pr1 is-successor-first-point-min-repeating
    equality-pred-first : Id first-point-min-repeating (succ-ℕ pred-first)
    equality-pred-first = pr2 is-successor-first-point-min-repeating
    is-successor-second-point-min-repeating :
      is-successor-ℕ second-point-min-repeating
    is-successor-second-point-min-repeating = is-successor-is-nonzero-ℕ np
    pred-second : 
    pred-second = pr1 is-successor-second-point-min-repeating
    equality-pred-second : Id second-point-min-repeating (succ-ℕ pred-second)
    equality-pred-second = pr2 is-successor-second-point-min-repeating

  has-finite-orbits-permutation :
    Σ   k  (is-nonzero-ℕ k) × Id (iterate k (map-equiv f) a) a)
  has-finite-orbits-permutation =
    has-finite-orbits-permutation'
      ( has-decidable-equality-ℕ second-point-min-repeating zero-ℕ)

  leq-has-finite-orbits-permutation-number-elements :
    ( pr1 has-finite-orbits-permutation) ≤-ℕ (number-of-elements-count eX)
  leq-has-finite-orbits-permutation-number-elements =
    cases-second-point
      ( has-decidable-equality-ℕ second-point-min-repeating zero-ℕ)
    where
    cases-second-point :
      is-decidable (Id second-point-min-repeating zero-ℕ) 
      (pr1 has-finite-orbits-permutation) ≤-ℕ (number-of-elements-count eX)
    cases-second-point (inl p) =
      tr
        ( λ x 
          ( pr1 (has-finite-orbits-permutation' x)) ≤-ℕ
          ( number-of-elements-count eX))
        { x = inl p}
        { y = has-decidable-equality-ℕ second-point-min-repeating zero-ℕ}
        ( eq-is-prop
          ( is-prop-type-Prop
            ( is-decidable-Prop
              ( Id-Prop ℕ-Set second-point-min-repeating zero-ℕ))))
        ( leq-first-point-min-reporting-succ-number-elements)
    cases-second-point (inr np) =
      ex-falso (not-not-eq-second-point-zero-min-reporting np)

  mult-has-finite-orbits-permutation :
    (k : ) 
    Id (iterate (k *ℕ (pr1 has-finite-orbits-permutation)) (map-equiv f) a) a
  mult-has-finite-orbits-permutation zero-ℕ = refl
  mult-has-finite-orbits-permutation (succ-ℕ k) =
    ( iterate-add-ℕ
      ( k *ℕ (pr1 has-finite-orbits-permutation))
      ( pr1 has-finite-orbits-permutation)
      ( map-equiv f)
      ( a)) 
    ( ( ap
        ( iterate (k *ℕ (pr1 has-finite-orbits-permutation)) (map-equiv f))
        ( pr2 (pr2 has-finite-orbits-permutation))) 
      ( mult-has-finite-orbits-permutation k))

For finite types, the number of orbits-permutation of a permutation is finite

module _
  {l : Level} (n : ) (X : UU-Fin l n) (f : Aut (type-UU-Fin n X))
  where

  same-orbits-permutation : Eq-Rel l (type-UU-Fin n X)
  (pr1 same-orbits-permutation) a b =
    trunc-Prop (Σ   k  Id (iterate k (map-equiv f) a) b))
  pr1 (pr2 same-orbits-permutation) = unit-trunc-Prop (pair 0 refl)
  pr1 (pr2 (pr2 same-orbits-permutation)) {a} {b} P =
    apply-universal-property-trunc-Prop
      ( P)
      ( pr1 same-orbits-permutation b a)
      ( λ (pair k p) 
        apply-universal-property-trunc-Prop
          ( has-cardinality-type-UU-Fin n X)
          ( pr1 same-orbits-permutation b a)
          ( λ h 
            unit-trunc-Prop
              (pair
                ( pr1 (lemma h k))
                ( ( ap (iterate (pr1 (lemma h k)) (map-equiv f)) (inv p)) 
                  ( ( inv (iterate-add-ℕ (pr1 (lemma h k)) k (map-equiv f) a)) 
                    ( ( ap
                        ( λ x  iterate x (map-equiv f) a)
                        ( pr2 (lemma h k))) 
                      ( mult-has-finite-orbits-permutation
                        ( type-UU-Fin n X)
                        ( pair n h)
                        ( f)
                        ( a)
                        ( k))))))))
    where
    has-finite-orbits-permutation-a :
      (h : Fin n  type-UU-Fin n X) 
      Σ   l  (is-nonzero-ℕ l) × Id (iterate l (map-equiv f) a) a)
    has-finite-orbits-permutation-a h =
      has-finite-orbits-permutation (type-UU-Fin n X) (pair n h) f a
    lemma :
      (h : Fin n  type-UU-Fin n X) (k : ) 
      Σ ( )
        ( λ j 
          Id (j +ℕ k) (k *ℕ (pr1 (has-finite-orbits-permutation-a h))))
    lemma h k =
      subtraction-leq-ℕ
        ( k)
        ( k *ℕ (pr1 (has-finite-orbits-permutation-a h)))
        ( leq-mul-is-nonzero-ℕ
          ( pr1 (has-finite-orbits-permutation-a h))
          ( k)
          ( pr1 (pr2 (has-finite-orbits-permutation-a h))))
  pr2 (pr2 (pr2 same-orbits-permutation)) {a} {b} {c} P Q =
    apply-universal-property-trunc-Prop
      ( P)
      ( pr1 same-orbits-permutation a c)
      ( λ (pair k1 p) 
        apply-universal-property-trunc-Prop
          ( Q)
          ( pr1 same-orbits-permutation a c)
          ( λ { (pair k2 q) 
                ( unit-trunc-Prop
                  ( pair
                    ( k2 +ℕ k1)
                    ( (iterate-add-ℕ k2 k1 (map-equiv f) a) 
                      ( ap (iterate k2 (map-equiv f)) p  q))))}))

  abstract
    is-decidable-same-orbits-permutation :
      ( a b : type-UU-Fin n X) 
      is-decidable (sim-Eq-Rel same-orbits-permutation a b)
    is-decidable-same-orbits-permutation a b =
      apply-universal-property-trunc-Prop
        ( has-cardinality-type-UU-Fin n X)
        ( is-decidable-Prop (prop-Eq-Rel same-orbits-permutation a b))
        ( λ h 
          is-decidable-trunc-Prop-is-merely-decidable
            ( Σ   k  Id (iterate k (map-equiv f) a) b))
            ( unit-trunc-Prop
              ( is-decidable-iterate-is-decidable-bounded h a b
                ( is-decidable-bounded-Σ-ℕ n
                  ( λ z  z ≤-ℕ n)
                  ( λ z  Id (iterate z (map-equiv f) a) b)
                  ( λ z  is-decidable-leq-ℕ z n)
                  ( λ z 
                    has-decidable-equality-equiv
                      ( inv-equiv h)
                      ( has-decidable-equality-Fin n)
                      ( iterate z (map-equiv f) a)
                      ( b))
                  ( λ m p  p)))))
      where
      is-decidable-iterate-is-decidable-bounded :
        ( h : Fin n  type-UU-Fin n X) (a b : type-UU-Fin n X) 
        is-decidable
          ( Σ   m  (m ≤-ℕ n) × (Id (iterate m (map-equiv f) a) b))) 
        is-decidable (Σ   m  Id (iterate m (map-equiv f) a) b))
      is-decidable-iterate-is-decidable-bounded h a b (inl p) =
        inl (pair (pr1 p) (pr2 (pr2 p)))
      is-decidable-iterate-is-decidable-bounded h a b (inr np) =
        inr
          ( λ p 
            np
              ( pair
                ( remainder-euclidean-division-ℕ m (pr1 p))
                ( pair
                  ( leq-le-ℕ
                    ( remainder-euclidean-division-ℕ m (pr1 p))
                    ( n)
                    ( concatenate-le-leq-ℕ
                      { y = m}
                      ( strict-upper-bound-remainder-euclidean-division-ℕ
                        ( m)
                        ( pr1 p)
                        ( pr1
                          ( pr2
                            ( has-finite-orbits-permutation
                              ( type-UU-Fin n X)
                              ( pair n h)
                              ( f)
                              ( a)))))
                      ( leq-has-finite-orbits-permutation-number-elements
                        ( type-UU-Fin n X)
                        ( pair n h)
                        ( f)
                        ( a))))
                  ( ( ap
                      ( iterate
                        ( remainder-euclidean-division-ℕ m (pr1 p))
                        ( map-equiv f))
                      ( inv
                        ( mult-has-finite-orbits-permutation
                          ( type-UU-Fin n X)
                          ( pair n h)
                          ( f)
                          ( a)
                          ( quotient-euclidean-division-ℕ m (pr1 p))))) 
                    ( ( inv
                        ( iterate-add-ℕ
                          ( remainder-euclidean-division-ℕ m (pr1 p))
                          ( (quotient-euclidean-division-ℕ m (pr1 p)) *ℕ m)
                          ( map-equiv f)
                          ( a))) 
                      ( ( ap
                          ( λ x  iterate x (map-equiv f) a)
                          ( ( commutative-add-ℕ
                              ( remainder-euclidean-division-ℕ m (pr1 p))
                              ( quotient-euclidean-division-ℕ m (pr1 p) *ℕ m)) 
                            ( eq-euclidean-division-ℕ m (pr1 p)))) 
                        ( pr2 p)))))))
        where
        m : 
        m = pr1
            ( has-finite-orbits-permutation
              ( type-UU-Fin n X)
              ( pair n h)
              ( f)
              ( a))

  abstract
    is-decidable-is-in-equivalence-class-same-orbits-permutation :
      (T : equivalence-class same-orbits-permutation) 
      (a : type-UU-Fin n X) 
      is-decidable (is-in-equivalence-class same-orbits-permutation T a)
    is-decidable-is-in-equivalence-class-same-orbits-permutation T a =
      is-decidable-is-in-equivalence-class-is-decidable
        ( same-orbits-permutation)
        ( is-decidable-same-orbits-permutation)
        ( T)
        ( a)

  abstract
    has-finite-number-orbits-permutation :
      is-finite (equivalence-class same-orbits-permutation)
    has-finite-number-orbits-permutation =
      is-finite-codomain
        ( is-finite-type-UU-Fin n X)
        ( is-surjective-class same-orbits-permutation)
        ( apply-universal-property-trunc-Prop
          ( has-cardinality-type-UU-Fin n X)
          ( pair
            ( has-decidable-equality
              ( equivalence-class same-orbits-permutation))
            ( is-prop-has-decidable-equality))
        ( λ h T1 T2 
          apply-universal-property-trunc-Prop
          ( pr2 T1)
          ( is-decidable-Prop
            ( Id-Prop (equivalence-class-Set same-orbits-permutation) T1 T2))
          ( λ (pair t1 p1) 
            cases-decidable-equality T1 T2 t1
              ( eq-pair-Σ
                ( ap
                  ( subtype-equivalence-class
                    same-orbits-permutation)
                  ( eq-has-same-elements-equivalence-class
                    same-orbits-permutation T1
                      ( class same-orbits-permutation t1) p1))
                ( all-elements-equal-type-trunc-Prop _ _))
              ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                T2 t1))))
      where
      cases-decidable-equality :
        (T1 T2 : equivalence-class same-orbits-permutation)
        (t1 : type-UU-Fin n X) 
        Id T1 (class same-orbits-permutation t1) 
        is-decidable
          ( is-in-equivalence-class same-orbits-permutation T2 t1) 
        is-decidable (Id T1 T2)
      cases-decidable-equality T1 T2 t1 p1 (inl p) =
        inl
          ( ( p1) 
            ( map-inv-is-equiv
              ( is-equiv-is-in-equivalence-class-eq-equivalence-class
                  same-orbits-permutation t1 T2)
              ( p)))
      cases-decidable-equality T1 T2 t1 p1 (inr np) =
        inr
          ( λ p 
            np
              ( is-in-equivalence-class-eq-equivalence-class
                same-orbits-permutation t1 T2 (inv p1  p)))

  number-of-orbits-permutation : 
  number-of-orbits-permutation =
    number-of-elements-is-finite has-finite-number-orbits-permutation

  sign-permutation-orbit : Fin 2
  sign-permutation-orbit =
    iterate (n +ℕ number-of-orbits-permutation) (succ-Fin 2) (zero-Fin 1)
module _
  {l1 : Level} (X : UU l1) (eX : count X) (a b : X) (np : ¬ (Id a b))
  where

  composition-transposition-a-b : (X  X)  (X  X)
  composition-transposition-a-b g =
    ( standard-transposition (has-decidable-equality-count eX) np) ∘e g

  composition-transposition-a-b-involution :
    ( g : X  X) 
    htpy-equiv
      ( composition-transposition-a-b (composition-transposition-a-b g))
      ( g)
  composition-transposition-a-b-involution g x =
    is-involution-map-transposition
      ( standard-2-Element-Decidable-Subtype
        ( has-decidable-equality-count eX)
        ( np))
      ( map-equiv g x)

  same-orbits-permutation-count : (X  X)  Eq-Rel l1 X
  same-orbits-permutation-count =
    same-orbits-permutation
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX)))

  abstract
    minimal-element-iterate :
      (g : X  X) (x y : X)  Σ   k  Id (iterate k (map-equiv g) x) y) 
      minimal-element-ℕ  k  Id (iterate k (map-equiv g) x) y)
    minimal-element-iterate g x y =
      well-ordering-principle-ℕ
        ( λ k  Id (iterate k (map-equiv g) x) y)
        ( λ k  has-decidable-equality-count eX (iterate k (map-equiv g) x) y)

  abstract
    minimal-element-iterate-nonzero :
      (g : X  X) (x y : X) 
      Σ   k  is-nonzero-ℕ k × Id (iterate k (map-equiv g) x) y) 
      minimal-element-ℕ
        ( λ k  is-nonzero-ℕ k × Id (iterate k (map-equiv g) x) y)
    minimal-element-iterate-nonzero g x y =
      well-ordering-principle-ℕ
        ( λ k  is-nonzero-ℕ k × Id (iterate k (map-equiv g) x) y)
        ( λ k 
          is-decidable-prod
            ( is-decidable-neg (has-decidable-equality-ℕ k zero-ℕ))
            ( has-decidable-equality-count eX (iterate k (map-equiv g) x) y))

  abstract
    minimal-element-iterate-2 :
      (g : X  X) (x y z : X) 
      Σ ( )
        ( λ k 
          ( Id (iterate k (map-equiv g) x) y) +
          ( Id (iterate k (map-equiv g) x) z)) 
      minimal-element-ℕ
        ( λ k 
          ( Id (iterate k (map-equiv g) x) y) +
          ( Id (iterate k (map-equiv g) x) z))
    minimal-element-iterate-2 g x y z p =
      well-ordering-principle-ℕ
        ( λ k 
          ( Id (iterate k (map-equiv g) x) y) +
          ( Id (iterate k (map-equiv g) x) z))
        ( λ k 
          is-decidable-coprod
          ( has-decidable-equality-count eX (iterate k (map-equiv g) x) y)
          ( has-decidable-equality-count eX (iterate k (map-equiv g) x) z))
        ( p)

  abstract
    equal-iterate-transposition :
      {l2 : Level} (x : X) (g : X  X) (C :   UU l2)
      ( F :
        (k : )  C k 
        ( ¬ (Id (iterate k (map-equiv g) x) a)) ×
        ( ¬ (Id (iterate k (map-equiv g) x) b)))
      ( Ind :
        (n : )  C (succ-ℕ n)  is-nonzero-ℕ n  C n) 
      (k : )  (is-zero-ℕ k + C k) 
      Id ( iterate k (map-equiv (composition-transposition-a-b g)) x)
         ( iterate k (map-equiv g) x)
    equal-iterate-transposition x g C F Ind zero-ℕ p = refl
    equal-iterate-transposition x g C F Ind (succ-ℕ k) (inl p) =
      ex-falso (is-nonzero-succ-ℕ k p)
    equal-iterate-transposition x g C F Ind (succ-ℕ k) (inr p) =
      cases-equal-iterate-transposition
        ( has-decidable-equality-count eX
          ( iterate (succ-ℕ k) (map-equiv g) x)
          ( a))
        ( has-decidable-equality-count eX
          ( iterate (succ-ℕ k) (map-equiv g) x)
          ( b))
      where
      induction-cases-equal-iterate-transposition :
        is-decidable (Id k zero-ℕ) 
        Id ( iterate k (map-equiv (composition-transposition-a-b g)) x)
           ( iterate k (map-equiv g) x)
      induction-cases-equal-iterate-transposition (inl s) =
        tr
          ( λ k 
            Id (iterate k (map-equiv (composition-transposition-a-b g)) x)
            (iterate k (map-equiv g) x))
          ( inv s)
          ( refl)
      induction-cases-equal-iterate-transposition (inr s) =
        equal-iterate-transposition x g C F Ind k (inr (Ind k p s))
      cases-equal-iterate-transposition :
        is-decidable (Id (iterate (succ-ℕ k) (map-equiv g) x) a) 
        is-decidable (Id (iterate (succ-ℕ k) (map-equiv g) x) b) 
        Id
          ( iterate (succ-ℕ k) (map-equiv (composition-transposition-a-b g)) x)
          ( iterate (succ-ℕ k) (map-equiv g) x)
      cases-equal-iterate-transposition (inl q) r =
        ex-falso (pr1 (F (succ-ℕ k) p) q)
      cases-equal-iterate-transposition (inr q) (inl r) =
        ex-falso (pr2 (F (succ-ℕ k) p) r)
      cases-equal-iterate-transposition (inr q) (inr r) =
        ( ap
          ( λ n 
            iterate n (map-equiv (composition-transposition-a-b g)) x)
          ( commutative-add-ℕ k (succ-ℕ zero-ℕ))) 
        ( ( iterate-add-ℕ
            ( succ-ℕ zero-ℕ)
            ( k)
            ( map-equiv (composition-transposition-a-b g))
            ( x)) 
          ( ( ap
              ( map-equiv (composition-transposition-a-b g))
              ( induction-cases-equal-iterate-transposition
                ( has-decidable-equality-ℕ k zero-ℕ))) 
            ( is-fixed-point-standard-transposition
              ( has-decidable-equality-count eX)
              ( np)
              ( iterate (succ-ℕ k) (map-equiv g) x)
              ( λ q'  q (inv q'))
              ( λ r'  r (inv r')))))

  abstract
    conserves-other-orbits-transposition :
      (g : X  X) (x y : X) 
      ¬ (sim-Eq-Rel (same-orbits-permutation-count g) x a) 
      ¬ (sim-Eq-Rel (same-orbits-permutation-count g) x b) 
      ( ( sim-Eq-Rel (same-orbits-permutation-count g) x y) 
        ( sim-Eq-Rel
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( x)
          ( y)))
    conserves-other-orbits-transposition g x y NA NB =
      pair
        ( λ P'  apply-universal-property-trunc-Prop P'
          ( prop-Eq-Rel
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( x)
            ( y))
          ( λ (pair k p)  unit-trunc-Prop
            (pair k
              ( (equal-iterate-transposition-other-orbits k) 
                ( p)))))
        ( is-equiv-is-prop is-prop-type-trunc-Prop is-prop-type-trunc-Prop
          ( λ P'  apply-universal-property-trunc-Prop P'
            ( prop-Eq-Rel (same-orbits-permutation-count g) x y)
            ( λ (pair k p)  unit-trunc-Prop
              ( pair k
                ( (inv (equal-iterate-transposition-other-orbits k)) 
                  ( p))))))
      where
      equal-iterate-transposition-other-orbits :
        (k : ) 
        Id
          ( iterate k (map-equiv (composition-transposition-a-b g)) x)
          ( iterate k (map-equiv g) x)
      equal-iterate-transposition-other-orbits k =
        equal-iterate-transposition x g  k'  unit)
           k' _ 
            pair
              ( λ q  NA (unit-trunc-Prop (pair k' q)))
              ( λ r  NB (unit-trunc-Prop (pair k' r))))
           _ _ _  star) k (inr star)

  conserves-other-orbits-transposition-quotient :
    (g : X  X)
    (T : equivalence-class (same-orbits-permutation-count g)) 
    ¬ (is-in-equivalence-class (same-orbits-permutation-count g) T a) 
    ¬ (is-in-equivalence-class (same-orbits-permutation-count g) T b) 
    equivalence-class
      ( same-orbits-permutation-count (composition-transposition-a-b g))
  pr1 (conserves-other-orbits-transposition-quotient g T nq nr) = pr1 T
  pr2 (conserves-other-orbits-transposition-quotient g (pair T1 T2) nq nr) =
    apply-universal-property-trunc-Prop
      ( T2)
      ( is-equivalence-class-Prop
        ( same-orbits-permutation-count (composition-transposition-a-b g))
        ( T1))
      ( λ (pair x Q) 
        unit-trunc-Prop
          ( pair x
            ( λ y 
              iff-equiv
                ( ( conserves-other-orbits-transposition g x y
                    ( nq  backward-implication (Q a))
                    ( nr  backward-implication (Q b))) ∘e
                  ( equiv-iff'
                    ( T1 y)
                    ( prop-Eq-Rel (same-orbits-permutation-count g) x y)
                    ( Q y))))))

  abstract
    not-same-orbits-transposition-same-orbits :
      ( g : X  X)
      ( P :
        ( sim-Eq-Rel
          ( same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g))
          ( a)
          ( b))) 
      ¬ ( sim-Eq-Rel
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( a)
          ( b))
    not-same-orbits-transposition-same-orbits g P Q =
      apply-universal-property-trunc-Prop Q empty-Prop
        ( λ (pair k2 q) 
          ( apply-universal-property-trunc-Prop P empty-Prop
            ( λ p  lemma3 p k2 q)))
      where
      neq-iterate-nonzero-le-minimal-element :
        ( pa : Σ   k  Id (iterate k (map-equiv g) a) b))
        ( k : ) 
        ( is-nonzero-ℕ k × le-ℕ k (pr1 (minimal-element-iterate g a b pa))) 
        ¬ (iterate k (map-equiv g) a  a) × ¬ (iterate k (map-equiv g) a  b)
      pr1 (neq-iterate-nonzero-le-minimal-element pa k (pair nz ineq)) q =
        contradiction-le-ℕ
          ( pr1 pair-k2)
          ( pr1 (minimal-element-iterate g a b pa))
          ( le-subtraction-ℕ
            ( pr1 (pair-k2))
            ( pr1 (minimal-element-iterate g a b pa))
            ( k)
            ( nz)
            ( commutative-add-ℕ k (pr1 (pair-k2))  pr2 (pr2 pair-k2)))
          ( pr2
            ( pr2 (minimal-element-iterate g a b pa))
            ( pr1 pair-k2)
            ( ( ap (iterate (pr1 pair-k2) (map-equiv g)) (inv q)) 
              ( (inv (iterate-add-ℕ (pr1 pair-k2) k (map-equiv g) a)) 
                ( ap
                  ( λ n  iterate n (map-equiv g) a)
                  ( pr2 (pr2 pair-k2)) 
                  pr1 (pr2 (minimal-element-iterate g a b pa))))))
        where
        pair-k2 :
          Σ ( )
            ( λ l 
              is-nonzero-ℕ l ×
              Id (l +ℕ k) (pr1 (minimal-element-iterate g a b pa)))
        pair-k2 =
          (subtraction-le-ℕ k (pr1 (minimal-element-iterate g a b pa)) ineq)
      pr2 (neq-iterate-nonzero-le-minimal-element pa k (pair nz ineq)) r =
        ex-falso
          ( contradiction-le-ℕ k (pr1 (minimal-element-iterate g a b pa))
            ineq (pr2 (pr2 (minimal-element-iterate g a b pa)) k r))
      equal-iterate-transposition-a :
        (pa : Σ   k  Id (iterate k (map-equiv g) a) b)) (k : ) 
        le-ℕ k (pr1 (minimal-element-iterate g a b pa)) 
        ( Id
          ( iterate k (map-equiv (composition-transposition-a-b g)) a)
          ( iterate k (map-equiv g) a))
      equal-iterate-transposition-a pa k ineq =
        equal-iterate-transposition a g
          ( λ k' 
            ( is-nonzero-ℕ k') ×
            ( le-ℕ k' (pr1 (minimal-element-iterate g a b pa))))
          ( neq-iterate-nonzero-le-minimal-element pa)
          ( λ n (pair _ s) nz 
            pair
              ( nz)
              ( transitive-le-ℕ n
                ( succ-ℕ n)
                ( pr1 (minimal-element-iterate g a b pa))
                ( succ-le-ℕ n) s))
          ( k)
          ( cases-equal-iterate-transposition-a
            ( has-decidable-equality-ℕ k zero-ℕ))
        where
        cases-equal-iterate-transposition-a :
          is-decidable (is-zero-ℕ k) 
          ( is-zero-ℕ k) +
          ( is-nonzero-ℕ k × le-ℕ k (pr1 (minimal-element-iterate g a b pa)))
        cases-equal-iterate-transposition-a (inl s) = inl s
        cases-equal-iterate-transposition-a (inr s) = inr (pair s ineq)
      lemma2 :
        ( pa : Σ   k  Id (iterate k (map-equiv g) a) b)) 
        is-decidable (Id (pr1 (minimal-element-iterate g a b pa)) zero-ℕ) 
        Id
          ( iterate
            ( pr1 (minimal-element-iterate g a b pa))
            ( map-equiv (composition-transposition-a-b g))
            ( a))
          ( a)
      lemma2 pa (inl p) =
        ex-falso
          ( np
            ( tr
              ( λ v  Id (iterate v (map-equiv g) a) b)
              ( p)
              ( pr1 (pr2 (minimal-element-iterate g a b pa)))))
      lemma2 pa (inr p) =
        ( ap
          ( λ n  iterate n (map-equiv (composition-transposition-a-b g)) a)
          ( pr2 (is-successor-k1) 
            commutative-add-ℕ (pr1 is-successor-k1) (succ-ℕ zero-ℕ))) 
          ( ( iterate-add-ℕ
              ( succ-ℕ zero-ℕ)
              ( pr1 is-successor-k1)
              ( map-equiv (composition-transposition-a-b g)) a) 
            ( ( ap
                ( map-equiv (composition-transposition-a-b g))
                ( equal-iterate-transposition-a pa (pr1 is-successor-k1)
                  ( tr
                    ( le-ℕ (pr1 is-successor-k1))
                    ( inv (pr2 is-successor-k1))
                    ( succ-le-ℕ (pr1 is-successor-k1))))) 
              ( ( ap
                  ( λ n 
                    map-standard-transposition
                      ( has-decidable-equality-count eX)
                      ( np)
                      ( iterate n (map-equiv g) a))
                  ( inv (pr2 is-successor-k1))) 
                ( ( ap
                    ( map-standard-transposition
                      ( has-decidable-equality-count eX) np)
                    ( pr1 (pr2 (minimal-element-iterate g a b pa)))) 
                  ( right-computation-standard-transposition
                    ( has-decidable-equality-count eX)
                    ( np))))))
        where
        is-successor-k1 :
          is-successor-ℕ (pr1 (minimal-element-iterate g a b pa))
        is-successor-k1 = is-successor-is-nonzero-ℕ p
      mult-lemma2 :
        ( pa : Σ   k  Id (iterate k (map-equiv g) a) b)) (k : ) 
        Id
          ( iterate
            ( k *ℕ (pr1 (minimal-element-iterate g a b pa)))
            ( map-equiv (composition-transposition-a-b g))
            ( a))
          ( a)
      mult-lemma2 pa zero-ℕ = refl
      mult-lemma2 pa (succ-ℕ k) =
        ( iterate-add-ℕ
          ( k *ℕ (pr1 (minimal-element-iterate g a b pa)))
          ( pr1 (minimal-element-iterate g a b pa))
          ( map-equiv (composition-transposition-a-b g)) a) 
        ( ap
          ( iterate
            ( k *ℕ (pr1 (minimal-element-iterate g a b pa)))
            ( map-equiv (composition-transposition-a-b g)))
          ( lemma2
            ( pa)
            ( has-decidable-equality-ℕ
              ( pr1 (minimal-element-iterate g a b pa))
              ( zero-ℕ))) 
          ( mult-lemma2 pa k))
      lemma3 :
        ( pa : Σ   k  Id (iterate k (map-equiv g) a) b)) (k : ) 
        ¬ (Id (iterate k (map-equiv (composition-transposition-a-b g)) a) b)
      lemma3 pa k q =
        contradiction-le-ℕ
          ( r)
          ( pr1 (minimal-element-iterate g a b pa))
          ( ineq)
          ( pr2
            ( pr2 (minimal-element-iterate g a b pa))
            ( r)
            ( inv (equal-iterate-transposition-a pa r ineq) 
              ( ( ap
                  ( iterate r (map-equiv (composition-transposition-a-b g)))
                  ( inv (mult-lemma2 pa quo))) 
                ( (inv
                    ( iterate-add-ℕ
                      ( r)
                      ( quo *ℕ (pr1 (minimal-element-iterate g a b pa)))
                      ( map-equiv (composition-transposition-a-b g)) a)) 
                  ( ( ap
                      ( λ n 
                        iterate
                          ( n)
                          ( map-equiv (composition-transposition-a-b g))
                          ( a))
                      ( commutative-add-ℕ
                        ( r)
                        ( quo *ℕ (pr1 (minimal-element-iterate g a b pa))) 
                        ( eq-euclidean-division-ℕ
                          ( pr1 (minimal-element-iterate g a b pa))
                          ( k)))) 
                    ( q))))))
        where
        r : 
        r =
          remainder-euclidean-division-ℕ
            ( pr1 (minimal-element-iterate g a b pa))
            ( k)
        quo : 
        quo =
          quotient-euclidean-division-ℕ
            ( pr1 (minimal-element-iterate g a b pa))
            ( k)
        ineq : le-ℕ r (pr1 (minimal-element-iterate g a b pa))
        ineq =
          strict-upper-bound-remainder-euclidean-division-ℕ
            ( pr1 (minimal-element-iterate g a b pa))
            ( k)
            ( λ p 
              np
              ( tr
                ( λ v  Id (iterate v (map-equiv g) a) b)
                ( p)
                ( pr1 (pr2 (minimal-element-iterate g a b pa)))))

  coprod-sim-Eq-Rel-a-b-Prop :
    ( g : X  X) 
    ( P :
      sim-Eq-Rel
        ( same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g))
        ( a)
        ( b))
    (x : X)  Prop l1
  coprod-sim-Eq-Rel-a-b-Prop g P x =
    coprod-Prop
      ( prop-Eq-Rel
        (same-orbits-permutation-count (composition-transposition-a-b g)) x a)
      ( prop-Eq-Rel
        (same-orbits-permutation-count (composition-transposition-a-b g)) x b)
      ( λ T1 T2  not-same-orbits-transposition-same-orbits g P
        ( trans-Eq-Rel
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( symm-Eq-Rel
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( T1))
          ( T2)))

  abstract
    split-orbits-a-b-transposition :
      (g : X  X) 
      (P :
        sim-Eq-Rel
          ( same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g))
          ( a)
          ( b))
      (x : X) 
      ( ( sim-Eq-Rel (same-orbits-permutation-count g) x a) 
        ( ( sim-Eq-Rel
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( x)
            ( a)) +
          ( sim-Eq-Rel
            ( same-orbits-permutation-count
              ( composition-transposition-a-b g))
            ( x)
            ( b))))
    split-orbits-a-b-transposition g P x =
      pair
        ( λ T 
          apply-universal-property-trunc-Prop T
            ( coprod-sim-Eq-Rel-a-b-Prop g P x)
             pa  lemma2 g (pair (pr1 pa) (inl (pr2 pa)))))
        ( is-equiv-is-prop is-prop-type-trunc-Prop
          ( is-prop-type-Prop (coprod-sim-Eq-Rel-a-b-Prop g P x))
          ( λ {
            (inl T) 
            apply-universal-property-trunc-Prop T
              ( prop-Eq-Rel (same-orbits-permutation-count g) x a)
              ( λ pa 
                lemma3
                  ( lemma2
                    ( composition-transposition-a-b g)
                    ( pair (pr1 pa) (inl (pr2 pa))))) ;
            (inr T) 
            apply-universal-property-trunc-Prop T
              ( prop-Eq-Rel (same-orbits-permutation-count g) x a)
              ( λ pa 
                lemma3
                  ( lemma2
                    ( composition-transposition-a-b g)
                    ( pair (pr1 pa) (inr (pr2 pa)))))}))
      where
      minimal-element-iterate-2-a-b :
        ( g : X  X) 
        ( Σ ( )
            ( λ k 
              ( Id (iterate k (map-equiv g) x) a) +
              ( Id (iterate k (map-equiv g) x) b))) 
        minimal-element-ℕ
          ( λ k 
            ( Id (iterate k (map-equiv g) x) a) +
            ( Id (iterate k (map-equiv g) x) b))
      minimal-element-iterate-2-a-b g = minimal-element-iterate-2 g x a b
      equal-iterate-transposition-same-orbits :
        ( g : X  X)
        ( pa :
          Σ ( )
            ( λ k 
              ( Id (iterate k (map-equiv g) x) a) +
              ( Id (iterate k (map-equiv g) x) b)))
        ( k : ) 
        ( le-ℕ k (pr1 (minimal-element-iterate-2-a-b g pa))) 
        Id
          ( iterate k (map-equiv (composition-transposition-a-b g)) x)
          ( iterate k (map-equiv g) x)
      equal-iterate-transposition-same-orbits g pa k ineq =
        equal-iterate-transposition x g
          ( λ k'  le-ℕ k' (pr1 (minimal-element-iterate-2-a-b g pa)))
          ( λ k' p  pair
            ( λ q 
              contradiction-le-ℕ k'
                ( pr1 (minimal-element-iterate-2-a-b g pa))
                ( p)
                ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inl q)))
            ( λ r 
              contradiction-le-ℕ k'
                ( pr1 (minimal-element-iterate-2-a-b g pa))
                ( p)
                ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inr r))))
          ( λ k' ineq' _ 
            transitive-le-ℕ k'
              ( succ-ℕ k')
              ( pr1 (minimal-element-iterate-2-a-b g pa))
              ( succ-le-ℕ k')
              ( ineq'))
          k (inr ineq)
      lemma2 :
        ( g : X  X)
        ( pa :
          Σ ( )
             k 
              ( Id (iterate k (map-equiv g) x) a) +
              ( Id (iterate k (map-equiv g) x) b))) 
        ( sim-Eq-Rel
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( x)
          ( a)) +
        ( sim-Eq-Rel
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( x)
          ( b))
      lemma2 g pa =
        cases-lemma2
          ( has-decidable-equality-ℕ
            ( pr1 (minimal-element-iterate-2-a-b g pa))
            ( zero-ℕ))
          ( pr1 (pr2 (minimal-element-iterate-2-a-b g pa)))
          ( refl)
        where
        cases-lemma2 :
          is-decidable (Id (pr1 (minimal-element-iterate-2-a-b g pa)) zero-ℕ) 
          (c :
            ( Id
              ( iterate
                ( pr1 (minimal-element-iterate-2-a-b g pa))
                ( map-equiv g)
                ( x))
              ( a)) +
            ( Id
              ( iterate
                ( pr1 (minimal-element-iterate-2-a-b g pa))
                ( map-equiv g)
                ( x))
              ( b))) 
          Id c (pr1 (pr2 (minimal-element-iterate-2-a-b g pa))) 
          ( sim-Eq-Rel
            ( same-orbits-permutation-count
              ( composition-transposition-a-b g))
            ( x)
            ( a)) +
          ( sim-Eq-Rel
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( x)
            ( b))
        cases-lemma2 (inl q) (inl c) r =
          inl
            ( unit-trunc-Prop
              ( pair zero-ℕ (tr  z  Id (iterate z (map-equiv g) x) a) q c)))
        cases-lemma2 (inl q) (inr c) r =
          inr
            ( unit-trunc-Prop
              ( pair zero-ℕ (tr  z  Id (iterate z (map-equiv g) x) b) q c)))
        cases-lemma2 (inr q) (inl c) r =
          inr (unit-trunc-Prop
            ( pair
              ( pr1 (minimal-element-iterate-2-a-b g pa))
              ( ap
                ( λ n 
                  iterate n (map-equiv (composition-transposition-a-b g)) x)
                ( pr2 (is-successor-k1) 
                  commutative-add-ℕ (pr1 is-successor-k1) (succ-ℕ zero-ℕ)) 
                ( iterate-add-ℕ
                  ( succ-ℕ zero-ℕ)
                  ( pr1 is-successor-k1)
                  ( map-equiv (composition-transposition-a-b g))
                  ( x) 
                  ( ap
                    ( map-equiv (composition-transposition-a-b g))
                    ( equal-iterate-transposition-same-orbits
                      ( g)
                      ( pa)
                      ( pr1 is-successor-k1)
                      ( tr
                        ( le-ℕ (pr1 is-successor-k1))
                        ( inv (pr2 is-successor-k1))
                        ( succ-le-ℕ (pr1 is-successor-k1)))) 
                    ( ap
                      ( λ n 
                        map-standard-transposition
                          ( has-decidable-equality-count eX)
                          ( np)
                          ( iterate n (map-equiv g) x))
                      ( inv (pr2 is-successor-k1)) 
                      ( ap
                        ( map-standard-transposition
                          ( has-decidable-equality-count eX)
                          ( np))
                        ( c) 
                        left-computation-standard-transposition
                          ( has-decidable-equality-count eX)
                          ( np))))))))
          where
          is-successor-k1 :
            is-successor-ℕ (pr1 (minimal-element-iterate-2-a-b g pa))
          is-successor-k1 = is-successor-is-nonzero-ℕ q
        cases-lemma2 (inr q) (inr c) r = inl (unit-trunc-Prop
          ( pair
            ( pr1 (minimal-element-iterate-2-a-b g pa))
            ( ap
              ( λ n  iterate n (map-equiv (composition-transposition-a-b g)) x)
              ( pr2 (is-successor-k1) 
                commutative-add-ℕ (pr1 is-successor-k1) (succ-ℕ zero-ℕ)) 
              ( (iterate-add-ℕ
                  ( succ-ℕ zero-ℕ)
                  ( pr1 is-successor-k1)
                  ( map-equiv (composition-transposition-a-b g))
                  ( x)) 
                ( ap
                  ( map-equiv (composition-transposition-a-b g))
                  ( equal-iterate-transposition-same-orbits
                    ( g)
                    ( pa)
                    ( pr1 is-successor-k1)
                    ( tr
                      ( le-ℕ (pr1 is-successor-k1))
                      ( inv (pr2 is-successor-k1))
                      ( succ-le-ℕ (pr1 is-successor-k1)))) 
                  ( ap
                    ( λ n 
                      map-standard-transposition
                        ( has-decidable-equality-count eX)
                        ( np)
                        ( iterate n (map-equiv g) x))
                    ( inv (pr2 is-successor-k1)) 
                    ( ( ap
                        ( map-standard-transposition
                          ( has-decidable-equality-count eX)
                          ( np))
                        ( c)) 
                      right-computation-standard-transposition
                        ( has-decidable-equality-count eX)
                        ( np))))))))
          where
          is-successor-k1 :
            is-successor-ℕ (pr1 (minimal-element-iterate-2-a-b g pa))
          is-successor-k1 = is-successor-is-nonzero-ℕ q
      lemma3 :
        ( ( sim-Eq-Rel
            ( same-orbits-permutation-count
              ( composition-transposition-a-b
                ( composition-transposition-a-b g)))
            ( x)
            ( a)) +
          ( sim-Eq-Rel
            ( same-orbits-permutation-count
              ( composition-transposition-a-b
                ( composition-transposition-a-b g)))
            ( x)
            ( b))) 
          sim-Eq-Rel (same-orbits-permutation-count g) x a
      lemma3 (inl T) =
        tr
           f  sim-Eq-Rel (same-orbits-permutation-count f) x a)
          { x = composition-transposition-a-b (composition-transposition-a-b g)}
          {y = g}
          ( eq-htpy-equiv (composition-transposition-a-b-involution g))
          ( T)
      lemma3 (inr T) =
        trans-Eq-Rel
          ( same-orbits-permutation-count g)
          ( tr
            ( λ g  sim-Eq-Rel (same-orbits-permutation-count g) x b)
            { x =
              composition-transposition-a-b (composition-transposition-a-b g)}
            {y = g}
            ( eq-htpy-equiv (composition-transposition-a-b-involution g))
            ( T))
          ( symm-Eq-Rel (same-orbits-permutation-count g) P)

  private
    module _
      ( g : X  X)
      ( P :
        sim-Eq-Rel
          ( same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g))
          ( a)
          ( b))
      ( h :
        count
          ( equivalence-class
            ( same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( g))))
      where

      h'-inl :
        ( k : Fin (number-of-elements-count h))
        ( T : equivalence-class (same-orbits-permutation-count g)) 
        Id (map-equiv-count h k) T 
        is-decidable
          ( is-in-equivalence-class (same-orbits-permutation-count g) T a) 
        is-decidable
          ( is-in-equivalence-class (same-orbits-permutation-count g) T b) 
        equivalence-class
          ( same-orbits-permutation-count (composition-transposition-a-b g))
      h'-inl k T p (inl q) r =
        class
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( a)
      h'-inl k T p (inr nq) (inl r) =
        ex-falso
          ( nq
            ( transitive-is-in-equivalence-class
              ( same-orbits-permutation-count g)
              ( T)
              ( b)
              ( a)
              ( r)
              ( symm-Eq-Rel (same-orbits-permutation-count g) P)))
      h'-inl k T p (inr nq) (inr nr) =
        conserves-other-orbits-transposition-quotient g T nq nr
      h' :
        Fin (succ-ℕ (number-of-elements-count h)) 
        equivalence-class
          ( same-orbits-permutation-count (composition-transposition-a-b g))

      h' (inl k) = h'-inl k (map-equiv-count h k) refl
        ( is-decidable-is-in-equivalence-class-same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g)
          ( map-equiv-count h k)
          ( a))
        ( is-decidable-is-in-equivalence-class-same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g)
          ( map-equiv-count h k)
          ( b))
      h' (inr k) =
        class
          ( same-orbits-permutation-count (composition-transposition-a-b g))
          ( b)

      cases-inv-h' :
        ( T :
          equivalence-class
          ( same-orbits-permutation-count (composition-transposition-a-b g))) 
        is-decidable
          ( is-in-equivalence-class
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( T)
            ( a)) 
        is-decidable
          ( is-in-equivalence-class
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( T)
            ( b)) 
        Fin (succ-ℕ (number-of-elements-count h))
      cases-inv-h' T (inl Q) R =
        inl
          ( map-inv-equiv-count h (class (same-orbits-permutation-count g) a))
      cases-inv-h' T (inr NQ) (inl R) = inr star
      cases-inv-h' T (inr NQ) (inr NR) =
        inl
          ( map-inv-equiv-count h
            ( pair
              ( pr1 T)
              ( tr
                ( λ f 
                  is-equivalence-class
                    ( same-orbits-permutation-count f)
                    ( pr1 T))
                { x =
                  composition-transposition-a-b
                    ( composition-transposition-a-b g)}
                { y = g}
                ( eq-htpy-equiv (composition-transposition-a-b-involution g))
                ( pr2
                  ( conserves-other-orbits-transposition-quotient
                    (composition-transposition-a-b g) T NQ NR)))))

      inv-h' :
        ( T :
          equivalence-class
            ( same-orbits-permutation-count
              ( composition-transposition-a-b g))) 
        Fin (succ-ℕ (number-of-elements-count h))
      inv-h' T =
        cases-inv-h' T
          ( is-decidable-is-in-equivalence-class-same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)
            ( T)
            ( a))
          ( is-decidable-is-in-equivalence-class-same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)
            ( T)
            ( b))
      H-conserves :
        ( T :
          equivalence-class
            ( same-orbits-permutation-count (composition-transposition-a-b g)))
        ( NQ :
          ¬ ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( T)
              ( a)))
        ( NR :
          ¬ ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( T)
              ( b))) 
        is-equivalence-class (same-orbits-permutation-count g) (pr1 T)
      H-conserves T NQ NR =
        tr
          ( λ f 
            is-equivalence-class (same-orbits-permutation-count f) (pr1 T))
          { x = composition-transposition-a-b (composition-transposition-a-b g)}
          { y = g}
          ( eq-htpy-equiv (composition-transposition-a-b-involution g))
          ( pr2
            ( conserves-other-orbits-transposition-quotient
              (composition-transposition-a-b g) T NQ NR))

      retr-h'-inr-inr :
        ( T :
          equivalence-class
            ( same-orbits-permutation-count (composition-transposition-a-b g)))
        ( NQ :
          ¬ ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( T)
              ( a)))
        ( NR :
          ¬ ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( T)
              ( b))) 
        is-decidable
          ( is-in-equivalence-class
            ( same-orbits-permutation-count g)
            ( pair (pr1 T) (H-conserves T NQ NR))
            ( a)) 
        is-decidable
          ( is-in-equivalence-class
            ( same-orbits-permutation-count g)
            ( pair (pr1 T) (H-conserves T NQ NR))
            ( b)) 
        Id
          ( h' (inl (map-inv-equiv-count h
            ( pair
              ( pr1 T)
              ( tr
                ( λ f 
                  is-equivalence-class
                    ( same-orbits-permutation-count f)
                    ( pr1 T))
                { x =
                  composition-transposition-a-b
                     (composition-transposition-a-b g)}
                {y = g}
                ( eq-htpy-equiv (composition-transposition-a-b-involution g))
                ( pr2
                  ( conserves-other-orbits-transposition-quotient
                    (composition-transposition-a-b g) T NQ NR)))))))
          ( T)
      retr-h'-inr-inr T NQ NR (inl Q') R' = ex-falso (NQ Q')
      retr-h'-inr-inr T NQ NR (inr NQ') (inl R') = ex-falso (NR R')
      retr-h'-inr-inr T NQ NR (inr NQ') (inr NR') =
        ( ap
          ( λ w 
            h'-inl
              ( map-inv-equiv-count h (pair (pr1 T) (H-conserves T NQ NR)))
              ( map-equiv (pr1 w) (pair (pr1 T) (H-conserves T NQ NR)))
              ( pr2 w)
              ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( g)
                  ( map-equiv (pr1 w) (pair (pr1 T) (H-conserves T NQ NR)))
                  ( a))
              ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( g)
                  ( map-equiv (pr1 w) (pair (pr1 T) (H-conserves T NQ NR)))
                  ( b)))
          { x = pair ((equiv-count h) ∘e (inv-equiv-count h)) refl}
          { y = pair
            id-equiv
              ( ap
                ( λ f  map-equiv f (pair (pr1 T) (H-conserves T NQ NR)))
                ( right-inverse-law-equiv (equiv-count h)))}
          ( eq-pair-Σ
            ( right-inverse-law-equiv (equiv-count h))
            ( eq-is-prop
              ( is-prop-type-Prop
                ( Id-Prop
                  ( equivalence-class-Set (same-orbits-permutation-count g))
                  ( map-equiv-count
                    ( h)
                    ( map-inv-equiv-count
                      ( h)
                      ( pair (pr1 T) (H-conserves T NQ NR))))
                  ( pair (pr1 T) (H-conserves T NQ NR))))))) 
          ( ap
             w 
              h'-inl
                ( map-inv-equiv-count h (pair (pr1 T) (H-conserves T NQ NR)))
                ( pair (pr1 T) (H-conserves T NQ NR))
                ( ap
                  ( λ f  map-equiv f (pair (pr1 T) (H-conserves T NQ NR)))
                  ( right-inverse-law-equiv (equiv-count h)))
                ( w)
                ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( g)
                  ( pair (pr1 T) (H-conserves T NQ NR))
                  ( b)))
            { x =
              is-decidable-is-in-equivalence-class-same-orbits-permutation
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( g)
                ( pair (pr1 T) (H-conserves T NQ NR))
                ( a)}
            { y = inr NQ'}
            ( eq-is-prop
              ( is-prop-is-decidable
                ( is-prop-is-in-equivalence-class
                  ( same-orbits-permutation-count g)
                  ( pair (pr1 T) (H-conserves T NQ NR))
                  ( a)))) 
            ( (ap
              ( λ w 
                h'-inl
                  ( map-inv-equiv-count h (pair (pr1 T) (H-conserves T NQ NR)))
                  ( pair (pr1 T) (H-conserves T NQ NR))
                  ( ap
                    ( λ f  map-equiv f (pair (pr1 T) (H-conserves T NQ NR)))
                    ( right-inverse-law-equiv (equiv-count h)))
                  ( inr NQ')
                  ( w))
              { x =
                is-decidable-is-in-equivalence-class-same-orbits-permutation
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( g)
                  ( pair (pr1 T) (H-conserves T NQ NR))
                  ( b)}
              { y = inr NR'}
              ( eq-is-prop
                ( is-prop-is-decidable
                  ( is-prop-is-in-equivalence-class
                    ( same-orbits-permutation-count g)
                    ( pair (pr1 T) (H-conserves T NQ NR))
                    ( b)))) 
              ( eq-pair-Σ refl ( eq-is-prop is-prop-type-trunc-Prop)))))
      retr-h' :
        (T :
          equivalence-class
            ( same-orbits-permutation-count
              ( composition-transposition-a-b g))) 
        is-decidable
          ( is-in-equivalence-class
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( T)
            ( a)) 
        is-decidable
          ( is-in-equivalence-class
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( T)
            ( b)) 
        Id (h' (inv-h' T)) T
      retr-h' T (inl Q) R =
        tr
           w 
            Id
              ( h'
                ( cases-inv-h' T w
                  ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                    ( number-of-elements-count eX)
                    ( pair X (unit-trunc-Prop (equiv-count eX)))
                    ( composition-transposition-a-b g)
                    ( T)
                    ( b))))
            ( T))
          { x = inl Q}
          { y =
            is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( composition-transposition-a-b g)
              ( T)
              ( a)}
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-prop-is-in-equivalence-class
                ( same-orbits-permutation-count
                  ( composition-transposition-a-b g))
                ( T)
                ( a))))
          ( ap
            ( λ w 
              h'-inl
                ( map-inv-equiv-count h
                  ( class (same-orbits-permutation-count g) a))
                ( map-equiv
                  ( pr1 w)
                  ( class (same-orbits-permutation-count g) a))
                (pr2 w)
                ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                    ( number-of-elements-count eX)
                    ( pair X (unit-trunc-Prop (equiv-count eX)))
                    ( g)
                    ( map-equiv
                      ( pr1 w)
                      ( class (same-orbits-permutation-count g) a))
                    ( a))
                ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                    ( number-of-elements-count eX)
                    ( pair X (unit-trunc-Prop (equiv-count eX))) g
                    ( map-equiv
                      ( pr1 w)
                      ( class (same-orbits-permutation-count g) a))
                    ( b)))
            { x = pair ((equiv-count h) ∘e (inv-equiv-count h)) refl}
            { y =
              pair
                ( id-equiv)
                ( ap
                  ( λ f 
                    map-equiv f (class (same-orbits-permutation-count g) a))
                  ( right-inverse-law-equiv (equiv-count h)))}
            ( eq-pair-Σ
              ( right-inverse-law-equiv (equiv-count h))
              ( eq-is-prop
                ( is-prop-type-Prop
                  ( Id-Prop
                    ( equivalence-class-Set (same-orbits-permutation-count g))
                    ( map-equiv-count h
                      ( map-inv-equiv-count h
                        ( class (same-orbits-permutation-count g) a)))
                    ( class (same-orbits-permutation-count g) a))))) 
            ( ap
              ( λ w 
                h'-inl
                  ( map-inv-equiv-count
                    ( h)
                    ( class (same-orbits-permutation-count g) a))
                  ( class (same-orbits-permutation-count g) a)
                  ( ap
                    ( λ f 
                      map-equiv f (class (same-orbits-permutation-count g) a))
                    ( right-inverse-law-equiv (equiv-count h)))
                  ( w)
                  ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                      ( number-of-elements-count eX)
                      ( pair X (unit-trunc-Prop (equiv-count eX)))
                      ( g)
                      (class (same-orbits-permutation-count g) a)
                      ( b)))
              { x =
                is-decidable-is-in-equivalence-class-same-orbits-permutation
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( g)
                ( map-equiv id-equiv
                  ( class (same-orbits-permutation-count g) a))
                ( a)}
              { y =
                inl
                  ( is-in-equivalence-class-eq-equivalence-class
                    ( same-orbits-permutation-count g)
                    ( a)
                    ( class (same-orbits-permutation-count g) a)
                    ( refl))}
              ( eq-is-prop
                ( is-prop-is-decidable
                  ( is-prop-is-in-equivalence-class
                    ( same-orbits-permutation-count g)
                    ( class (same-orbits-permutation-count g) a) a))) 
              ( eq-effective-quotient'
                ( same-orbits-permutation-count
                  ( composition-transposition-a-b g))
                ( a)
                ( T)
                ( Q))))
      retr-h' T (inr NQ) (inl R) =
        tr
           w  Id (h' (cases-inv-h' T (pr1 w) (pr2 w))) T)
          {x = pair (inr NQ) (inl R)}
          {y = pair
            (is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( composition-transposition-a-b g)
              ( T)
              ( a))
            ( is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( composition-transposition-a-b g)
              ( T)
              ( b))}
          ( eq-is-prop
            ( is-prop-Σ
              ( is-prop-is-decidable
                ( is-prop-is-in-equivalence-class
                  ( same-orbits-permutation-count
                    ( composition-transposition-a-b g))
                  ( T)
                  ( a)))
              ( λ _ 
                is-prop-is-decidable
                  ( is-prop-is-in-equivalence-class
                    ( same-orbits-permutation-count
                      ( composition-transposition-a-b g))
                    ( T)
                    ( b)))))
          ( eq-effective-quotient'
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( b)
            ( T)
            ( R))
      retr-h' T (inr NQ) (inr NR) =
        tr
           w  Id (h' (cases-inv-h' T (pr1 w) (pr2 w))) T)
          {x = pair (inr NQ) (inr NR)}
          {y = pair
            (is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( composition-transposition-a-b g)
              ( T)
              ( a))
            (is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( composition-transposition-a-b g)
              ( T)
              ( b))}
          ( eq-is-prop
            ( is-prop-Σ
              ( is-prop-is-decidable
                ( is-prop-is-in-equivalence-class
                  ( same-orbits-permutation-count
                    ( composition-transposition-a-b g))
                  ( T)
                  ( a)))
              ( λ _ 
                is-prop-is-decidable
                ( is-prop-is-in-equivalence-class
                  ( same-orbits-permutation-count
                    ( composition-transposition-a-b g))
                  ( T)
                  ( b)))))
          ( retr-h'-inr-inr T NQ NR
            ( is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( g)
              ( pair (pr1 T) (H-conserves T NQ NR))
              ( a))
            ( is-decidable-is-in-equivalence-class-same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( g)
              ( pair (pr1 T) (H-conserves T NQ NR)) b))
      sec-h'-inl :
        ( k : Fin (number-of-elements-count h))
        ( Q :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation-count g)
              ( map-equiv-count h k)
              ( a)))
        ( R :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation-count g)
              ( map-equiv-count h k)
              ( b)))
        ( Q' :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( h'-inl k (map-equiv-count h k) refl Q R)
              ( a)))
        ( R' :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( h'-inl k (map-equiv-count h k) refl Q R)
              ( b))) 
        Id
          ( cases-inv-h' (h'-inl k (map-equiv-count h k) refl Q R) Q' R')
          ( inl k)
      sec-h'-inl k (inl Q) R (inl Q') R' =
        ap inl
          ( is-injective-map-equiv (equiv-count h)
            ( ap
              ( λ f  map-equiv f (class (same-orbits-permutation-count g) a))
              ( right-inverse-law-equiv (equiv-count h)) 
              ( eq-effective-quotient'
                ( same-orbits-permutation-count g)
                ( a)
                ( map-equiv-count h k)
                ( Q))))
      sec-h'-inl k (inl Q) R (inr NQ') R' =
        ex-falso
          ( NQ'
            ( is-in-equivalence-class-eq-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( a)
              ( class
                ( same-orbits-permutation-count
                  ( composition-transposition-a-b g))
                ( a))
              ( refl)))
      sec-h'-inl k (inr NQ) (inl R) Q' R' =
        ex-falso
        ( NQ
          ( transitive-is-in-equivalence-class
            ( same-orbits-permutation-count g)
            ( map-equiv-count h k)
            ( b)
            ( a)
            ( R)
            ( symm-Eq-Rel (same-orbits-permutation-count g) P)))
      sec-h'-inl k (inr NQ) (inr NR) (inl Q') R' = ex-falso (NQ Q')
      sec-h'-inl k (inr NQ) (inr NR) (inr NQ') (inl R') = ex-falso (NR R')
      sec-h'-inl k (inr NQ) (inr NR) (inr NQ') (inr NR') =
        ap
          ( inl)
          ( ap
            ( map-inv-equiv-count h)
            ( eq-pair-Σ
              ( refl)
              ( eq-is-prop is-prop-type-trunc-Prop)) 
            ap  f  map-equiv f k) (left-inverse-law-equiv (equiv-count h)))
      sec-h'-inr :
        ( Q :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( class
                ( same-orbits-permutation-count
                  ( composition-transposition-a-b g))
                ( b))
              ( a))) 
        ( R :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( class
                ( same-orbits-permutation-count
                  ( composition-transposition-a-b g))
                ( b))
              ( b))) 
        Id
          ( cases-inv-h'
            ( class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( b))
            ( Q)
            ( R))
          ( inr star)
      sec-h'-inr (inl Q) R =
        ex-falso (not-same-orbits-transposition-same-orbits g P
          ( symm-Eq-Rel
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( Q)))
      sec-h'-inr (inr Q) (inl R) = refl
      sec-h'-inr (inr Q) (inr NR) =
        ex-falso
          ( NR
            ( is-in-equivalence-class-eq-equivalence-class
              ( same-orbits-permutation-count (composition-transposition-a-b g))
              ( b)
              ( class
                ( same-orbits-permutation-count
                  ( composition-transposition-a-b g))
                ( b))
              ( refl)))
      sec-h' :
        (k : Fin (succ-ℕ (number-of-elements-count h)))  Id (inv-h' (h' k)) k
      sec-h' (inl k) =
        sec-h'-inl k Q R
          ( is-decidable-is-in-equivalence-class-same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)
            ( h'-inl k (map-equiv-count h k) refl Q R)
            ( a))
          ( is-decidable-is-in-equivalence-class-same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)
            ( h'-inl k (map-equiv-count h k) refl Q R)
            ( b))
        where
        Q :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation
                ( number-of-elements-count eX)
                (pair X (unit-trunc-Prop (equiv-count eX)))
                ( g))
              ( map-equiv-count h k)
              ( a))
        Q =
          is-decidable-is-in-equivalence-class-same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g)
            ( map-equiv-count h k)
            ( a)
        R :
          is-decidable
            ( is-in-equivalence-class
              ( same-orbits-permutation
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( g))
              ( map-equiv-count h k)
              ( b))
        R =
          is-decidable-is-in-equivalence-class-same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g)
            ( map-equiv-count h k)
            ( b)
      sec-h' (inr star) =
        sec-h'-inr
        ( is-decidable-is-in-equivalence-class-same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( composition-transposition-a-b g)
          ( class
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( b))
          ( a))
        ( is-decidable-is-in-equivalence-class-same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( composition-transposition-a-b g)
          ( class
            ( same-orbits-permutation-count (composition-transposition-a-b g))
            ( b))
          ( b))

  transf-same-orbits-count :
    ( g : X  X)
    ( P :
      sim-Eq-Rel
        ( same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g))
        ( a)
        ( b)) 
    count
      ( equivalence-class
        ( same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g))) 
      count
        ( equivalence-class
          ( same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)))
  transf-same-orbits-count g P h =
    pair
      ( succ-ℕ (number-of-elements-count h))
      ( pair
        ( h' g P h)
        ( is-equiv-has-inverse
          ( inv-h' g P h)
          ( λ T 
            retr-h'
              ( g)
              ( P)
              ( h)
              ( T)
              ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( composition-transposition-a-b g)
                ( T)
                ( a))
              ( is-decidable-is-in-equivalence-class-same-orbits-permutation
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( composition-transposition-a-b g)
                ( T)
                ( b)))
          ( sec-h' g P h)))

  abstract
    number-orbits-composition-transposition :
      ( g : X  X)
      ( P :
        sim-Eq-Rel
          ( same-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g))
          ( a)
          ( b)) 
      Id
        ( succ-ℕ
          ( number-of-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g)))
        ( number-of-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( composition-transposition-a-b g))
    number-orbits-composition-transposition g P =
      apply-universal-property-trunc-Prop
        ( has-finite-number-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g))
        ( Id-Prop
          ( ℕ-Set)
          ( succ-ℕ
            ( number-of-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( g)))
          ( number-of-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)))
        ( λ h 
          ( ap
            ( succ-ℕ  number-of-elements-is-finite)
            ( eq-is-prop is-prop-type-trunc-Prop) 
            ( ap
              ( succ-ℕ  pr1)
              ( all-elements-equal-has-finite-cardinality
                ( has-finite-cardinality-is-finite (unit-trunc-Prop h))
                ( has-finite-cardinality-count h)) 
              ( ap
                ( pr1)
                ( all-elements-equal-has-finite-cardinality
                  ( has-finite-cardinality-count
                    ( transf-same-orbits-count g P h))
                  ( has-finite-cardinality-is-finite
                    ( unit-trunc-Prop (transf-same-orbits-count g P h)))) 
                ap
                  ( number-of-elements-is-finite)
                  ( eq-is-prop is-prop-type-trunc-Prop)))))

  abstract
    same-orbits-transposition-not-same-orbits :
      ( g : X  X)
      ( NP : ¬ (sim-Eq-Rel (same-orbits-permutation-count g) a b)) 
      sim-Eq-Rel
        ( same-orbits-permutation-count (composition-transposition-a-b g))
        ( a)
        ( b)
    same-orbits-transposition-not-same-orbits g NP =
      unit-trunc-Prop (pair (pr1 minimal-element-iterate-repeating) lemma)
      where
      minimal-element-iterate-repeating :
        minimal-element-ℕ
          ( λ k  is-nonzero-ℕ k × Id (iterate k (map-equiv g) a) a)
      minimal-element-iterate-repeating =
        minimal-element-iterate-nonzero
          ( g)
          ( a)
          ( a)
          ( has-finite-orbits-permutation X eX g a)
      neq-iterate-nonzero-le-minimal-element :
        (k : ) 
        is-nonzero-ℕ k × le-ℕ k (pr1 minimal-element-iterate-repeating) 
        ¬ (Id (iterate k (map-equiv g) a) a) ×
        ¬ (Id (iterate k (map-equiv g) a) b)
      pr1 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) Q =
        contradiction-le-ℕ k (pr1 minimal-element-iterate-repeating) ineq
          (pr2 (pr2 minimal-element-iterate-repeating) k (pair nz Q))
      pr2 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) R =
        NP (unit-trunc-Prop (pair k R))
      equal-iterate-transposition-a :
        (k : )  le-ℕ k (pr1 minimal-element-iterate-repeating) 
        Id
          ( iterate k (map-equiv (composition-transposition-a-b g)) a)
          ( iterate k (map-equiv g) a)
      equal-iterate-transposition-a k ineq =
        equal-iterate-transposition a g
          ( λ k' 
            ( is-nonzero-ℕ k') ×
            ( le-ℕ k' (pr1 minimal-element-iterate-repeating)))
          ( neq-iterate-nonzero-le-minimal-element)
          ( λ n (pair _ s) nz 
            pair
              ( nz)
              ( transitive-le-ℕ n
                ( succ-ℕ n)
                ( pr1 minimal-element-iterate-repeating)
                ( succ-le-ℕ n)
                ( s)))
          ( k)
          ( cases-equal-iterate-transposition-a
            ( has-decidable-equality-ℕ k zero-ℕ))
        where
        cases-equal-iterate-transposition-a :
          is-decidable (is-zero-ℕ k) 
          ( is-zero-ℕ k) +
          ( is-nonzero-ℕ k × le-ℕ k (pr1 minimal-element-iterate-repeating))
        cases-equal-iterate-transposition-a (inl s) = inl s
        cases-equal-iterate-transposition-a (inr s) = inr (pair s ineq)
      lemma :
        Id
          ( iterate
            ( pr1 minimal-element-iterate-repeating)
            ( map-equiv (composition-transposition-a-b g))
            ( a))
          ( b)
      lemma =
        ( ap
          ( λ n  iterate n (map-equiv (composition-transposition-a-b g)) a)
          ( pr2 (is-successor-k1) 
            commutative-add-ℕ (pr1 is-successor-k1) (succ-ℕ zero-ℕ))) 
        ( iterate-add-ℕ
          ( succ-ℕ zero-ℕ)
          ( pr1 is-successor-k1)
          ( map-equiv (composition-transposition-a-b g))
          ( a) 
          ( ap
            ( map-equiv (composition-transposition-a-b g))
            ( equal-iterate-transposition-a
              ( pr1 is-successor-k1)
              ( tr
                ( le-ℕ (pr1 is-successor-k1))
                ( inv (pr2 is-successor-k1))
                ( succ-le-ℕ (pr1 is-successor-k1)))) 
            ( ap
              ( λ n 
                map-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np)
                  ( iterate n (map-equiv g) a))
              ( inv (pr2 is-successor-k1)) 
              ( ap
                ( map-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np))
                ( pr2 (pr1 (pr2 minimal-element-iterate-repeating))) 
                ( left-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np))))))
        where
        is-successor-k1 : is-successor-ℕ (pr1 minimal-element-iterate-repeating)
        is-successor-k1 =
          is-successor-is-nonzero-ℕ
            ( pr1 (pr1 (pr2 minimal-element-iterate-repeating)))

  abstract
    number-orbits-composition-transposition' :
      ( g : X  X)
      (NP :
        ¬ ( sim-Eq-Rel
            ( same-orbits-permutation
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( g))
            ( a)
            ( b))) 
      Id
        ( number-of-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g))
        ( succ-ℕ
          ( number-of-orbits-permutation
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)))
    number-orbits-composition-transposition' g NP =
      ( ap
        ( number-of-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX))))
        ( inv (eq-htpy-equiv (composition-transposition-a-b-involution g)))) 
        ( inv
          ( number-orbits-composition-transposition
            ( composition-transposition-a-b g)
            ( same-orbits-transposition-not-same-orbits g NP)))

  abstract
    opposite-sign-composition-transposition-count :
      (g : X  X) 
      Id
        ( sign-permutation-orbit
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g))
        ( succ-Fin
          ( 2)
          ( sign-permutation-orbit
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( composition-transposition-a-b g)))
    opposite-sign-composition-transposition-count g =
      cases-opposite-sign-composition-transposition
        ( is-decidable-same-orbits-permutation
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( g)
          ( a)
          ( b))
      where
      cases-opposite-sign-composition-transposition :
        is-decidable (sim-Eq-Rel (same-orbits-permutation-count g) a b) 
        Id
          ( sign-permutation-orbit
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( g))
          ( succ-Fin
            ( 2)
            ( sign-permutation-orbit
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( composition-transposition-a-b g)))
      cases-opposite-sign-composition-transposition (inl P) =
        inv
          ( is-involution-aut-Fin-two-ℕ
            ( equiv-succ-Fin 2)
            ( sign-permutation-orbit
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( g))) 
        ap
          ( λ k 
            succ-Fin
              ( 2)
              ( iterate
                ( (number-of-elements-count eX) +ℕ k)
                ( succ-Fin 2)
                ( zero-Fin 1)))
          ( number-orbits-composition-transposition g P)
      cases-opposite-sign-composition-transposition (inr NP) =
        ap
          ( λ k 
            iterate
              ( (number-of-elements-count eX) +ℕ k)
              ( succ-Fin 2)
              ( zero-Fin 1))
          ( number-orbits-composition-transposition' g NP)

module _
  {l : Level} (X : UU l) (eX : count X)
  where

  abstract
    sign-list-transpositions-count :
      ( li :
        list
          ( Σ ( X  Decidable-Prop l)
              ( λ P 
                has-cardinality 2 (Σ X (type-Decidable-Prop  P))))) 
      Id
        ( iterate
          ( length-list li)
          ( succ-Fin 2)
          ( sign-permutation-orbit
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( id-equiv)))
        ( sign-permutation-orbit
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( permutation-list-transpositions li))
    sign-list-transpositions-count nil = refl
    sign-list-transpositions-count (cons t li) =
      ap (succ-Fin 2)
        ( sign-list-transpositions-count li 
          opposite-sign-composition-transposition-count
            ( X)
            ( eX)
            ( pr1 two-elements-t)
            ( pr1 (pr2 two-elements-t))
            ( pr1 (pr2 (pr2 two-elements-t)))
            ( permutation-list-transpositions li)) 
        ( is-involution-aut-Fin-two-ℕ
          ( equiv-succ-Fin 2)
          ( sign-permutation-orbit
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( permutation-list-transpositions
              ( cons
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( pr1 (pr2 (pr2 two-elements-t))))
                ( li)))) 
          ( ap
            ( λ g 
              sign-permutation-orbit
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( permutation-list-transpositions (cons g li)))
            { x =
              standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( pr1 (pr2 (pr2 two-elements-t)))}
            { y = t}
            ( pr2 (pr2 (pr2 two-elements-t)))))
      where
      two-elements-t :
        Σ ( X)
          ( λ x 
            Σ ( X)
              ( λ y 
                Σ ( ¬ (Id x y))
                  ( λ np 
                    Id
                      ( standard-2-Element-Decidable-Subtype
                        ( has-decidable-equality-count eX)
                        ( np))
                      ( t))))
      two-elements-t = two-elements-transposition eX t