Orientations of the complete undirected graph

Content created by Egbert Rijke, Eléonore Mangel, Fredrik Bakke, Jonathan Prieto-Cubides, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-04-04.
Last modified on 2024-02-27.

{-# 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.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
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.function-types
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.negated-equality
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.transport-along-identifications
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) =
    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)) 
        d1 Y  d3 Y  (is-decidable (d1 Y  d2 Y)) 
        is-decidable (d2 Y  d3 Y) 
        ((d1 Y  d2 Y) × ¬ (d2 Y  d3 Y)) +
        ((d2 Y  d3 Y) × ¬ (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  d' Y  d Y))))
        ( λ h  unit-trunc-Prop (h' ∘e h))
      where
      h' :
        Σ ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
          ( λ Y  d Y  d' Y) 
        Σ ( 2-Element-Decidable-Subtype l (type-UU-Fin n X))
          ( λ Y  d' Y  d Y)
      pr1 h' (pair Y np) = pair Y  p'  np (inv p'))
      pr2 h' =
        is-equiv-is-invertible
          ( λ (pair Y np)  pair Y  p'  np (inv p')))
          ( λ (pair Y np)  eq-pair-eq-fiber (eq-is-prop is-prop-neg))
          ( λ (pair Y np)  eq-pair-eq-fiber (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'))
        ( transitive-cong-ℕ
          ( 2)
          ( k1 +ℕ k2)
          ( zero-ℕ)
          ( 2 *ℕ k')
          ( scalar-invariant-cong-ℕ' 2 0 2 k' (cong-zero-ℕ' 2))
          ( transitive-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-ℕ)
            ( 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)))
            ( symmetric-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))))) 
      ( 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 _ _ _
                    ( unit-trunc-Prop
                      ( inv-equiv
                        ( equiv-symmetric-difference-subtype-pointwise-difference
                            d1 d2 d3)))
                    ( 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)))))))))))
    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 :
    equivalence-relation 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  (_ , 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) p2 p1
  abstract
    is-decidable-even-difference-orientation-Complete-Undirected-Graph :
      (Y Y' : orientation-Complete-Undirected-Graph) 
      is-decidable
        ( sim-equivalence-relation
            ( 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-is-invertible
      ( 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-eq-fiber (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-equivalence-relation
        ( even-difference-orientation-Complete-Undirected-Graph n X)
        ( d)
        ( d') 
        sim-equivalence-relation
          ( 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-is-invertible
          ( λ (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-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-equivalence-relation
            ( 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 
          Σ (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 
          Σ (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)  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 :
      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-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)

  transitive-canonical-orientation-count :
    orientation-Complete-Undirected-Graph
      ( number-of-elements-count eX)
      ( pair X (unit-trunc-Prop (equiv-count eX)))
  transitive-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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y i)) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y i)) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y j)) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      x  i  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 : i  j)
      (Y : 2-Element-Decidable-Subtype l X) (x : X) 
      ( type-Decidable-Prop (pr1 Y x)) 
      ( type-Decidable-Prop (pr1 Y j)) 
      x  i  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 : i  j)
      ( two-elements : Σ X
        ( λ x  Σ X
          ( λ y  Σ (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 : 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 : 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  Σ (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 : 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  Σ (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))