Orientations of the complete undirected graph

{-# OPTIONS --lossy-unification #-}
module univalent-combinatorics.orientations-complete-undirected-graph where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.congruence-natural-numbers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import finite-group-theory.transpositions

open import foundation.cartesian-product-types
open import foundation.coproduct-types
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.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.function-extensionality
open import foundation.functions
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.intersections-subtypes
open import foundation.involutions
open import foundation.logical-equivalences
open import foundation.mere-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels

open import univalent-combinatorics.2-element-decidable-subtypes
open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.decidable-subtypes
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types
open import univalent-combinatorics.symmetric-difference
module _
  {l : Level} (n : ) (X : UU-Fin l n)
  where

  orientation-Complete-Undirected-Graph : UU (lsuc l)
  orientation-Complete-Undirected-Graph =
    ((pair P H) : 2-Element-Decidable-Subtype l (type-UU-Fin n X)) 
    Σ (type-UU-Fin n X) (type-Decidable-Prop  P)

  is-set-orientation-Complete-Undirected-Graph :
    is-set orientation-Complete-Undirected-Graph
  is-set-orientation-Complete-Undirected-Graph =
    is-set-Π
      ( λ (P , H) 
        is-set-Σ
          ( is-set-type-UU-Fin n X)
          ( λ x  is-set-is-prop (is-prop-type-Decidable-Prop (P x))))

  2-Element-Decidable-Subtype-subtype-pointwise-difference :
    orientation-Complete-Undirected-Graph 
    orientation-Complete-Undirected-Graph 
    2-Element-Decidable-Subtype l (type-UU-Fin n X)  Decidable-Prop l
  pr1 (2-Element-Decidable-Subtype-subtype-pointwise-difference d d' Y) =
    ¬ (Id (d Y) (d' Y))
  pr1 (pr2 (2-Element-Decidable-Subtype-subtype-pointwise-difference d d' Y)) =
    is-prop-neg
  pr2 (pr2 (2-Element-Decidable-Subtype-subtype-pointwise-difference d d' Y)) =
    is-decidable-neg
      ( has-decidable-equality-is-finite
        ( is-finite-type-decidable-subtype
          ( pr1 Y)
          ( is-finite-type-UU-Fin n X))
        ( d Y)
        ( d' Y))
  is-finite-subtype-pointwise-difference :
    (d d' : orientation-Complete-Undirected-Graph) 
    is-finite
      ( Σ
        ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
        ( λ Y 
          type-Decidable-Prop
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d d' Y)))
  is-finite-subtype-pointwise-difference d d' =
    is-finite-type-decidable-subtype
      ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d d')
      ( is-finite-2-Element-Decidable-Subtype n X)
  mod-two-number-of-differences-orientation-Complete-Undirected-Graph :
    orientation-Complete-Undirected-Graph 
    orientation-Complete-Undirected-Graph  Fin 2
  mod-two-number-of-differences-orientation-Complete-Undirected-Graph d d' =
    mod-two-ℕ (number-of-elements-is-finite
      ( is-finite-subtype-pointwise-difference d d'))
  abstract
    equiv-symmetric-difference-subtype-pointwise-difference :
      ( d1 d2 d3 : orientation-Complete-Undirected-Graph) 
      ( type-decidable-subtype
        ( symmetric-difference-decidable-subtype
          ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d2)
          ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d2 d3)) 
        type-decidable-subtype
          ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d3))
    equiv-symmetric-difference-subtype-pointwise-difference d1 d2 d3 =
      equiv-Σ
        ( λ x 
          pr1
            (subtype-decidable-subtype
              (2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d3)
              ( x)))
        ( id-equiv)
        ( λ Y 
          equiv-iff
            ( prop-Decidable-Prop
              ( symmetric-difference-decidable-subtype
                ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                  d1 d2)
                ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                  d2 d3)
                ( Y)))
            ( prop-Decidable-Prop
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                d1 d3 Y))
            ( f Y)
            ( g Y))
      where
      f :
        (Y : 2-Element-Decidable-Subtype l (type-UU-Fin n X)) 
        type-Prop
          ( prop-Decidable-Prop
            ( symmetric-difference-decidable-subtype
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d2)
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d2 d3)
              ( Y))) 
          type-Prop
            ( prop-Decidable-Prop
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                d1 d3 Y))
      f Y (inl (pair np nnq)) r =
        np (r 
          inv
            ( double-negation-elim-is-decidable
              ( has-decidable-equality-is-finite
                ( is-finite-type-decidable-subtype
                  ( pr1 Y)
                  ( is-finite-type-UU-Fin n X))
                ( d2 Y)
                ( d3 Y))
              ( nnq)))
      f Y (inr (pair nq nnp)) r =
        nq
          ( ( inv
              ( double-negation-elim-is-decidable
                ( has-decidable-equality-is-finite
                  ( is-finite-type-decidable-subtype
                    ( pr1 Y)
                    ( is-finite-type-UU-Fin n X))
                  ( d1 Y)
                  ( d2 Y))
                ( nnp))) 
            ( r))
      cases-g :
        (Y : 2-Element-Decidable-Subtype l (type-UU-Fin n X)) 
        ¬ (Id (d1 Y) (d3 Y))  (is-decidable (Id (d1 Y) (d2 Y))) 
        is-decidable (Id (d2 Y) (d3 Y)) 
        (¬ (Id (d1 Y) (d2 Y)) × ¬ (¬ (Id (d2 Y) (d3 Y)))) +
        (¬ (Id (d2 Y) (d3 Y)) × ¬ (¬ (Id (d1 Y) (d2 Y))))
      cases-g Y nr (inl p) (inl q) = ex-falso (nr (p  q))
      cases-g Y nr (inl p) (inr nq) = inr (pair nq  f  f p))
      cases-g Y nr (inr np) (inl q) = inl (pair np  f  f q))
      cases-g Y nr (inr np) (inr nq) =
        ex-falso
          (apply-universal-property-trunc-Prop
            ( pr2 Y)
            ( empty-Prop)
            ( λ h 
              contradiction-3-distinct-element-2-Element-Type
                ( 2-element-type-2-Element-Decidable-Subtype Y)
                ( d1 Y)
                ( d2 Y)
                ( d3 Y)
                ( np)
                ( nq)
                ( nr)))
      g :
        (Y : 2-Element-Decidable-Subtype l (type-UU-Fin n X)) 
        type-Decidable-Prop
          ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d3 Y) 
        type-Decidable-Prop
          ( symmetric-difference-decidable-subtype
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d2)
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d2 d3) Y)
      g Y r =
        cases-g Y r
          ( has-decidable-equality-is-finite
            ( is-finite-type-decidable-subtype
              ( pr1 Y)
              ( is-finite-type-UU-Fin n X))
            ( d1 Y)
            ( d2 Y))
          ( has-decidable-equality-is-finite
            ( is-finite-type-decidable-subtype
              ( pr1 Y)
              ( is-finite-type-UU-Fin n X))
            ( d2 Y)
            ( d3 Y))
  is-symmetric-mod-two-number-of-differences-orientation-Complete-Undirected-Graph :
    ( d d' : orientation-Complete-Undirected-Graph) (m : Fin 2) 
    Id
      ( m)
      ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
        d d') 
    Id
      ( m)
      ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
        d' d)
  is-symmetric-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
    d d' m p =
    ( p) 
    ( ap
      ( mod-two-ℕ  number-of-elements-has-finite-cardinality)
      ( all-elements-equal-has-finite-cardinality
        ( has-finite-cardinality-d'-d)
        ( has-finite-cardinality-is-finite
          ( is-finite-subtype-pointwise-difference d' d))))
    where
    has-finite-cardinality-d'-d :
      has-finite-cardinality
        ( Σ ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
            ( λ Y 
              type-Decidable-Prop
                ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                  d' d Y)))
    pr1 has-finite-cardinality-d'-d =
      pr1
        ( has-finite-cardinality-is-finite
          ( is-finite-subtype-pointwise-difference d d'))
    pr2 has-finite-cardinality-d'-d =
      apply-universal-property-trunc-Prop
        ( pr2
          ( has-finite-cardinality-is-finite
            ( is-finite-subtype-pointwise-difference d d')))
        ( trunc-Prop
          ( ( Fin (pr1 has-finite-cardinality-d'-d)) 
            ( Σ ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
                ( λ Y  ¬ (Id (d' Y) (d Y))))))
        ( λ h  unit-trunc-Prop (h' ∘e h))
      where
      h' :
        Σ ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
          ( λ Y  ¬ (Id (d Y) (d' Y))) 
        Σ ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
          ( λ Y  ¬ (Id (d' Y) (d Y)))
      pr1 h' (pair Y np) = pair Y  p'  np (inv p'))
      pr2 h' =
        is-equiv-has-inverse
          ( λ (pair Y np)  pair Y  p'  np (inv p')))
          ( λ (pair Y np)  eq-pair-Σ refl (eq-is-prop is-prop-neg))
          ( λ (pair Y np)  eq-pair-Σ refl (eq-is-prop is-prop-neg))
  eq-mod-two-number-of-differences-orientation-Complete-Undirected-Graph :
    (d1 d2 d3 : orientation-Complete-Undirected-Graph) (m : Fin 2) 
    Id
      ( m)
      ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
        d1 d2) 
    Id
      ( m)
      ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
        d2 d3) 
    Id
      ( zero-Fin 1)
      ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
        d1 d3)
  eq-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
    d1 d2 d3 m p1 p2 =
    inv
      ( is-zero-mod-succ-ℕ
        ( 1)
        ( dist-ℕ (k1 +ℕ k2) (2 *ℕ k'))
        ( trans-cong-ℕ
          ( 2)
          ( k1 +ℕ k2)
          ( zero-ℕ)
          ( 2 *ℕ k')
          ( trans-cong-ℕ 2
            ( k1 +ℕ k2)
            ( add-ℕ
              ( nat-Fin 2
                ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                    d1 d2))
              ( nat-Fin 2
                ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                    d2 d3)))
            ( zero-ℕ)
            ( symm-cong-ℕ 2
              ( add-ℕ
                ( nat-Fin 2
                  ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                      d1 d2))
                ( nat-Fin 2
                  ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                      d2 d3)))
              ( k1 +ℕ k2)
              ( cong-add-ℕ k1 k2))
            ( concatenate-eq-cong-ℕ 2
              ( ( ap-binary
                ( add-ℕ)
                ( ap (nat-Fin 2) (inv p1))
                ( ap (nat-Fin 2) (inv p2))) 
                ( ap
                  ( λ n  n +ℕ (nat-Fin 2 m))
                  ( inv (left-unit-law-mul-ℕ (nat-Fin 2 m)))))
              ( scalar-invariant-cong-ℕ' 2 2 0 (nat-Fin 2 m) (cong-zero-ℕ' 2))))
          ( scalar-invariant-cong-ℕ' 2 0 2 k' (cong-zero-ℕ' 2)))) 
      ( ap
        ( mod-two-ℕ)
        ( ( symmetric-dist-ℕ (k1 +ℕ k2) (2 *ℕ k')) 
          ( inv
            ( rewrite-left-add-dist-ℕ
              ( k)
              ( 2 *ℕ k')
              ( k1 +ℕ k2)
              ( inv
                ( eq-symmetric-difference
                  ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
                  ( is-finite-2-Element-Decidable-Subtype n X)
                  ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                      d1 d2)
                  ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                      d2 d3)))) 
            ( ap
              ( number-of-elements-has-finite-cardinality)
              ( all-elements-equal-has-finite-cardinality
                ( has-finite-cardinality-is-finite
                  ( is-finite-type-decidable-subtype
                    ( symmetric-difference-decidable-subtype
                      ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                          d1 d2)
                      ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                          d2 d3))
                    ( is-finite-2-Element-Decidable-Subtype n X)))
               ( pair
                 ( number-of-elements-is-finite
                   ( is-finite-type-decidable-subtype
                     ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                        d1 d3)
                     ( is-finite-2-Element-Decidable-Subtype n X)))
                 ( transitive-mere-equiv
                   ( pr2
                    ( has-finite-cardinality-is-finite
                      ( is-finite-type-decidable-subtype
                        ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                            d1 d3)
                        ( is-finite-2-Element-Decidable-Subtype n X))))
                   ( unit-trunc-Prop
                     ( inv-equiv
                       ( equiv-symmetric-difference-subtype-pointwise-difference
                          d1 d2 d3))))))))))
    where
    k : 
    k =
      number-of-elements-is-finite
        ( is-finite-type-decidable-subtype
          ( symmetric-difference-decidable-subtype
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                d1 d2)
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                d2 d3))
          ( is-finite-2-Element-Decidable-Subtype n X))
    k1 : 
    k1 =
      number-of-elements-is-finite
        (is-finite-subtype-pointwise-difference d1 d2)
    k2 : 
    k2 =
      number-of-elements-is-finite
        (is-finite-subtype-pointwise-difference d2 d3)
    k' : 
    k' =
      number-of-elements-is-finite
        ( is-finite-type-decidable-subtype
          ( intersection-decidable-subtype
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d1 d2)
            ( 2-Element-Decidable-Subtype-subtype-pointwise-difference d2 d3))
          ( is-finite-2-Element-Decidable-Subtype n X))
  even-difference-orientation-Complete-Undirected-Graph :
    Eq-Rel lzero orientation-Complete-Undirected-Graph
  pr1 even-difference-orientation-Complete-Undirected-Graph d d' =
    Id-Prop
      ( Fin-Set 2)
      ( zero-Fin 1)
      ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
          d d')
  pr1 (pr2 even-difference-orientation-Complete-Undirected-Graph) {d} =
    ap
      ( mod-two-ℕ  number-of-elements-has-finite-cardinality)
      ( all-elements-equal-has-finite-cardinality
        ( pair
          ( 0)
          ( unit-trunc-Prop (equiv-is-empty id  (pair _ np)  np refl))))
        ( has-finite-cardinality-is-finite
          ( is-finite-subtype-pointwise-difference d d)))
  pr1 (pr2 (pr2 even-difference-orientation-Complete-Undirected-Graph))
    {d} {d'} p =
    is-symmetric-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
      d d' (zero-Fin 1) p
  pr2 (pr2 (pr2 even-difference-orientation-Complete-Undirected-Graph))
    {d1} {d2} {d3} p1 p2 =
    eq-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
      d1 d2 d3 (zero-Fin 1) p1 p2
  abstract
    is-decidable-even-difference-orientation-Complete-Undirected-Graph :
      (Y Y' : orientation-Complete-Undirected-Graph) 
      is-decidable
        (sim-Eq-Rel even-difference-orientation-Complete-Undirected-Graph Y Y')
    is-decidable-even-difference-orientation-Complete-Undirected-Graph Y Y' =
      has-decidable-equality-is-finite
        ( is-finite-Fin 2)
        ( zero-Fin 1)
        ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
            Y Y')
  quotient-sign : UU (lsuc l)
  quotient-sign =
    equivalence-class even-difference-orientation-Complete-Undirected-Graph
  quotient-sign-Set : Set (lsuc l)
  quotient-sign-Set =
    equivalence-class-Set even-difference-orientation-Complete-Undirected-Graph
module _
  {l : Level} (n : )
  where
  map-orientation-complete-undirected-graph-equiv :
    (X X' : UU-Fin l n) 
    (type-UU-Fin n X  type-UU-Fin n X') 
    orientation-Complete-Undirected-Graph n X 
    orientation-Complete-Undirected-Graph n X'
  pr1 (map-orientation-complete-undirected-graph-equiv X X' e d Y) =
    map-equiv e (pr1 (d (precomp-equiv-2-Element-Decidable-Subtype e Y)))
  pr2 (map-orientation-complete-undirected-graph-equiv X X' e d Y) =
    pr2 (d (precomp-equiv-2-Element-Decidable-Subtype e Y))
  orientation-complete-undirected-graph-equiv :
    (X X' : UU-Fin l n) 
    (type-UU-Fin n X  type-UU-Fin n X') 
    orientation-Complete-Undirected-Graph n X 
    orientation-Complete-Undirected-Graph n X'
  pr1 (orientation-complete-undirected-graph-equiv X X' e) =
    map-orientation-complete-undirected-graph-equiv X X' e
  pr2 (orientation-complete-undirected-graph-equiv X X' e) =
    is-equiv-has-inverse
      ( map-orientation-complete-undirected-graph-equiv X' X (inv-equiv e))
      ( λ d 
        eq-htpy
          ( λ Y 
            eq-pair-Σ
              (( ( ap
                ( λ Y'  (map-equiv e  (map-equiv (inv-equiv e))) (pr1 (d Y')))
                ( eq-pair-Σ
                  ( ap
                    ( λ h  pr1 Y  map-equiv h)
                    ( left-inverse-law-equiv (inv-equiv e)))
                  ( eq-is-prop is-prop-type-trunc-Prop))) 
                ( ap
                  ( λ h  map-equiv h (pr1 (d Y)))
                  ( left-inverse-law-equiv (inv-equiv e)))))
              ( eq-is-prop
                ( is-prop-type-Decidable-Prop (pr1 Y (pr1 (id d Y)))))))
      ( λ d 
        eq-htpy
          ( λ Y 
            eq-pair-Σ
              ( ( ap
                ( λ Y'  (map-equiv (inv-equiv e)  map-equiv e) (pr1 (d Y')))
                ( eq-pair-Σ
                  ( ap
                    ( λ h  pr1 Y  map-equiv h)
                    ( right-inverse-law-equiv (inv-equiv e)))
                  ( eq-is-prop is-prop-type-trunc-Prop))) 
                ( ap
                  ( λ h  map-equiv h (pr1 (d Y)))
                  ( right-inverse-law-equiv (inv-equiv e))))
              ( eq-is-prop
                ( is-prop-type-Decidable-Prop (pr1 Y (pr1 (id d Y)))))))
  abstract
    preserves-id-equiv-orientation-complete-undirected-graph-equiv :
      (X : UU-Fin l n) 
      Id (orientation-complete-undirected-graph-equiv X X id-equiv) id-equiv
    preserves-id-equiv-orientation-complete-undirected-graph-equiv X =
      eq-htpy-equiv
        ( λ d 
          eq-htpy
            ( λ Y 
              eq-pair-Σ
                ( ap
                  ( pr1  d)
                  ( eq-pair-Σ refl (eq-is-prop is-prop-type-trunc-Prop)))
                ( eq-is-prop
                  ( is-prop-type-Decidable-Prop
                    ( pr1 Y (pr1 (map-equiv id-equiv d Y)))))))
    preserves-comp-orientation-complete-undirected-graph-equiv :
      ( X Y Z : UU-Fin l n)
      (e : type-UU-Fin n X  type-UU-Fin n Y) 
      (f : type-UU-Fin n Y  type-UU-Fin n Z) 
      Id
        ( orientation-complete-undirected-graph-equiv X Z (f ∘e e))
        ( ( orientation-complete-undirected-graph-equiv Y Z f) ∘e
          ( orientation-complete-undirected-graph-equiv X Y e))
    preserves-comp-orientation-complete-undirected-graph-equiv X Y Z e f =
      eq-htpy-equiv
        ( λ d 
          eq-htpy
            ( λ S 
              eq-pair-Σ
                ( ap
                  ( λ S'  map-equiv (f ∘e e) (pr1 (d S')))
                  ( htpy-eq
                    ( preserves-comp-precomp-equiv-2-Element-Decidable-Subtype
                        e f)
                    ( S)))
                ( eq-is-prop
                  ( is-prop-type-Decidable-Prop
                    ( pr1 S
                      ( pr1
                        ( map-equiv
                          ( orientation-complete-undirected-graph-equiv Y Z f ∘e
                            orientation-complete-undirected-graph-equiv X Y e)
                          ( d)
                          ( S))))))))
    preserves-even-difference-orientation-complete-undirected-graph-equiv :
      (X X' : UU-Fin l n) ( e : type-UU-Fin n X  type-UU-Fin n X') 
      ( d d' : orientation-Complete-Undirected-Graph n X) 
      ( sim-Eq-Rel
        ( even-difference-orientation-Complete-Undirected-Graph n X)
        ( d)
        ( d') 
        sim-Eq-Rel
          ( even-difference-orientation-Complete-Undirected-Graph n X')
          ( map-orientation-complete-undirected-graph-equiv X X' e d)
          ( map-orientation-complete-undirected-graph-equiv X X' e d'))
    pr1
      ( preserves-even-difference-orientation-complete-undirected-graph-equiv
          X X' e d d') =
      _∙ ap
          ( mod-two-ℕ  number-of-elements-has-finite-cardinality)
          ( all-elements-equal-has-finite-cardinality
            ( has-finite-cardinality-is-finite
              ( is-finite-subtype-pointwise-difference n X d d'))
            ( pair
              ( number-of-elements-is-finite
                ( is-finite-subtype-pointwise-difference n X'
                  ( map-orientation-complete-undirected-graph-equiv X X' e d)
                  ( map-orientation-complete-undirected-graph-equiv X X' e d')))
              ( map-trunc-Prop
                ( equiv-subtype-pointwise-difference-equiv ∘e_)
                ( pr2
                  ( has-finite-cardinality-is-finite
                    ( is-finite-subtype-pointwise-difference n X'
                      ( map-orientation-complete-undirected-graph-equiv
                          X X' e d)
                      ( map-orientation-complete-undirected-graph-equiv
                          X X' e d')))))))
      where
      equiv-subtype-pointwise-difference-equiv :
        Σ (2-Element-Decidable-Subtype l (type-UU-Fin n X'))
          ( λ Y 
            type-Decidable-Prop
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference n X'
                ( map-orientation-complete-undirected-graph-equiv X X' e d)
                ( map-orientation-complete-undirected-graph-equiv X X' e d')
                ( Y))) 
        Σ (2-Element-Decidable-Subtype l (type-UU-Fin n X))
          ( λ Y 
            type-Decidable-Prop
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                  n X d d' Y))
      pr1 (pr1 equiv-subtype-pointwise-difference-equiv (pair Y NQ)) =
        precomp-equiv-2-Element-Decidable-Subtype e Y
      pr2 (pr1 equiv-subtype-pointwise-difference-equiv (pair Y NQ)) p =
        NQ
          ( eq-pair-Σ
            ( ap (map-equiv e) (pr1 (pair-eq-Σ p)))
            ( eq-is-prop
              ( is-prop-type-Decidable-Prop
                ( pr1
                  ( Y)
                  ( pr1
                    ( map-orientation-complete-undirected-graph-equiv
                        X X' e d' Y))))))
      pr2 equiv-subtype-pointwise-difference-equiv =
        is-equiv-has-inverse
          ( λ (pair Y NQ) 
            pair
              ( precomp-equiv-2-Element-Decidable-Subtype (inv-equiv e) Y)
              ( λ p 
                NQ
                  ( eq-pair-Σ
                    ( ( ap
                      ( λ Y'  pr1 (d Y'))
                      ( eq-pair-Σ
                        ( ap
                          ( λ h  pr1 Y  (map-equiv h))
                          ( inv (left-inverse-law-equiv e)))
                        ( eq-is-prop is-prop-type-trunc-Prop))) 
                      ( ( is-injective-map-equiv e (pr1 (pair-eq-Σ p))) 
                        ( ap
                          ( λ Y'  pr1 (d' Y'))
                          ( eq-pair-Σ
                            ( ap
                              ( λ h  pr1 Y  map-equiv h)
                              ( left-inverse-law-equiv e))
                            ( eq-is-prop is-prop-type-trunc-Prop)))))
                    ( eq-is-prop
                      ( is-prop-type-Decidable-Prop (pr1 Y (pr1 (d' Y))))))))
          ( λ (pair Y NQ) 
            eq-pair-Σ
              ( eq-pair-Σ
                ( ap  h  pr1 Y  map-equiv h) (left-inverse-law-equiv e))
                ( eq-is-prop is-prop-type-trunc-Prop))
              ( eq-is-prop
                ( is-prop-type-Decidable-Prop
                  ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                      n X d d' Y))))
          ( λ (pair Y NQ) 
            eq-pair-Σ
              ( eq-pair-Σ
                ( ap  h  pr1 Y  map-equiv h) (right-inverse-law-equiv e))
                ( eq-is-prop is-prop-type-trunc-Prop))
              ( eq-is-prop
                ( is-prop-type-Decidable-Prop
                  ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                    ( n)
                    ( X')
                    ( map-orientation-complete-undirected-graph-equiv X X' e d)
                    ( map-orientation-complete-undirected-graph-equiv X X' e d')
                    ( Y)))))
    pr2
      ( preserves-even-difference-orientation-complete-undirected-graph-equiv
          X X' e d d')
      P =
      tr
        ( λ g 
          sim-Eq-Rel
            ( even-difference-orientation-Complete-Undirected-Graph n X)
            ( map-equiv g d)
            ( map-equiv g d'))
        { x =
          orientation-complete-undirected-graph-equiv X' X (inv-equiv e) ∘e
          orientation-complete-undirected-graph-equiv X X' e}
        { y = id-equiv}
        ( ( inv
            ( preserves-comp-orientation-complete-undirected-graph-equiv
                X X' X e (inv-equiv e))) 
          ( ( ap
              ( orientation-complete-undirected-graph-equiv X X)
              ( left-inverse-law-equiv e)) 
            ( preserves-id-equiv-orientation-complete-undirected-graph-equiv
              ( X))))
        ( pr1
          ( preserves-even-difference-orientation-complete-undirected-graph-equiv
            ( X')
            ( X)
            ( inv-equiv e)
            ( map-orientation-complete-undirected-graph-equiv X X' e d)
            ( map-orientation-complete-undirected-graph-equiv X X' e d'))
          ( P))
module _
  {l : Level} {X : UU l}
  (eX : count X) (ineq : leq-ℕ 2 (number-of-elements-count eX))
  where

  cases-orientation-aut-count :
    (e : X  X)
    ( Y : 2-Element-Decidable-Subtype l X)
    ( two-elements : Σ X
      ( λ x  Σ X
        ( λ y  Σ (¬ (Id x y))
          ( λ np 
            Id
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np))
              ( Y))))) 
    is-decidable
      ( Id (map-equiv e (pr1 two-elements)) (pr1 two-elements)) 
    is-decidable
      ( Id (map-equiv e (pr1 (pr2 two-elements))) (pr1 (pr2 two-elements))) 
    Σ X  z  type-Decidable-Prop (pr1 Y z))
  cases-orientation-aut-count
    e Y (pair x (pair y (pair np P))) (inl q) r =
    pair x (tr  Z  type-Decidable-Prop (pr1 Z x)) P (inl refl))
  cases-orientation-aut-count
    e Y (pair x (pair y (pair np P))) (inr nq) (inl nr) =
    pair y (tr  Z  type-Decidable-Prop (pr1 Z y)) P (inr refl))
  cases-orientation-aut-count
    e Y (pair x (pair y (pair np P))) (inr nq) (inr nr) =
    pair x (tr  Z  type-Decidable-Prop (pr1 Z x)) P (inl refl))

  orientation-aut-count :
    X  X 
    orientation-Complete-Undirected-Graph
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX)))
  orientation-aut-count e Y =
    cases-orientation-aut-count e Y
      ( two-elements-transposition eX Y)
      ( has-decidable-equality-count eX
        ( map-equiv e (pr1 (two-elements-transposition eX Y)))
        ( pr1 (two-elements-transposition eX Y)))
      ( has-decidable-equality-count eX
        ( map-equiv e (pr1 (pr2 (two-elements-transposition eX Y))))
        ( pr1 (pr2 (two-elements-transposition eX Y))))

  cases-orientation-two-elements-count :
    ( i j : X)
    ( Y : 2-Element-Decidable-Subtype l X)
    ( two-elements : Σ X
      ( λ x  Σ X
        ( λ y  Σ (¬ (Id x y))
          ( λ np' 
            Id
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np'))
              ( Y))))) 
    is-decidable (Id (pr1 two-elements) i) 
    is-decidable (Id (pr1 two-elements) j) 
    is-decidable (Id (pr1 (pr2 two-elements)) i) 
    Σ X  z  type-Decidable-Prop (pr1 Y z))
  cases-orientation-two-elements-count
    i j Y (pair x (pair y (pair np' P))) (inl q) r s =
    pair y (tr  Z  type-Decidable-Prop (pr1 Z y)) P (inr refl))
  cases-orientation-two-elements-count
    i j Y (pair x (pair y (pair np' P))) (inr nq) (inl r) (inl s) =
    pair x (tr  Z  type-Decidable-Prop (pr1 Z x)) P (inl refl))
  cases-orientation-two-elements-count
    i j Y (pair x (pair y (pair np' P))) (inr nq) (inl r) (inr ns) =
    pair y (tr  Z  type-Decidable-Prop (pr1 Z y)) P (inr refl))
  cases-orientation-two-elements-count
    i j Y (pair x (pair y (pair np' P))) (inr nq) (inr nr) s =
    pair x (tr  Z  type-Decidable-Prop (pr1 Z x)) P (inl refl))

  orientation-two-elements-count :
    (i j : X)  ¬ (Id i j) 
    orientation-Complete-Undirected-Graph
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX)))
  orientation-two-elements-count i j np Y =
    cases-orientation-two-elements-count i j Y
      ( two-elements-transposition eX Y)
      ( has-decidable-equality-count eX
        ( pr1 (two-elements-transposition eX Y)) i)
      ( has-decidable-equality-count eX
        ( pr1 (two-elements-transposition eX Y)) j)
      ( has-decidable-equality-count eX
        ( pr1 (pr2 (two-elements-transposition eX Y))) i)

  first-element-count : X
  first-element-count =
    map-equiv-count
      ( eX)
      ( pr1
        ( two-distinct-elements-leq-2-Fin
          ( number-of-elements-count eX)
          ( ineq)))

  second-element-count : X
  second-element-count =
    map-equiv-count
      ( eX)
      ( pr1
        ( pr2
          ( two-distinct-elements-leq-2-Fin
            ( number-of-elements-count eX)
            ( ineq))))

  abstract
    distinct-two-elements-count :
      ¬ (Id first-element-count second-element-count)
    distinct-two-elements-count p =
      pr2
        ( pr2
          ( two-distinct-elements-leq-2-Fin
            ( number-of-elements-count eX)
            ( ineq)))
        ( is-injective-map-equiv (equiv-count eX) p)

  canonical-2-Element-Decidable-Subtype-count :
    2-Element-Decidable-Subtype l X
  canonical-2-Element-Decidable-Subtype-count =
    standard-2-Element-Decidable-Subtype
      ( has-decidable-equality-count eX)
      ( distinct-two-elements-count)

  canonical-orientation-count :
    orientation-Complete-Undirected-Graph
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX)))
  canonical-orientation-count =
    orientation-two-elements-count
      ( first-element-count)
      ( second-element-count)
      ( distinct-two-elements-count)

  trans-canonical-orientation-count :
    orientation-Complete-Undirected-Graph
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX)))
  trans-canonical-orientation-count =
    orientation-two-elements-count
      ( second-element-count)
      ( first-element-count)
      ( λ p  distinct-two-elements-count (inv p))

  abstract
    cases-inward-edge-left-two-elements-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ¬ (Id x i)  ¬ (Id x j) 
      ( ( Id (pr1 (two-elements-transposition eX Y)) x) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) i)) +
      ( ( Id (pr1 (two-elements-transposition eX Y)) i) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) x)) 
      Id
        ( pr1 (orientation-two-elements-count i j np Y))
        ( x)
    cases-inward-edge-left-two-elements-orientation-count
      i j np Y x nq nr (inl (pair r1 r2)) =
      ( ap
        ( λ d 
          pr1
            ( cases-orientation-two-elements-count i j Y
              ( two-elements-transposition eX Y)
              ( pr1 d)
              ( pr2 d)
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))))
        { x =
          pair
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( i))
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( j))}
        { y = pair (inr  p  nq (inv r1  p))) (inr  p  nr (inv r1  p)))}
        ( eq-pair-Σ
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i)))
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX (pr1 (two-elements-transposition eX Y)) j))))) 
        ( r1)
    cases-inward-edge-left-two-elements-orientation-count
      i j np Y x nq nr (inr (pair r1 r2)) =
      ( ap
        ( λ d 
          pr1
            ( cases-orientation-two-elements-count i j Y
              ( two-elements-transposition eX Y)
              ( d)
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (two-elements-transposition eX Y))
                ( j))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))))
        { x =
          has-decidable-equality-count
            ( eX)
            ( pr1 (two-elements-transposition eX Y))
            ( i)}
        { y = inl r1}
        ( eq-is-prop
          ( is-prop-is-decidable
            ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i)))) 
      ( r2)

    inward-edge-left-two-elements-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y i)) 
      ¬ (Id x i)  ¬ (Id x j) 
      Id
        ( pr1 (orientation-two-elements-count i j np Y))
        ( x)
    inward-edge-left-two-elements-orientation-count i j np Y x p1 p2 nq nr =
      cases-inward-edge-left-two-elements-orientation-count i j np Y x nq nr
        ( eq-two-elements-transposition eX Y x i nq p1 p2)

    cases-inward-edge-left-transposition-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ¬ (Id x i)  ¬ (Id x j) 
      ( ( Id (pr1 (two-elements-transposition eX Y)) x) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) i)) +
      ( ( Id (pr1 (two-elements-transposition eX Y)) i) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) x)) 
      Id
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y)))
        ( x)
    cases-inward-edge-left-transposition-orientation-count
      i j np Y x nq nr (inl (pair r1 r2)) =
      ( ap
        ( λ d 
          pr1
            ( cases-orientation-aut-count
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( Y)
              ( two-elements-transposition eX Y)
              ( d)
              ( has-decidable-equality-count eX
                ( map-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))
                  ( pr1 (pr2 (two-elements-transposition eX Y))))
                ( pr1 (pr2 (two-elements-transposition eX Y))))))
        { x =
          has-decidable-equality-count eX
            ( map-equiv
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( pr1 (two-elements-transposition eX Y)))
            ( pr1 (two-elements-transposition eX Y))}

        { y =
          inl
            ( tr
              ( λ y 
                Id
                  ( map-equiv
                    ( transposition
                      ( standard-2-Element-Decidable-Subtype
                        ( has-decidable-equality-count eX)
                        ( np)))
                    ( y))
                  ( y))
              ( inv r1)
              ( is-fixed-point-standard-transposition
                ( has-decidable-equality-count eX)
                ( np)
                ( x)
                ( λ q  nq (inv q))
                ( λ r  nr (inv r))))}
        ( eq-is-prop
          ( is-prop-is-decidable
            ( is-set-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( pr1 (two-elements-transposition eX Y)))
              ( pr1 (two-elements-transposition eX Y)))))) 
        ( r1)
    cases-inward-edge-left-transposition-orientation-count
      i j np Y x nq nr (inr (pair r1 r2)) =
      ( ap
        ( λ w 
          pr1
            ( cases-orientation-aut-count
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( Y)
              ( two-elements-transposition eX Y)
              ( pr1 w)
              ( pr2 w)))
        { x =
          pair
            ( has-decidable-equality-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( pr1 (two-elements-transposition eX Y)))
              ( pr1 (two-elements-transposition eX Y)))
            ( has-decidable-equality-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( pr1 (pr2 (two-elements-transposition eX Y))))
              ( pr1 (pr2 (two-elements-transposition eX Y))))}
        { y =
          pair
            ( inr
              ( λ s 
                np
                  ( inv r1 
                    ( inv s 
                       tr
                        ( λ y 
                          Id
                            ( map-equiv
                              ( transposition
                                ( standard-2-Element-Decidable-Subtype
                                  ( has-decidable-equality-count eX)
                                  ( np)))
                              ( y))
                            ( j))
                        ( inv r1)
                        ( left-computation-standard-transposition
                          ( has-decidable-equality-count eX)
                          ( np))))))
            ( inl
              ( tr
                ( λ y 
                  Id
                    ( map-equiv
                      ( transposition
                        ( standard-2-Element-Decidable-Subtype
                          ( has-decidable-equality-count eX)
                          ( np)))
                      ( y))
                    ( y))
                ( inv r2)
                ( is-fixed-point-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np)
                  ( x)
                  ( λ q  nq (inv q))
                  ( λ r  nr (inv r)))))}
        ( eq-pair-Σ
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX
                ( map-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))
                  ( pr1 (two-elements-transposition eX Y)))
                ( pr1 (two-elements-transposition eX Y)))))
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX
                ( map-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))
                  ( pr1 (pr2 (two-elements-transposition eX Y))))
                ( pr1 (pr2 (two-elements-transposition eX Y)))))))) 
        ( r2)

    inward-edge-left-transposition-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y i)) 
      ¬ (Id x i)  ¬ (Id x j) 
      Id
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y)))
        ( x)
    inward-edge-left-transposition-orientation-count i j np Y x p1 p2 nq nr =
      cases-inward-edge-left-transposition-orientation-count i j np Y x nq nr
        ( eq-two-elements-transposition eX Y x i nq p1 p2)

    cases-inward-edge-right-two-elements-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ¬ (Id x i)  ¬ (Id x j) 
      ( ( Id (pr1 (two-elements-transposition eX Y)) x) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) j)) +
      ( ( Id (pr1 (two-elements-transposition eX Y)) j) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) x)) 
      Id
        ( pr1 (orientation-two-elements-count i j np Y))
        ( x)
    cases-inward-edge-right-two-elements-orientation-count
      i j np Y x nq nr (inl (pair r1 r2)) =
      ( ap
        ( λ d 
          pr1
            ( cases-orientation-two-elements-count i j Y
              ( two-elements-transposition eX Y)
              ( pr1 d)
              ( pr2 d)
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))))
        { x =
          pair
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( i))
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( j))}
        { y = pair (inr  p  nq (inv r1  p))) (inr  p  nr (inv r1  p)))}
        ( eq-pair-Σ
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i)))
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX (pr1 (two-elements-transposition eX Y)) j))))) 
        ( r1)
    cases-inward-edge-right-two-elements-orientation-count
      i j np Y x nq nr (inr (pair r1 r2)) =
      ( ap
        ( λ d 
          pr1
            ( cases-orientation-two-elements-count i j Y
              ( two-elements-transposition eX Y)
              ( pr1 d)
              ( pr2 d)
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))))
        { x =
          pair
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( i))
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( j))}
        { y = pair (inr λ p  np (inv p  r1)) (inl r1)}
        ( eq-pair-Σ
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i)))
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX (pr1 (two-elements-transposition eX Y)) j))))) 
        ( ( ap
          ( λ d 
            pr1
              ( cases-orientation-two-elements-count i j Y
                ( two-elements-transposition eX Y)
                ( inr λ p  np (inv p  r1))
                ( inl r1)
                ( d)))
          { x =
            has-decidable-equality-count
              ( eX)
              ( pr1 (pr2 (two-elements-transposition eX Y)))
              ( i)}
          { y = inr  q  nq (inv r2  q))}
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))))) 
          ( r2))

    inward-edge-right-two-elements-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y j)) 
      ¬ (Id x i)  ¬ (Id x j) 
      Id
        ( pr1 (orientation-two-elements-count i j np Y))
        ( x)
    inward-edge-right-two-elements-orientation-count i j np Y x p1 p2 nq nr =
      cases-inward-edge-right-two-elements-orientation-count i j np Y x nq nr
        ( eq-two-elements-transposition eX Y x j nr p1 p2)

    cases-inward-edge-right-transposition-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ¬ (Id x i)  ¬ (Id x j) 
      ( ( Id (pr1 (two-elements-transposition eX Y)) x) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) j)) +
      ( ( Id (pr1 (two-elements-transposition eX Y)) j) ×
        ( Id (pr1 (pr2 (two-elements-transposition eX Y))) x)) 
      Id
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y)))
        ( x)
    cases-inward-edge-right-transposition-orientation-count
      i j np Y x nq nr (inl (pair r1 r2)) =
      ( ap
        ( λ d 
          pr1
            ( cases-orientation-aut-count
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( Y)
              ( two-elements-transposition eX Y)
              ( d)
              ( has-decidable-equality-count eX
                ( map-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))
                  ( pr1 (pr2 (two-elements-transposition eX Y))))
                ( pr1 (pr2 (two-elements-transposition eX Y))))))
        { x =
          has-decidable-equality-count eX
            ( map-equiv
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( pr1 (two-elements-transposition eX Y)))
            ( pr1 (two-elements-transposition eX Y))}
        { y =
          inl
            ( tr
              ( λ y 
                Id
                  ( map-equiv
                    ( transposition
                      ( standard-2-Element-Decidable-Subtype
                        ( has-decidable-equality-count eX)
                        ( np)))
                    ( y))
                  ( y))
              ( inv r1)
              ( is-fixed-point-standard-transposition
                ( has-decidable-equality-count eX)
                ( np)
                ( x)
                ( λ q  nq (inv q))
                ( λ r  nr (inv r))))}
        ( eq-is-prop
          ( is-prop-is-decidable
            ( is-set-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( pr1 (two-elements-transposition eX Y)))
              ( pr1 (two-elements-transposition eX Y)))))) 
        ( r1)
    cases-inward-edge-right-transposition-orientation-count
      i j np Y x nq nr (inr (pair r1 r2)) =
      ( ap
        ( λ w 
          pr1
            ( cases-orientation-aut-count
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( Y)
              ( two-elements-transposition eX Y)
              ( pr1 w)
              ( pr2 w)))
        { x =
          pair
            ( has-decidable-equality-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( pr1 (two-elements-transposition eX Y)))
              ( pr1 (two-elements-transposition eX Y)))
            ( has-decidable-equality-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( pr1 (pr2 (two-elements-transposition eX Y))))
              ( pr1 (pr2 (two-elements-transposition eX Y))))}
        { y =
          pair
            ( inr
               λ s 
                np
                  ( ( tr
                    ( λ y 
                      Id
                        ( i)
                        ( map-equiv
                          ( transposition
                            ( standard-2-Element-Decidable-Subtype
                              ( has-decidable-equality-count eX)
                              ( np)))
                          ( y)))
                    ( inv r1)
                    ( inv
                      ( right-computation-standard-transposition
                        ( has-decidable-equality-count eX)
                        ( np))) 
                    ( s  r1))))
            ( inl
              ( tr
                ( λ y 
                  Id
                    ( map-equiv
                      ( transposition
                        ( standard-2-Element-Decidable-Subtype
                          ( has-decidable-equality-count eX)
                          ( np)))
                      ( y))
                    ( y))
                ( inv r2)
                ( is-fixed-point-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np)
                  ( x)
                  ( λ q  nq (inv q))
                  ( λ r  nr (inv r)))))}
        ( eq-pair-Σ
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX
                ( map-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))
                  ( pr1 (two-elements-transposition eX Y)))
                ( pr1 (two-elements-transposition eX Y)))))
          ( eq-is-prop
            ( is-prop-is-decidable
              ( is-set-count eX
                ( map-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))
                  ( pr1 (pr2 (two-elements-transposition eX Y))))
                ( pr1 (pr2 (two-elements-transposition eX Y)))))))) 
        ( r2)

    inward-edge-right-transposition-orientation-count :
      (i j : X) (np : ¬ (Id i j))
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y j)) 
      ¬ (Id x i)  ¬ (Id x j) 
      Id
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y)))
        ( x)
    inward-edge-right-transposition-orientation-count i j np Y x p1 p2 nq nr =
      cases-inward-edge-right-transposition-orientation-count i j np Y x nq nr
        ( eq-two-elements-transposition eX Y x j nr p1 p2)

    cases-eq-orientation-two-elements-count :
      ( i j : X)
      ( np : ¬ (Id i j))
      ( two-elements : Σ X
        ( λ x  Σ X
          ( λ y  Σ (¬ (Id x y))
            ( λ np' 
              Id
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np'))
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))))) 
      (q : is-decidable (Id (pr1 two-elements) i)) 
      (r : is-decidable (Id (pr1 two-elements) j)) 
      (s : is-decidable (Id (pr1 (pr2 two-elements)) i)) 
      (t : is-decidable (Id (pr1 (pr2 two-elements)) j)) 
      Id
        ( pr1
          ( cases-orientation-two-elements-count i j
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))
            ( two-elements)
            ( q)
            ( r)
            ( s)))
        ( j)
    cases-eq-orientation-two-elements-count
      i j np (pair x (pair y (pair np' P))) (inl q) r s (inl t) = t
    cases-eq-orientation-two-elements-count
      i j np (pair x (pair y (pair np' P))) (inl q) r s (inr nt) =
      ex-falso
        ( nt
          ( ( inv
            ( left-computation-standard-transposition
              ( has-decidable-equality-count eX)
              ( np'))) 
            ( ( ap
              ( map-standard-transposition
                ( has-decidable-equality-count eX)
                ( np'))
              ( q)) 
              ( ( ap  Y  map-transposition Y i) P) 
                ( left-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np))))))
    cases-eq-orientation-two-elements-count
      i j np (pair x (pair y (pair np' P))) (inr nq) (inl r) (inl s) t = r
    cases-eq-orientation-two-elements-count
      i j np (pair x (pair y (pair np' P))) (inr nq) (inl r) (inr ns) t =
      ex-falso
        ( ns
          ( ( inv
              ( left-computation-standard-transposition
                ( has-decidable-equality-count eX)
                ( np'))) 
            ( ( ap
                ( map-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np'))
                ( r)) 
              ( ( ap  Y  map-transposition Y j) P) 
                ( right-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np))))))
    cases-eq-orientation-two-elements-count
      i j np (pair x (pair y (pair np' P))) (inr nq) (inr nr) s t =
      ex-falso
        ( contradiction-3-distinct-element-2-Element-Type
          ( 2-element-type-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))
          ( pair i (inl refl))
          ( pair j (inr refl))
          ( pair
            ( x)
            (tr  Y  type-Decidable-Prop (pr1 Y x)) P (inl refl)))
          ( λ eq  np (pr1 (pair-eq-Σ eq)))
          ( λ eq  nr (inv (pr1 (pair-eq-Σ eq))))
          ( λ eq  nq (inv (pr1 (pair-eq-Σ eq)))))

    eq-orientation-two-elements-count :
      (i j : X) (np : ¬ (Id i j)) 
      Id
        ( pr1
          ( orientation-two-elements-count i j np
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( j)
    eq-orientation-two-elements-count i j np =
      cases-eq-orientation-two-elements-count i j np
        ( two-elements-transposition eX
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np)))
        ( has-decidable-equality-count eX
          ( pr1
            ( two-elements-transposition eX
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np))))
          ( i))
        ( has-decidable-equality-count eX
          ( pr1
          ( two-elements-transposition eX
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
          ( j))
        ( has-decidable-equality-count eX
          ( pr1
          ( pr2
            ( two-elements-transposition eX
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))))
          ( i))
        ( has-decidable-equality-count eX
          ( pr1
            ( pr2
              ( two-elements-transposition eX
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))))
          ( j))

  cases-eq-orientation-aut-orientation-two-elements-count-left :
    ( i j : X) (np : ¬ (Id i j)) 
    ( Id
      ( pr1
        ( orientation-aut-count
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( j)) 
    ( Y : 2-Element-Decidable-Subtype l X) 
    ( two-elements : Σ X
      ( λ x  Σ X
        ( λ y  Σ (¬ (Id x y))
          ( λ np' 
            Id
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np'))
              ( Y))))) 
    Id (two-elements-transposition eX Y) two-elements 
    is-decidable (Id (pr1 two-elements) i) 
    is-decidable (Id (pr1 two-elements) j) 
    is-decidable (Id (pr1 (pr2 two-elements)) i) 
    is-decidable (Id (pr1 (pr2 two-elements)) j) 
    Id
      ( pr1
        ( orientation-aut-count
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( Y)))
      ( pr1 (orientation-two-elements-count i j np Y))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P))) R (inl q) r s (inl t) =
    ( ap
      ( λ Y' 
        pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y')))
      ( inv P 
        ( eq-equal-elements-standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np')
          ( np)
          ( q)
          ( t)))) 
      ( Q 
        ( ( inv (eq-orientation-two-elements-count i j np)) 
          ( ap
            ( λ Y'  pr1 (orientation-two-elements-count i j np Y'))
            ( ( eq-equal-elements-standard-2-Element-Decidable-Subtype
              (has-decidable-equality-count eX)
              ( np)
              ( np')
              ( inv q)
              ( inv t)) 
              ( P)))))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P))) R (inl q) r s (inr nt) =
    ( inward-edge-left-transposition-orientation-count i j np Y y
      ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inl q))
      ( λ s'  np' (q  inv s'))
      ( nt)) 
      ( inv
        ( inward-edge-left-two-elements-orientation-count i j np Y y
          ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inl q))
          ( λ s'  np' (q  inv s'))
          ( nt)))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P))) R (inr nq) (inl r) (inl s) t =
    ( ap
      ( λ Y' 
        pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y')))
      ( inv P 
        ( ( is-commutative-standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np')) 
          ( eq-equal-elements-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( λ p  np' (inv p))
            ( np)
            ( s)
            ( r))))) 
      ( Q 
        ( ( inv (eq-orientation-two-elements-count i j np)) 
          ( ap
            ( λ Y'  pr1 (orientation-two-elements-count i j np Y'))
            ( eq-equal-elements-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)
              ( λ p  np' (inv p))
              ( inv s)
              ( inv r) 
              ( ( inv
                ( is-commutative-standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np'))) 
                ( P))))))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P))) R (inr nq) (inl r) (inr ns) t =
    ( inward-edge-right-transposition-orientation-count i j np Y y
      ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inl r))
      ( ns)
      ( λ t'  np' (r  inv t'))) 
      ( inv
        ( inward-edge-right-two-elements-orientation-count i j np Y y
          ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inl r))
          ( ns)
          ( λ t'  np' (r  inv t'))))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P))) R (inr nq) (inr nr) (inl s) t =
    ( inward-edge-left-transposition-orientation-count i j np Y x
      ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inr s))
      ( nq)
      ( nr)) 
      ( inv
        ( inward-edge-left-two-elements-orientation-count i j np Y x
          ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inr s))
          ( nq)
          ( nr)))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P)))
    R (inr nq) (inr nr) (inr ns) (inl t) =
    ( inward-edge-right-transposition-orientation-count i j np Y x
      ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inr t))
      ( nq)
      ( nr)) 
      ( inv
        ( inward-edge-right-two-elements-orientation-count i j np Y x
          ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inr t))
          ( nq)
          ( nr)))
  cases-eq-orientation-aut-orientation-two-elements-count-left
    i j np Q Y (pair x (pair y (pair np' P)))
    R (inr nq) (inr nr) (inr ns) (inr nt) =
    ( ap
      ( λ w 
        pr1
          ( cases-orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y)
            ( pr1 w)
            ( pr2 w)
            ( has-decidable-equality-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                (pr1 (pr2 (pr1 w))))
              (pr1 (pr2 (pr1 w))))))
      { x =
        pair
          ( two-elements-transposition eX Y)
          ( has-decidable-equality-count eX
            ( map-equiv
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( pr1 (two-elements-transposition eX Y)))
            ( pr1 (two-elements-transposition eX Y)))}
      { y =
        pair
          ( pair x (pair y (pair np' P)))
          ( inl
            ( is-fixed-point-standard-transposition
              ( has-decidable-equality-count eX)
              ( np)
              ( x)
              ( λ q  nq (inv q))
              ( λ r  nr (inv r))))}
      ( eq-pair-Σ
        ( R)
        ( eq-is-prop
          ( is-prop-is-decidable
            ( is-set-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( x))
              ( x)))))) 
      ( ap
        ( λ w 
          pr1
            ( cases-orientation-two-elements-count i j Y
              ( pair x (pair y (pair np' P)))
              ( pr1 w)
              ( pr2 w)
              ( has-decidable-equality-count eX y i)))
        { x = pair (inr nq) (inr nr)}
        { y =
          pair
            ( has-decidable-equality-count eX x i)
            ( has-decidable-equality-count eX x j)}
        ( eq-pair-Σ
          ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))
          ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))) 
        ap
          ( λ k 
            pr1
              ( cases-orientation-two-elements-count i j Y k
                ( has-decidable-equality-count eX (pr1 k) i)
                ( has-decidable-equality-count eX (pr1 k) j)
                ( has-decidable-equality-count eX (pr1 (pr2 k)) i)))
          ( inv R))

  cases-eq-orientation-aut-orientation-two-elements-count-right :
    ( i j : X) (np : ¬ (Id i j)) 
    ( Id
      ( pr1
        ( orientation-aut-count
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( i)) 
    ( Y : 2-Element-Decidable-Subtype l X) 
    ( two-elements : Σ X
      ( λ x  Σ X
        ( λ y  Σ (¬ (Id x y))
          ( λ np' 
            Id
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np'))
              ( Y))))) 
    Id (two-elements-transposition eX Y) two-elements 
    is-decidable (Id (pr1 two-elements) i) 
    is-decidable (Id (pr1 two-elements) j) 
    is-decidable (Id (pr1 (pr2 two-elements)) i) 
    is-decidable (Id (pr1 (pr2 two-elements)) j) 
    Id
      ( pr1
        ( orientation-aut-count
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( Y)))
      ( pr1 (orientation-two-elements-count j i (np  inv) Y))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P))) R (inl q) r s (inl t) =
    ( ap
      ( λ Y' 
        pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y')))
      ( inv P 
        ( eq-equal-elements-standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np')
          ( np)
          ( q)
          ( t)))) 
      ( Q 
        ( ( inv (eq-orientation-two-elements-count j i (np  inv))) 
           ap
            ( pr1  orientation-two-elements-count j i (np  inv))
            ( ( is-commutative-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np  inv)) 
              ( ( eq-equal-elements-standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( λ p  np (inv (inv p)))
                ( np')
                ( inv q)
                ( inv t)) 
                ( P)))))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P))) R (inl q) r s (inr nt) =
    ( inward-edge-left-transposition-orientation-count i j np Y y
      ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inl q))
      ( λ s'  np' (q  inv s'))
      ( nt)) 
      ( inv
        ( inward-edge-right-two-elements-orientation-count
          ( j)
          ( i)
          ( np  inv)
          ( Y)
          ( y)
          ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inl q))
          ( nt)
          ( λ s'  np' (q  inv s'))))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P))) R (inr nq) (inl r) (inl s) t =
    ( ap
      ( λ Y' 
        pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y')))
      ( inv P 
        ( ( is-commutative-standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np')) 
          ( eq-equal-elements-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( λ p  np' (inv p))
            ( np)
            ( s)
            ( r))))) 
      ( Q 
        ( ( inv (eq-orientation-two-elements-count j i (np  inv))) 
          ( ap
            ( pr1  orientation-two-elements-count j i (np  inv))
            ( eq-equal-elements-standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np  inv)
                ( np')
                ( inv r)
                ( inv s) 
                ( P)))))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P))) R (inr nq) (inl r) (inr ns) t =
    ( inward-edge-right-transposition-orientation-count i j np Y y
      ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inl r))
      ( ns)
      ( λ t'  np' (r  inv t'))) 
      ( inv
        ( inward-edge-left-two-elements-orientation-count
          ( j)
          ( i)
          ( np  inv)
          ( Y)
          ( y)
          ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inl r))
          ( λ t'  np' (r  inv t'))
          ( ns)))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P))) R (inr nq) (inr nr) (inl s) t =
    ( inward-edge-left-transposition-orientation-count i j np Y x
      ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inr s))
      ( nq)
      ( nr)) 
      ( inv
        ( inward-edge-right-two-elements-orientation-count
          ( j)
          ( i)
          ( np  inv)
          ( Y)
          ( x)
          ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inr s))
          ( nr)
          ( nq)))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P)))
    R (inr nq) (inr nr) (inr ns) (inl t) =
    ( inward-edge-right-transposition-orientation-count i j np Y x
      ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
      ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inr t))
      ( nq)
      ( nr)) 
      ( inv
        ( inward-edge-left-two-elements-orientation-count
          ( j)
          ( i)
          ( np  inv)
          ( Y)
          ( x)
          ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
          ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inr t))
          ( nr)
          ( nq)))
  cases-eq-orientation-aut-orientation-two-elements-count-right
    i j np Q Y (pair x (pair y (pair np' P)))
    R (inr nq) (inr nr) (inr ns) (inr nt) =
    ( ap
      ( λ w 
        pr1
          ( cases-orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( Y)
            ( pr1 w)
            ( pr2 w)
            ( has-decidable-equality-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                (pr1 (pr2 (pr1 w))))
              (pr1 (pr2 (pr1 w))))))
      { x =
        pair
          ( two-elements-transposition eX Y)
          ( has-decidable-equality-count eX
            ( map-equiv
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( pr1 (two-elements-transposition eX Y)))
            ( pr1 (two-elements-transposition eX Y)))}
      { y =
        pair
          ( pair x (pair y (pair np' P)))
          ( inl
            ( is-fixed-point-standard-transposition
              ( has-decidable-equality-count eX)
              ( np)
              ( x)
              ( λ q  nq (inv q))
              ( λ r  nr (inv r))))}
      ( eq-pair-Σ
        ( R)
        ( eq-is-prop
          ( is-prop-is-decidable
            ( is-set-count eX
              ( map-equiv
                ( transposition
                  ( standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np)))
                ( x))
              ( x)))))) 
      ( ap
        ( λ w 
          pr1
            ( cases-orientation-two-elements-count j i Y
              ( pair x (pair y (pair np' P)))
              ( pr1 w)
              ( pr2 w)
              ( has-decidable-equality-count eX y j)))
        { x = pair (inr nr) (inr nq)}
        { y =
          pair
            ( has-decidable-equality-count eX x j)
            ( has-decidable-equality-count eX x i)}
        ( eq-pair-Σ
          ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))
          ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))) 
        ( ap
          ( λ k 
            pr1
              ( cases-orientation-two-elements-count j i Y k
                ( has-decidable-equality-count eX (pr1 k) j)
                ( has-decidable-equality-count eX (pr1 k) i)
                ( has-decidable-equality-count eX (pr1 (pr2 k)) j)))
          ( inv R)))

  cases-eq-orientation-aut-orientation-two-elements-count :
    ( i j : X) (np : ¬ (Id i j)) 
    is-decidable
      ( Id
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( j)) 
    ( Id
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( orientation-two-elements-count i j np)) +
    ( Id
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( orientation-two-elements-count j i (np  inv)))
  cases-eq-orientation-aut-orientation-two-elements-count i j np (inl q) =
    inl
      ( eq-htpy
        ( λ Y 
          eq-pair-Σ
            ( cases-eq-orientation-aut-orientation-two-elements-count-left
              ( i)
              ( j)
              ( np)
              ( q)
              ( Y)
              ( two-elements-transposition eX Y)
              ( refl)
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (two-elements-transposition eX Y))
                ( i))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (two-elements-transposition eX Y))
                ( j))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( j)))
            ( eq-is-prop
              ( is-prop-type-Decidable-Prop
                ( pr1 Y (pr1 (orientation-two-elements-count i j np Y)))))))
  cases-eq-orientation-aut-orientation-two-elements-count i j np (inr nq) =
    inr
      ( eq-htpy
        ( λ Y 
          eq-pair-Σ
            ( cases-eq-orientation-aut-orientation-two-elements-count-right
              ( i)
              ( j)
              ( np)
              ( q'
                ( has-decidable-equality-count eX
                  ( pr1
                    ( orientation-aut-count
                      ( transposition
                        ( standard-2-Element-Decidable-Subtype
                          ( has-decidable-equality-count eX)
                          ( np)))
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np))))
                  ( i)))
              ( Y)
              ( two-elements-transposition eX Y)
              ( refl)
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (two-elements-transposition eX Y))
                ( i))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (two-elements-transposition eX Y))
                ( j))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( i))
              ( has-decidable-equality-count
                ( eX)
                ( pr1 (pr2 (two-elements-transposition eX Y)))
                ( j)))
            ( eq-is-prop
              ( is-prop-type-Decidable-Prop
                ( pr1
                  ( Y)
                  ( pr1
                    ( orientation-two-elements-count
                        j i (np  inv) Y)))))))
    where
    q' :
      is-decidable
        ( Id
          ( pr1
            ( orientation-aut-count
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np))))
          ( i)) 
      Id
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( i)
    q' (inl r) = r
    q' (inr nr) =
      ex-falso
        ( contradiction-3-distinct-element-2-Element-Type
          ( 2-element-type-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))
          ( pair i (inl refl))
          ( pair j (inr refl))
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( λ p  np (pr1 (pair-eq-Σ p)))
          ( λ q  nq (pr1 (pair-eq-Σ (inv q))))
          ( λ r  nr (pr1 (pair-eq-Σ (inv r)))))

  eq-orientation-aut-orientation-two-elements-count :
    ( i j : X) (np : ¬ (Id i j)) 
    ( Id
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
              ( np))))
      ( orientation-two-elements-count i j np)) +
    ( Id
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( orientation-two-elements-count j i (np  inv)))
  eq-orientation-aut-orientation-two-elements-count i j np =
    cases-eq-orientation-aut-orientation-two-elements-count i j np
      (has-decidable-equality-count eX
        ( pr1
          ( orientation-aut-count
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np)))
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( j))

  cases-eq-map-orientation-transposition-orientation-two-elements-count :
    ( i j : X) (np : ¬ (Id i j))
    ( Y : 2-Element-Decidable-Subtype l X)
    ( two-elements :
      Σ X
        ( λ x  Σ X
          ( λ y  Σ (¬ (Id x y))
            ( λ np' 
              Id
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np'))
                ( Y))))) 
    Id (two-elements-transposition eX Y) two-elements 
    is-decidable (Id (pr1 two-elements) i) 
    is-decidable (Id (pr1 two-elements) j) 
    is-decidable (Id (pr1 (pr2 two-elements)) i) 
    is-decidable (Id (pr1 (pr2 two-elements)) j) 
    Id
      ( pr1
        ( map-orientation-complete-undirected-graph-equiv
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( orientation-two-elements-count i j np)
          ( Y)))
      ( pr1 ( orientation-two-elements-count j i (np  inv) Y))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P))) R (inl q) r s (inl t) =
    ( ap
      ( λ Y' 
        map-inv-equiv
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( pr1
            ( orientation-two-elements-count i j np Y')))
      ( ( ap
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( inv P 
          ( eq-equal-elements-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np')
            ( np)
            ( q)
            ( t)))) 
        ( eq-transposition-precomp-standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np)))) 
      ( ( ap
        ( map-inv-equiv
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( eq-orientation-two-elements-count i j np)) 
        ( ( ap
          ( λ e  map-equiv e j)
          { x =
            inv-equiv
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))}
          ( own-inverse-is-involution
            ( is-involution-map-transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np))))) 
          ( ( right-computation-standard-transposition
              ( has-decidable-equality-count eX)
              ( np)) 
            ( inv (eq-orientation-two-elements-count j i (np  inv)) 
              ( ap
              ( λ Y'  pr1 (orientation-two-elements-count j i (np  inv) Y'))
              ( ( is-commutative-standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np  inv)) 
                ( ( eq-equal-elements-standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( λ p  np (inv (inv p)))
                  ( np')
                  ( inv q)
                  ( inv t)) 
                  ( P))))))))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P))) R (inl q) r s (inr nt) =
    ( ap
      ( map-inv-equiv
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( inward-edge-right-two-elements-orientation-count i j np
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( Y))
        ( y)
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( y)))
          ( P)
          ( inr
            ( inv
              ( is-fixed-point-standard-transposition
                ( has-decidable-equality-count eX)
                ( np)
                ( y)
                ( λ s'  np' (q  s'))
                ( λ t  nt (inv t))))))
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( j)))
          ( P)
          ( inl
            ( q 
              ( inv
                ( right-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np))))))
        ( λ s'  np' (q  inv s'))
        ( nt))) 
      ( ( is-fixed-point-standard-transposition
        ( has-decidable-equality-count eX)
        ( np)
        ( y)
        ( λ s'  np' (q  s'))
        ( λ t  nt (inv t))) 
        ( inv
          ( inward-edge-right-two-elements-orientation-count j i (np  inv) Y y
            ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
            ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inl q))
            ( nt)
            ( λ s'  np' (q  inv s')))))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P))) R (inr nq) (inl r) (inl s) t =
    ( ap
      ( λ Y' 
        map-inv-equiv
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( pr1
            ( orientation-two-elements-count i j np Y')))
      ( ( ap
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( inv P 
          ( is-commutative-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np') 
            ( eq-equal-elements-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( λ p  np' (inv p))
              ( np)
              ( s)
              ( r))))) 
        ( eq-transposition-precomp-standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np)))) 
      ( ( ap
        ( map-inv-equiv
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))
        ( eq-orientation-two-elements-count i j np)) 
        ( ( ap
          ( λ e  map-equiv e j)
          { x =
            inv-equiv
              ( transposition
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np)))}
          ( own-inverse-is-involution
            ( is-involution-map-transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np))))) 
          ( ( right-computation-standard-transposition
              ( has-decidable-equality-count eX)
              ( np)) 
            ( ( inv (eq-orientation-two-elements-count j i (np  inv))) 
              ( ap
                ( pr1  orientation-two-elements-count j i (np  inv))
                ( eq-equal-elements-standard-2-Element-Decidable-Subtype
                    ( has-decidable-equality-count eX)
                    ( np  inv)
                    ( np')
                    ( inv r)
                    ( inv s) 
                    ( P)))))))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P))) R (inr nq) (inl r) (inr ns) t =
     ap
      ( map-inv-equiv
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( inward-edge-left-two-elements-orientation-count i j np
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( Y))
        ( y)
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( y)))
          ( P)
          ( inr
            ( inv
              ( is-fixed-point-standard-transposition
                ( has-decidable-equality-count eX)
                ( np)
                ( y)
                ( λ s'  ns (inv s'))
                ( λ t  np' (r  t))))))
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( i)))
          ( P)
          ( inl
            ( r 
               inv
                ( left-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np)))))
        ( ns)
        ( λ t  np' (r  inv t))) 
      ( ( is-fixed-point-standard-transposition
        ( has-decidable-equality-count eX)
        ( np)
        ( y)
        ( λ s'  ns (inv s'))
        ( λ t  np' (r  t))) 
        ( inv
          ( inward-edge-left-two-elements-orientation-count j i (np  inv) Y y
            ( tr  Y'  type-Decidable-Prop (pr1 Y' y)) P (inr refl))
            ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inl r))
            ( λ t'  np' (r  inv t'))
            ( ns))))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P))) R (inr nq) (inr nr) (inl s) t =
     ap
      ( map-inv-equiv
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( inward-edge-right-two-elements-orientation-count i j np
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( Y))
        ( x)
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( x)))
          ( P)
          ( inl
            ( inv
              ( is-fixed-point-standard-transposition
                ( has-decidable-equality-count eX)
                ( np)
                ( x)
                ( λ q  nq (inv q))
                ( λ r  nr (inv r))))))
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( j)))
          ( P)
          ( inr
            ( s 
              ( inv
                ( right-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np))))))
        ( nq)
        ( nr)) 
      ( is-fixed-point-standard-transposition
        ( has-decidable-equality-count eX)
        ( np)
        ( x)
        ( λ q  nq (inv q))
        ( λ r  nr (inv r)) 
        ( inv
          ( inward-edge-right-two-elements-orientation-count j i (np  inv) Y x
            ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
            ( tr  Y'  type-Decidable-Prop (pr1 Y' i)) P (inr s))
            ( nr)
            ( nq))))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P)))
    R (inr nq) (inr nr) (inr ns) (inl t) =
    ( ap
      ( map-inv-equiv
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( inward-edge-left-two-elements-orientation-count i j np
        ( precomp-equiv-2-Element-Decidable-Subtype
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
          ( Y))
        ( x)
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( x)))
          ( P)
          ( inl
            ( inv
              ( is-fixed-point-standard-transposition
                ( has-decidable-equality-count eX)
                ( np)
                ( x)
                ( λ q  nq (inv q))
                ( λ r  nr (inv r))))))
        ( tr
          ( λ Y' 
            type-Decidable-Prop
              ( ( pr1 Y' 
                ( map-inv-equiv
                  ( transposition
                    ( standard-2-Element-Decidable-Subtype
                      ( has-decidable-equality-count eX)
                      ( np)))))
                ( i)))
          ( P)
          ( inr
            ( t 
               inv
                ( left-computation-standard-transposition
                  ( has-decidable-equality-count eX)
                  ( np)))))
        ( nq)
        ( nr))) 
      ( ( is-fixed-point-standard-transposition
        ( has-decidable-equality-count eX)
        ( np)
        ( x)
        ( λ q  nq (inv q))
        ( λ r  nr (inv r))) 
        ( inv
          ( inward-edge-left-two-elements-orientation-count j i (np  inv) Y x
            ( tr  Y'  type-Decidable-Prop (pr1 Y' x)) P (inl refl))
            ( tr  Y'  type-Decidable-Prop (pr1 Y' j)) P (inr t))
            ( nr)
            ( nq))))
  cases-eq-map-orientation-transposition-orientation-two-elements-count
    i j np Y (pair x (pair y (pair np' P)))
    R (inr nq) (inr nr) (inr ns) (inr nt) =
    ( ap
      ( map-inv-equiv
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( ( ap
        ( λ Y' 
          pr1
            ( orientation-two-elements-count i j np Y'))
        ( ( ap
          ( precomp-equiv-2-Element-Decidable-Subtype
            ( transposition
              ( standard-2-Element-Decidable-Subtype
                ( has-decidable-equality-count eX)
                ( np))))
          ( inv P)) 
          ( ( eq-transposition-precomp-ineq-standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np)
            ( np')
            ( λ q  nq (inv q))
            ( λ s  ns (inv s))
            ( λ r  nr (inv r))
            ( λ t  nt (inv t))) 
            ( P)))) 
        ( ( ap
          ( λ k 
            pr1
              ( cases-orientation-two-elements-count i j Y k
                ( has-decidable-equality-count eX (pr1 k) i)
                ( has-decidable-equality-count eX (pr1 k) j)
                ( has-decidable-equality-count eX (pr1 (pr2 k)) i)))
          ( R)) 
          ( ap
            ( λ w 
              pr1
                ( cases-orientation-two-elements-count i j Y
                  ( pair x (pair y (pair np' P)))
                  ( pr1 w)
                  ( pr2 w)
                  ( has-decidable-equality-count eX y i)))
            { x =
              pair
                ( has-decidable-equality-count eX x i)
                ( has-decidable-equality-count eX x j)}
            { y = pair (inr nq) (inr nr)}
            ( eq-pair-Σ
              ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))
              ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))))))) 
      ( ( is-fixed-point-standard-transposition
        ( has-decidable-equality-count eX)
        ( np)
        ( x)
        ( λ q  nq (inv q))
        ( λ r  nr (inv r))) 
        ( ( ap
          ( λ w 
            pr1
              ( cases-orientation-two-elements-count j i Y
                ( pair x (pair y (pair np' P)))
                ( pr1 w)
                ( pr2 w)
                ( has-decidable-equality-count eX y j)))
          { x = pair (inr nr) (inr nq)}
          { y =
            pair
              ( has-decidable-equality-count eX x j)
              ( has-decidable-equality-count eX x i)}
          ( eq-pair-Σ
            ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))
            ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i))))) 
          ( ap
            ( λ k 
              pr1
                ( cases-orientation-two-elements-count j i Y k
                  ( has-decidable-equality-count eX (pr1 k) j)
                  ( has-decidable-equality-count eX (pr1 k) i)
                  ( has-decidable-equality-count eX (pr1 (pr2 k)) j)))
            ( inv R))))

  eq-map-orientation-transposition-orientation-two-elements-count :
    ( i j : X) (np : ¬ (Id i j)) 
    Id
      ( map-orientation-complete-undirected-graph-equiv
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np)))
        ( orientation-two-elements-count i j np))
      ( orientation-two-elements-count j i (np  inv))
  eq-map-orientation-transposition-orientation-two-elements-count i j np =
    eq-htpy
      ( λ Y 
        eq-pair-Σ
          ( cases-eq-map-orientation-transposition-orientation-two-elements-count
            ( i)
            ( j)
            ( np)
            ( Y)
            ( two-elements-transposition eX Y)
            ( refl)
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( i))
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (two-elements-transposition eX Y))
              ( j))
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (pr2 (two-elements-transposition eX Y)))
              ( i))
            ( has-decidable-equality-count
              ( eX)
              ( pr1 (pr2 (two-elements-transposition eX Y)))
              ( j)))
          ( eq-is-prop
            ( is-prop-type-Decidable-Prop
              ( pr1 Y
                ( pr1 (orientation-two-elements-count j i (np  inv) Y))))))

  equiv-fin-1-difference-orientation-two-elements-count :
    ( i j : X) (np : ¬ (Id i j)) 
    Fin 1 
    Σ (2-Element-Decidable-Subtype l X)
    ( λ Y  type-Decidable-Prop
      ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( orientation-two-elements-count i j np)
        ( orientation-two-elements-count j i (np  inv))
        ( Y)))
  pr1 (pr1 (equiv-fin-1-difference-orientation-two-elements-count i j np) x) =
    standard-2-Element-Decidable-Subtype (has-decidable-equality-count eX) np
  pr2 (pr1 (equiv-fin-1-difference-orientation-two-elements-count i j np) x) q =
    np
      ( ( inv
        ( eq-orientation-two-elements-count j i (np  inv))) 
        ( ( ap
          ( λ Y  pr1 (orientation-two-elements-count j i (np  inv) Y))
          { x =
            standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np  inv)}
          { y =
            standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)}
          ( inv
            ( is-commutative-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))) 
          ( inv (ap pr1 q) 
            eq-orientation-two-elements-count i j np)))
  pr2 (equiv-fin-1-difference-orientation-two-elements-count i j np) =
    is-equiv-has-inverse
      ( λ x  inr star)
      ( λ T 
        eq-pair-Σ
          ( retr-fin-1-difference-orientation-two-elements-count
            ( T)
            ( two-elements-transposition eX (pr1 T))
            ( refl)
            ( has-decidable-equality-count
              (eX) (pr1 (two-elements-transposition eX (pr1 T))) (i))
            ( has-decidable-equality-count
              (eX) (pr1 (two-elements-transposition eX (pr1 T))) (j))
            ( has-decidable-equality-count
              (eX) (pr1 (pr2 (two-elements-transposition eX (pr1 T)))) (i))
            ( has-decidable-equality-count
              (eX) (pr1 (pr2 (two-elements-transposition eX (pr1 T)))) (j)))
          ( eq-is-prop
            ( is-prop-type-Decidable-Prop
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( orientation-two-elements-count i j np)
                ( orientation-two-elements-count j i (np  inv))
                ( pr1 T)))))
       ( sec-fin-1-difference-orientation-two-elements-count)
    where
    retr-fin-1-difference-orientation-two-elements-count :
      ( T :
        Σ (2-Element-Decidable-Subtype l X)
           Y 
            type-Decidable-Prop
              ( 2-Element-Decidable-Subtype-subtype-pointwise-difference
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( orientation-two-elements-count i j np)
                ( orientation-two-elements-count j i (np  inv))
                ( Y)))) 
      ( two-elements : Σ X
        ( λ x  Σ X
          ( λ y  Σ (¬ (Id x y))
            ( λ np' 
              Id
                ( standard-2-Element-Decidable-Subtype
                  ( has-decidable-equality-count eX)
                  ( np'))
                ( pr1 T))))) 
      Id two-elements (two-elements-transposition eX (pr1 T)) 
      is-decidable (Id (pr1 two-elements) i) 
      is-decidable (Id (pr1 two-elements) j) 
      is-decidable (Id (pr1 (pr2 two-elements)) i) 
      is-decidable (Id (pr1 (pr2 two-elements)) j) 
      Id
        ( standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np))
        ( pr1 T)
    retr-fin-1-difference-orientation-two-elements-count
      T (pair x (pair y (pair np' P))) Q (inl q) r s (inl t) =
        ap
        ( λ w 
          standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            {x = pr1 w}
            {y = j}
            ( pr2 w))
        { x = pair i np}
        { y = pair x  p  np (inv q  p))}
        ( eq-pair-Σ
          ( inv q)
          ( eq-is-prop is-prop-neg)) 
        ( ( ap
          ( λ w 
            standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              {x = x}
              {y = pr1 w}
              ( pr2 w))
          { x = pair j  p  np (inv q  p))}
          { y = pair y np'}
          ( eq-pair-Σ
            ( inv t)
            ( eq-is-prop is-prop-neg))) 
          ( P))
    retr-fin-1-difference-orientation-two-elements-count
      T (pair x (pair y (pair np' P))) Q (inl q) r s (inr nt) =
       ex-falso
        ( pr2 T
          ( eq-pair-Σ
            ( ( inward-edge-left-two-elements-orientation-count i j np
              ( pr1 T)
              ( y)
              ( tr
                ( λ Y  type-Decidable-Prop (pr1 Y y))
                ( P)
                ( inr refl))
              ( tr
                ( λ z  type-Decidable-Prop (pr1 (pr1 T) z))
                ( q)
                ( tr
                  ( λ Y  type-Decidable-Prop (pr1 Y x))
                  ( P)
                  ( inl refl)))
              ( λ s  np' (q  inv s))
              ( nt)) 
              ( inv
                ( inward-edge-right-two-elements-orientation-count j i
                  ( np  inv)
                  ( pr1 T)
                  ( y)
                  ( tr
                    ( λ Y  type-Decidable-Prop (pr1 Y y))
                    ( P)
                    ( inr refl))
                  ( tr
                    ( λ z  type-Decidable-Prop (pr1 (pr1 T) z))
                    ( q)
                    ( tr
                      ( λ Y  type-Decidable-Prop (pr1 Y x))
                      ( P)
                      ( inl refl)))
                  ( nt)
                  ( λ s  np' (q  inv s)))))
            ( eq-is-prop
              ( is-prop-type-Decidable-Prop
                ( pr1
                  ( pr1 T)
                  ( pr1
                    ( orientation-two-elements-count
                        j i (np  inv) (pr1 T))))))))
    retr-fin-1-difference-orientation-two-elements-count
      T (pair x (pair y (pair np' P))) Q (inr nq) (inl r) (inl s) t =
       ap
        ( λ w 
          standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            {x = pr1 w}
            {y = j}
            ( pr2 w))
        { x = pair i np}
        { y = pair y  p  np (inv s  p))}
        ( eq-pair-Σ
          ( inv s)
          ( eq-is-prop is-prop-neg)) 
        ( ( ap
          ( λ w 
            standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              {x = y}
              {y = pr1 w}
              ( pr2 w))
          { x = pair j  p  np (inv s  p))}
          { y = pair x  p  np' (inv p))}
          ( eq-pair-Σ
            ( inv r)
            ( eq-is-prop is-prop-neg))) 
          ( inv
            ( is-commutative-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np')) 
            ( P)))
    retr-fin-1-difference-orientation-two-elements-count
      T (pair x (pair y (pair np' P))) Q (inr nq) (inl r) (inr ns) t =
       ex-falso
        ( pr2 T
          ( eq-pair-Σ
            ( inward-edge-right-two-elements-orientation-count i j np
              ( pr1 T)
              ( y)
              ( tr
                ( λ Y  type-Decidable-Prop (pr1 Y y))
                ( P)
                ( inr refl))
              ( tr
                ( λ z  type-Decidable-Prop (pr1 (pr1 T) z))
                ( r)
                ( tr
                  ( λ Y  type-Decidable-Prop (pr1 Y x))
                  ( P)
                  ( inl refl)))
              ( ns)
              ( λ t  np' (r  inv t)) 
              ( inv
                ( inward-edge-left-two-elements-orientation-count j i
                  ( np  inv)
                  ( pr1 T)
                  ( y)
                  ( tr
                    ( λ Y  type-Decidable-Prop (pr1 Y y))
                    ( P)
                    ( inr refl))
                  ( tr
                    ( λ z  type-Decidable-Prop (pr1 (pr1 T) z))
                    ( r)
                    ( tr
                      ( λ Y  type-Decidable-Prop (pr1 Y x))
                      ( P)
                      ( inl refl)))
                  ( λ t  np' (r  inv t))
                  ( ns))))
            ( eq-is-prop
              ( is-prop-type-Decidable-Prop
                ( pr1
                  ( pr1 T)
                  ( pr1
                    ( orientation-two-elements-count
                        j i (np  inv) (pr1 T))))))))
    retr-fin-1-difference-orientation-two-elements-count
      T (pair x (pair y (pair np' P))) Q (inr nq) (inr nr) s t =
      ex-falso
        ( pr2 T
          ( ap
            ( λ w 
              cases-orientation-two-elements-count i j
                ( pr1 T)
                ( w)
                ( has-decidable-equality-count eX
                  ( pr1 w) i)
                ( has-decidable-equality-count eX
                  (pr1 w) j)
                ( has-decidable-equality-count eX
                  (pr1 (pr2 w)) i))
            ( inv Q) 
            ( ( ap
              ( λ D 
                cases-orientation-two-elements-count i j
                  ( pr1 T)
                  ( pair x (pair y (pair np' P)))
                  ( pr1 D)
                  ( pr2 D)
                  ( has-decidable-equality-count eX y i))
              { y = pair (inr nq) (inr nr)}
              ( eq-pair-Σ
                ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))
                ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j))))) 
              ( ap
                ( λ D 
                  cases-orientation-two-elements-count j i
                    ( pr1 T)
                    (pair x (pair y (pair np' P)))
                    ( pr1 D)
                    ( pr2 D)
                    ( has-decidable-equality-count eX y j))
                { x = pair (inr nr) (inr nq)}
                { y =
                  pair
                    ( has-decidable-equality-count eX x j)
                    ( has-decidable-equality-count eX x i)}
                ( eq-pair-Σ
                  ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))
                  ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))) 
                ( ap
                  ( λ w 
                    cases-orientation-two-elements-count j i
                      ( pr1 T)
                      ( w)
                      ( has-decidable-equality-count eX (pr1 w) j)
                      ( has-decidable-equality-count eX (pr1 w) i)
                      ( has-decidable-equality-count eX (pr1 (pr2 w)) j))
                  ( Q))))))
    sec-fin-1-difference-orientation-two-elements-count :
      ( ( λ x  inr {A = empty} star) 
        pr1 (equiv-fin-1-difference-orientation-two-elements-count i j np)) ~
      ( id)
    sec-fin-1-difference-orientation-two-elements-count (inr star) = refl

  eq-orientation-pointwise-difference-two-elements-count :
    ( i j : X) (np : ¬ (Id i j)) 
    Id
      1
      ( number-of-elements-is-finite
        ( is-finite-subtype-pointwise-difference
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( orientation-two-elements-count i j np)
          ( orientation-two-elements-count j i (np  inv))))
  eq-orientation-pointwise-difference-two-elements-count i j np =
     ap
      ( number-of-elements-has-finite-cardinality)
      ( all-elements-equal-has-finite-cardinality
        ( pair
          ( 1)
          ( unit-trunc-Prop
            ( equiv-fin-1-difference-orientation-two-elements-count i j np)))
        ( has-finite-cardinality-is-finite
          ( is-finite-subtype-pointwise-difference
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( orientation-two-elements-count i j np)
            ( orientation-two-elements-count j i (np  inv)))))

  cases-not-even-difference-orientation-aut-transposition-count :
    ( i j : X) (np : ¬ (Id i j)) 
    ( Id
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( orientation-two-elements-count i j np)) +
    ( Id
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( orientation-two-elements-count j i (np  inv))) 
    ¬ ( sim-Eq-Rel
      ( even-difference-orientation-Complete-Undirected-Graph
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX))))
      ( orientation-aut-count
        ( transposition
          ( standard-2-Element-Decidable-Subtype
            ( has-decidable-equality-count eX)
            ( np))))
      ( map-orientation-complete-undirected-graph-equiv
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( transposition (standard-2-Element-Decidable-Subtype
          ( has-decidable-equality-count eX)
          ( np)))
        ( orientation-aut-count
          ( transposition
            ( standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))))))
  cases-not-even-difference-orientation-aut-transposition-count
    i j np (inl pl) =
    tr
      ( λ d 
        ¬ ( sim-Eq-Rel
          ( even-difference-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX))))
          ( d)
          ( map-orientation-complete-undirected-graph-equiv
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( transposition (standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
            ( d))))
      ( inv pl)
      ( tr
        ( λ d 
          ¬ ( sim-Eq-Rel
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( orientation-two-elements-count i j np)
            ( d)))
        ( inv
          ( eq-map-orientation-transposition-orientation-two-elements-count
              i j np))
        ( λ p 
          neq-inl-inr
            ( p 
              ( inv
                ( ap mod-two-ℕ
                  ( eq-orientation-pointwise-difference-two-elements-count
                      i j np))))))
  cases-not-even-difference-orientation-aut-transposition-count
    i j np (inr pr) =
    tr
      ( λ d 
        ¬ ( sim-Eq-Rel
          ( even-difference-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX))))
          ( d)
          ( map-orientation-complete-undirected-graph-equiv
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( transposition (standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np)))
            ( d))))
      ( inv pr)
      ( tr
        ( λ d 
          ¬ ( sim-Eq-Rel
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( orientation-two-elements-count j i (np  inv))
            ( d)))
        ( inv
          ( ( ap
            ( λ w 
              map-orientation-complete-undirected-graph-equiv
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( pair X (unit-trunc-Prop (equiv-count eX)))
                ( transposition w)
                ( orientation-two-elements-count j i (np  inv)))
            ( is-commutative-standard-2-Element-Decidable-Subtype
              ( has-decidable-equality-count eX)
              ( np))) 
            ( eq-map-orientation-transposition-orientation-two-elements-count
                j i (np  inv))))
        ( λ p 
          neq-inl-inr
            ( p 
              ( inv
                ( ap
                  ( mod-two-ℕ)
                  ( eq-orientation-pointwise-difference-two-elements-count j i
                    ( np  inv)))))))

  not-even-difference-orientation-aut-transposition-count :
    (Y : 2-Element-Decidable-Subtype l X) 
    ¬ ( sim-Eq-Rel
      ( even-difference-orientation-Complete-Undirected-Graph
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX))))
      ( orientation-aut-count (transposition Y))
      ( map-orientation-complete-undirected-graph-equiv
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( pair X (unit-trunc-Prop (equiv-count eX)))
        ( transposition Y)
        ( orientation-aut-count (transposition Y))))
  not-even-difference-orientation-aut-transposition-count Y =
    tr
      ( λ Y' 
        ¬ ( sim-Eq-Rel
          ( even-difference-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX))))
          ( orientation-aut-count (transposition Y'))
          ( map-orientation-complete-undirected-graph-equiv
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( transposition Y')
            ( orientation-aut-count (transposition Y')))))
      ( pr2 (pr2 (pr2 (two-elements-transposition eX Y))))
      ( cases-not-even-difference-orientation-aut-transposition-count
        ( pr1 (two-elements-transposition eX Y))
        ( pr1 (pr2 (two-elements-transposition eX Y)))
        ( pr1 (pr2 (pr2 (two-elements-transposition eX Y))))
        ( eq-orientation-aut-orientation-two-elements-count
          ( pr1 (two-elements-transposition eX Y))
          ( pr1 (pr2 (two-elements-transposition eX Y)))
          ( pr1 (pr2 (pr2 (two-elements-transposition eX Y))))))

  inv-orientation :
    (T :
      quotient-sign
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX)))) 
    is-decidable
      ( is-in-equivalence-class
        ( even-difference-orientation-Complete-Undirected-Graph
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX))))
        ( T)
        ( canonical-orientation-count)) 
    Fin 2
  inv-orientation T (inl P) = inl (inr star)
  inv-orientation T (inr NP) = inr star

  equiv-fin-2-quotient-sign-count :
    Fin 2 
    ( quotient-sign
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX))))
  pr1 equiv-fin-2-quotient-sign-count (inl (inr star)) =
    class
      ( even-difference-orientation-Complete-Undirected-Graph
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX))))
      ( canonical-orientation-count)
  pr1 equiv-fin-2-quotient-sign-count (inr star) =
    class
      ( even-difference-orientation-Complete-Undirected-Graph
        ( number-of-elements-count eX)
        ( pair X (unit-trunc-Prop (equiv-count eX))))
      ( trans-canonical-orientation-count)
  pr2 equiv-fin-2-quotient-sign-count =
    is-equiv-has-inverse
      ( λ T 
        inv-orientation
          ( T)
          ( is-decidable-is-in-equivalence-class-is-decidable
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( is-decidable-even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( T)
            ( canonical-orientation-count)))
      ( λ T 
        retr-orientation
          ( T)
          ( is-decidable-is-in-equivalence-class-is-decidable
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( is-decidable-even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( T)
            ( canonical-orientation-count)))
      ( λ k 
        sec-orientation
          k
          ( is-decidable-is-in-equivalence-class-is-decidable
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( is-decidable-even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( pr1 equiv-fin-2-quotient-sign-count k)
            ( canonical-orientation-count)))
    where
    cases-retr-orientation :
      (T :
        equivalence-class
          ( even-difference-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX))))) 
      ¬ ( is-in-equivalence-class
        ( even-difference-orientation-Complete-Undirected-Graph
          (number-of-elements-count eX)
          (pair X (unit-trunc-Prop (equiv-count eX))))
        ( T)
        ( canonical-orientation-count)) 
      ( t :
        orientation-Complete-Undirected-Graph
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))) 
      Id
        ( class
          ( even-difference-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX))))
          ( t))
        ( T) 
      ( k : Fin 2) 
      Id
        ( k)
        ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))
          ( t)
          ( canonical-orientation-count)) 
      is-in-equivalence-class
        ( even-difference-orientation-Complete-Undirected-Graph
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX))))
        ( T)
        ( trans-canonical-orientation-count)
    cases-retr-orientation T NH t q (inl (inr star)) r =
      ex-falso
        ( NH
          ( tr
            ( λ x 
              is-in-equivalence-class
                ( even-difference-orientation-Complete-Undirected-Graph
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX))))
                ( x)
                ( canonical-orientation-count))
            ( q)
            ( r)))
    cases-retr-orientation T NH t q (inr star) r =
      tr
         x 
          is-in-equivalence-class
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( x)
            ( trans-canonical-orientation-count))
        ( q)
        ( eq-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX)))
            ( t)
            ( canonical-orientation-count)
            ( trans-canonical-orientation-count)
            ( inr star)
            ( r)
            ( is-symmetric-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX)))
              ( trans-canonical-orientation-count)
              ( canonical-orientation-count)
              ( inr star)
              ( is-symmetric-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( canonical-orientation-count)
                  ( trans-canonical-orientation-count)
                  ( inr star)
                  (ap
                    ( mod-two-ℕ)
                    { x = 1}
                    { y =
                      number-of-elements-is-finite
                        ( is-finite-subtype-pointwise-difference
                          ( number-of-elements-count eX)
                          ( pair X (unit-trunc-Prop (equiv-count eX)))
                          ( canonical-orientation-count)
                          ( trans-canonical-orientation-count))}
                    ( eq-orientation-pointwise-difference-two-elements-count
                      ( first-element-count)
                      ( second-element-count)
                      ( distinct-two-elements-count))))))
    retr-orientation :
      (T :
        quotient-sign
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX)))) 
      (H :
        is-decidable
          (is-in-equivalence-class
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))
            ( T)
            ( canonical-orientation-count))) 
      Id (pr1 equiv-fin-2-quotient-sign-count (inv-orientation T H)) T
    retr-orientation T (inl H) =
      eq-effective-quotient'
        ( even-difference-orientation-Complete-Undirected-Graph
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX))))
        ( canonical-orientation-count)
        ( T)
        ( H)
    retr-orientation T (inr NH) =
      eq-effective-quotient'
        ( even-difference-orientation-Complete-Undirected-Graph
          ( number-of-elements-count eX)
          ( pair X (unit-trunc-Prop (equiv-count eX))))
        ( trans-canonical-orientation-count)
        ( T)
        ( apply-universal-property-trunc-Prop
          ( pr2 T)
          ( pair
            ( is-in-equivalence-class
              ( even-difference-orientation-Complete-Undirected-Graph
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX))))
              ( T)
              ( trans-canonical-orientation-count))
            ( is-prop-is-in-equivalence-class
              ( even-difference-orientation-Complete-Undirected-Graph
                ( number-of-elements-count eX)
                ( pair X (unit-trunc-Prop (equiv-count eX))))
              ( T)
              ( trans-canonical-orientation-count)))
          ( λ (pair t r) 
            cases-retr-orientation
              ( T)
              ( NH)
              ( t)
              ( eq-pair-Σ
                ( ap
                  ( pr1)
                  ( inv
                    ( eq-has-same-elements-equivalence-class
                      ( even-difference-orientation-Complete-Undirected-Graph
                        ( number-of-elements-count eX)
                        ( pair X (unit-trunc-Prop (equiv-count eX))))
                      ( T)
                      ( class
                        ( even-difference-orientation-Complete-Undirected-Graph
                          ( number-of-elements-count eX)
                          ( pair X (unit-trunc-Prop (equiv-count eX))))
                        ( t))
                      ( r))))
                ( all-elements-equal-type-trunc-Prop _ (pr2 T)))
              ( mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( t)
                  ( canonical-orientation-count))
              ( refl)))
    sec-orientation :
      (k : Fin 2)
      ( D : is-decidable
        ( is-in-equivalence-class
          ( even-difference-orientation-Complete-Undirected-Graph
            ( number-of-elements-count eX)
            ( pair X (unit-trunc-Prop (equiv-count eX))))
          ( pr1 equiv-fin-2-quotient-sign-count k)
          ( canonical-orientation-count))) 
      Id
        ( inv-orientation
          ( pr1 equiv-fin-2-quotient-sign-count k)
          ( D))
        ( k)
    sec-orientation (inl (inr star)) (inl Q) = refl
    sec-orientation (inl (inr star)) (inr NQ) =
      ex-falso
        ( NQ
          ( refl-Eq-Rel
            ( even-difference-orientation-Complete-Undirected-Graph
              ( number-of-elements-count eX)
              ( pair X (unit-trunc-Prop (equiv-count eX))))))
    sec-orientation (inr star) (inl Q) =
      ex-falso
        ( neq-inl-inr
          ( Q 
            inv
              ( is-symmetric-mod-two-number-of-differences-orientation-Complete-Undirected-Graph
                  ( number-of-elements-count eX)
                  ( pair X (unit-trunc-Prop (equiv-count eX)))
                  ( canonical-orientation-count)
                  ( trans-canonical-orientation-count)
                  ( inr star)
                  ( ap mod-two-ℕ
                    ( eq-orientation-pointwise-difference-two-elements-count
                      ( first-element-count)
                      ( second-element-count)
                      ( distinct-two-elements-count))))))
    sec-orientation (inr star) (inr NQ) = refl

module _
  {l : Level} (n : ) (X : UU-Fin l n) (ineq : leq-ℕ 2 n)
  where

  equiv-fin-2-quotient-sign-equiv-Fin :
    (h : Fin n  type-UU-Fin n X)  Fin 2  quotient-sign n X
  equiv-fin-2-quotient-sign-equiv-Fin h =
    tr
      ( λ e  Fin 2  quotient-sign n (pair (type-UU-Fin n X) e))
      ( all-elements-equal-type-trunc-Prop
        ( unit-trunc-Prop (equiv-count (pair n h)))
        ( pr2 X))
      ( equiv-fin-2-quotient-sign-count (pair n h) ineq)