Deloopings of the sign homomorphism
{-# OPTIONS --lossy-unification #-}
module finite-group-theory.delooping-sign-homomorphism where
Imports
open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.natural-numbers open import finite-group-theory.finite-type-groups open import finite-group-theory.permutations open import finite-group-theory.sign-homomorphism open import finite-group-theory.transpositions open import foundation.commuting-squares-of-maps open import foundation.contractible-types open import foundation.coproduct-types open import foundation.decidable-propositions open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.embeddings 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-propositional-truncation open import foundation.functoriality-set-quotients open import foundation.identity-types open import foundation.injective-maps 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.raising-universe-levels open import foundation.reflecting-maps-equivalence-relations open import foundation.sets open import foundation.truncated-types open import foundation.uniqueness-set-quotients open import foundation.unit-type open import foundation.univalence open import foundation.univalence-action-on-equivalences open import foundation.universal-property-set-quotients open import foundation.universe-levels open import group-theory.concrete-groups open import group-theory.groups open import group-theory.homomorphisms-concrete-groups open import group-theory.homomorphisms-generated-subgroups open import group-theory.homomorphisms-groups open import group-theory.homomorphisms-semigroups open import group-theory.isomorphisms-groups open import group-theory.loop-groups-sets open import group-theory.subgroups-generated-by-subsets-groups open import group-theory.symmetric-groups open import synthetic-homotopy-theory.loop-spaces open import univalent-combinatorics.2-element-decidable-subtypes open import univalent-combinatorics.equality-finite-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.set-quotients-of-index-two open import univalent-combinatorics.standard-finite-types
Ideas
The delooping of a group homomorphism f : G → H is a pointed map
Bf : BG → BH equiped with an homotopy witnessing that the following square
commutes :
f
G --------> H
| |
≅| |≅
| |
v v
BG ------> BH
ΩBf
In this file, we study the delooping of the sign homomorphism, and, more
precisely, how to detect that a pointed map between BSn and BS2 is a
delooping of the sign homomorphism.
Definition
Construction of the delooping of the sign homomorphism with quotients (Corollary 25)
module _ { l1 l2 l3 : Level} ( D : (n : ℕ) (X : UU-Fin l1 n) → UU l2) ( R : (n : ℕ) (X : UU-Fin l1 n) → Eq-Rel l3 (D n X)) ( is-decidable-R : (n : ℕ) → leq-ℕ 2 n → (X : UU-Fin l1 n) (a b : D n X) → is-decidable (sim-Eq-Rel (R n X) a b)) ( equiv-D/R-fin-2-equiv : (n : ℕ) (X : UU-Fin l1 n) → leq-ℕ 2 n → Fin n ≃ type-UU-Fin n X → Fin 2 ≃ equivalence-class (R n X)) ( quotient-aut-succ-succ-Fin : (n : ℕ) → ( raise-Fin l1 (n +ℕ 2) ≃ raise-Fin l1 (n +ℕ 2)) → D ( n +ℕ 2) ( raise-Fin l1 (n +ℕ 2), unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))) ( not-R-transposition-fin-succ-succ : (n : ℕ) → ( Y : 2-Element-Decidable-Subtype l1 (raise-Fin l1 (n +ℕ 2))) → ¬ ( sim-Eq-Rel ( R ( n +ℕ 2) ( raise-Fin l1 (n +ℕ 2) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))) ( quotient-aut-succ-succ-Fin n (transposition Y)) ( map-equiv ( univalent-action-equiv ( mere-equiv-Prop (Fin (n +ℕ 2))) ( D (n +ℕ 2)) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( transposition Y)) ( quotient-aut-succ-succ-Fin n (transposition Y))))) where private l4 : Level l4 = l2 ⊔ lsuc l3 eq-counting-equivalence-class-R : (n : ℕ) → Id ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( raise (l2 ⊔ lsuc l3) (Fin 2)) eq-counting-equivalence-class-R n = eq-equiv ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( raise l4 (Fin 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv ( equiv-D/R-fin-2-equiv ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2)) ( star) ( compute-raise-Fin l1 (n +ℕ 2)))) invertible-action-D-equiv : (n : ℕ) (X X' : UU-Fin l1 n) → type-UU-Fin n X ≃ type-UU-Fin n X' → D n X ≃ D n X' invertible-action-D-equiv n = univalent-action-equiv (mere-equiv-Prop (Fin n)) (D n) preserves-id-equiv-invertible-action-D-equiv : (n : ℕ) (X : UU-Fin l1 n) → Id (invertible-action-D-equiv n X X id-equiv) id-equiv preserves-id-equiv-invertible-action-D-equiv n = preserves-id-equiv-univalent-action-equiv (mere-equiv-Prop (Fin n)) (D n) preserves-R-invertible-action-D-equiv : ( n : ℕ) → ( X X' : UU-Fin l1 n) ( e : type-UU-Fin n X ≃ type-UU-Fin n X') → ( a a' : D n X) → ( sim-Eq-Rel (R n X) a a' ↔ sim-Eq-Rel ( R n X') ( map-equiv (invertible-action-D-equiv n X X' e) a) ( map-equiv (invertible-action-D-equiv n X X' e) a')) preserves-R-invertible-action-D-equiv n X X' = Ind-univalent-action-equiv (mere-equiv-Prop (Fin n)) (D n) X ( λ Y f → ( a a' : D n X) → ( sim-Eq-Rel (R n X) a a' ↔ sim-Eq-Rel (R n Y) (map-equiv f a) (map-equiv f a'))) ( λ a a' → id , id) ( X') raise-UU-Fin-Fin : (n : ℕ) → UU-Fin l1 n pr1 (raise-UU-Fin-Fin n) = raise l1 (Fin n) pr2 (raise-UU-Fin-Fin n) = unit-trunc-Prop (compute-raise-Fin l1 n) that-thing : (n : ℕ) → Fin 2 ≃ equivalence-class (R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) that-thing n = equiv-D/R-fin-2-equiv ( n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( star) ( compute-raise-Fin l1 (n +ℕ 2)) quotient-loop-Fin : (n : ℕ) → type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) → ( D (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)) ≃ D (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) quotient-loop-Fin n p = invertible-action-D-equiv ( n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)) map-quotient-loop-Fin : (n : ℕ) → type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) → D (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)) → D (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)) map-quotient-loop-Fin n p = map-equiv (quotient-loop-Fin n p) quotient-set-Fin : (n : ℕ) → Set l4 quotient-set-Fin n = equivalence-class-Set (R n (raise-UU-Fin-Fin n)) quotient-map-quotient-Fin : (n : ℕ) → D n (raise-UU-Fin-Fin n) → type-Set (quotient-set-Fin n) quotient-map-quotient-Fin n = class (R n (raise-UU-Fin-Fin n)) quotient-reflecting-map-quotient-Fin : (n : ℕ) → reflecting-map-Eq-Rel ( R n (raise-UU-Fin-Fin n)) ( type-Set (quotient-set-Fin n)) quotient-reflecting-map-quotient-Fin n = quotient-reflecting-map-equivalence-class (R n (raise-UU-Fin-Fin n)) mere-equiv-D/R-fin-2 : (n : ℕ) (X : UU-Fin l1 n) → leq-ℕ 2 n → mere-equiv (Fin 2) (equivalence-class (R n X)) mere-equiv-D/R-fin-2 n X ineq = map-trunc-Prop ( equiv-D/R-fin-2-equiv n X ineq) ( has-cardinality-type-UU-Fin n X) map-quotient-delooping-sign : (n : ℕ) → classifying-type-Concrete-Group (UU-Fin-Group l1 n) → classifying-type-Concrete-Group (UU-Fin-Group l4 2) map-quotient-delooping-sign 0 X = Fin-UU-Fin l4 2 map-quotient-delooping-sign 1 X = Fin-UU-Fin l4 2 pr1 (map-quotient-delooping-sign (succ-ℕ (succ-ℕ n)) X) = equivalence-class (R (succ-ℕ (succ-ℕ n)) X) pr2 (map-quotient-delooping-sign (succ-ℕ (succ-ℕ n)) X) = mere-equiv-D/R-fin-2 (succ-ℕ (succ-ℕ n)) X star quotient-delooping-sign : (n : ℕ) → hom-Concrete-Group (UU-Fin-Group l1 n) (UU-Fin-Group l4 2) pr1 (quotient-delooping-sign n) = map-quotient-delooping-sign n pr2 (quotient-delooping-sign 0) = refl pr2 (quotient-delooping-sign 1) = refl pr2 (quotient-delooping-sign (succ-ℕ (succ-ℕ n))) = eq-pair-Σ ( eq-counting-equivalence-class-R n) ( eq-is-prop is-prop-type-trunc-Prop) map-quotient-delooping-sign-loop : ( n : ℕ) ( X Y : UU l1) → ( eX : mere-equiv (Fin (n +ℕ 2)) X) → ( eY : mere-equiv (Fin (n +ℕ 2)) Y) → Id X Y → Id ( equivalence-class (R (n +ℕ 2) (X , eX))) ( equivalence-class (R (n +ℕ 2) (Y , eY))) map-quotient-delooping-sign-loop n X Y eX eY p = ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)) private map-quotient-delooping-sign-loop-Fin : ( n : ℕ) → type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) → type-Group (loop-group-Set (quotient-set-Fin (n +ℕ 2))) map-quotient-delooping-sign-loop-Fin n = map-quotient-delooping-sign-loop n ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) quotient-delooping-sign-loop : ( n : ℕ) → type-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) pr1 (quotient-delooping-sign-loop n) = map-quotient-delooping-sign-loop-Fin n pr2 (quotient-delooping-sign-loop n) p q = ( ap ( ap (equivalence-class ∘ R (n +ℕ 2))) ( ap ( eq-pair-Σ (p ∙ q)) ( eq-is-prop ( is-trunc-Id ( is-prop-type-trunc-Prop _ ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))))) ∙ ( inv ( compute-eq-pair-Σ ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( p) ( q) ( eq-is-prop is-prop-type-trunc-Prop) ( eq-is-prop is-prop-type-trunc-Prop))))) ∙ ( ap-concat ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)) ( eq-pair-Σ q (eq-is-prop is-prop-type-trunc-Prop))) abstract coherence-square-map-quotient-delooping-sign-loop-Set : ( n : ℕ) ( X Y : UU l1) ( eX : mere-equiv (Fin (n +ℕ 2)) X) ( eY : mere-equiv (Fin (n +ℕ 2)) Y) ( p : Id X Y) → ( Id (tr (mere-equiv (Fin (n +ℕ 2))) p eX) eY) → ( sX : is-set X) ( sY : is-set Y) → coherence-square-maps ( map-equiv ( invertible-action-D-equiv ( n +ℕ 2) ( Y , eY) ( X , eX) ( map-hom-symmetric-group-loop-group-Set (X , sX) (Y , sY) (p)))) ( class (R (n +ℕ 2) (Y , eY))) ( class (R (n +ℕ 2) (X , eX))) ( map-equiv ( map-hom-symmetric-group-loop-group-Set ( equivalence-class-Set (R (n +ℕ 2) (X , eX))) ( equivalence-class-Set (R (n +ℕ 2) (Y , eY))) ( map-quotient-delooping-sign-loop n X Y eX eY p))) coherence-square-map-quotient-delooping-sign-loop-Set n X .X eX .eX refl refl sX sY x = ( ap ( λ w → map-equiv ( map-hom-symmetric-group-loop-group-Set ( equivalence-class-Set (R (n +ℕ 2) (X , eX))) ( equivalence-class-Set (R (n +ℕ 2) (X , eX))) ( w)) ( class (R (n +ℕ 2) (X , eX)) (x))) ( ap ( λ w → ap (equivalence-class ∘ R (n +ℕ 2)) (eq-pair-Σ refl w)) { x = eq-is-prop is-prop-type-trunc-Prop} ( eq-is-prop ( is-trunc-Id ( is-prop-type-trunc-Prop ( tr (mere-equiv (Fin (n +ℕ 2))) refl eX) ( eX)))))) ∙ ( ap ( class (R (n +ℕ 2) (X , tr (mere-equiv (Fin (n +ℕ 2))) refl eX))) ( inv ( htpy-eq-equiv ( preserves-id-equiv-invertible-action-D-equiv (n +ℕ 2) (X , eX)) ( x)))) coherence-square-map-quotient-delooping-sign-loop-Fin : (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → coherence-square-maps ( map-quotient-loop-Fin n p) ( quotient-map-quotient-Fin (n +ℕ 2)) ( quotient-map-quotient-Fin (n +ℕ 2)) ( map-equiv ( map-hom-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)) ( quotient-set-Fin (n +ℕ 2)) ( map-quotient-delooping-sign-loop-Fin n p))) coherence-square-map-quotient-delooping-sign-loop-Fin n p = coherence-square-map-quotient-delooping-sign-loop-Set n ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( p) ( eq-is-prop is-prop-type-trunc-Prop) ( is-set-type-Set (raise-Fin-Set l1 (n +ℕ 2))) ( is-set-type-Set (raise-Fin-Set l1 (n +ℕ 2))) private is-contr-equiv-quotient : ( n : ℕ) → ( p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → is-contr ( Σ ( type-Group (symmetric-Group (quotient-set-Fin (n +ℕ 2)))) ( λ h' → coherence-square-maps ( map-quotient-loop-Fin n p) ( quotient-map-quotient-Fin (n +ℕ 2)) ( map-reflecting-map-Eq-Rel ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2))) ( map-equiv h'))) is-contr-equiv-quotient n p = unique-equiv-is-set-quotient ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-set-Fin (n +ℕ 2)) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2)) ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-set-Fin (n +ℕ 2)) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2)) ( is-set-quotient-equivalence-class ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( is-set-quotient-equivalence-class ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( quotient-loop-Fin n p , ( λ {x} {y} → preserves-R-invertible-action-D-equiv ( n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)) ( x) ( y))) abstract eq-quotient-delooping-sign-loop-equiv-is-set-quotient : (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → Id ( map-hom-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)) ( quotient-set-Fin (n +ℕ 2)) ( map-quotient-delooping-sign-loop-Fin n p)) ( pr1 (center (is-contr-equiv-quotient n p))) eq-quotient-delooping-sign-loop-equiv-is-set-quotient n p = ap pr1 { x = pair ( map-hom-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)) ( quotient-set-Fin (n +ℕ 2)) ( map-quotient-delooping-sign-loop-Fin n p)) ( coherence-square-map-quotient-delooping-sign-loop-Fin n p)} { y = center (is-contr-equiv-quotient n p)} ( eq-is-contr (is-contr-equiv-quotient n p)) cases-map-quotient-aut-Fin : ( n : ℕ) → ( h : type-Group (symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))) → ( is-decidable ( sim-Eq-Rel ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-aut-succ-succ-Fin n h) ( map-equiv ( invertible-action-D-equiv (n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( h)) ( quotient-aut-succ-succ-Fin n h)))) → type-Group (symmetric-Group (quotient-set-Fin (n +ℕ 2))) cases-map-quotient-aut-Fin n h (inl D) = id-equiv cases-map-quotient-aut-Fin n h (inr ND) = that-thing n ∘e (equiv-succ-Fin 2 ∘e (inv-equiv (that-thing n))) map-quotient-aut-Fin : (n : ℕ) → type-Group (symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) → type-Group (symmetric-Group (quotient-set-Fin (n +ℕ 2))) map-quotient-aut-Fin n h = cases-map-quotient-aut-Fin n h ( is-decidable-R ( n +ℕ 2) ( star) ( raise-UU-Fin-Fin (n +ℕ 2)) ( quotient-aut-succ-succ-Fin n h) ( map-equiv ( invertible-action-D-equiv (n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( h)) ( quotient-aut-succ-succ-Fin n h))) eq-map-quotient-aut-fin-transposition : (n : ℕ) (Y : 2-Element-Decidable-Subtype l1 (raise l1 (Fin (n +ℕ 2)))) → Id ( map-quotient-aut-Fin n (transposition Y)) ( that-thing n ∘e (equiv-succ-Fin 2 ∘e (inv-equiv (that-thing n)))) eq-map-quotient-aut-fin-transposition n Y = ap ( cases-map-quotient-aut-Fin n (transposition Y)) { x = is-decidable-R ( n +ℕ 2) ( star) ( raise-UU-Fin-Fin (n +ℕ 2)) ( quotient-aut-succ-succ-Fin n (transposition Y)) ( map-equiv ( invertible-action-D-equiv ( n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( transposition Y)) ( quotient-aut-succ-succ-Fin n (transposition Y)))} { y = inr (not-R-transposition-fin-succ-succ n Y)} ( eq-is-prop ( is-prop-is-decidable ( is-prop-sim-Eq-Rel ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-aut-succ-succ-Fin n (transposition Y)) ( map-equiv ( invertible-action-D-equiv ( n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( transposition Y)) ( quotient-aut-succ-succ-Fin n (transposition Y)))))) private this-third-thing : (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → D ( n +ℕ 2) ( raise-Fin l1 (n +ℕ 2) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) this-third-thing n p = quotient-aut-succ-succ-Fin n ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)) cases-eq-map-quotient-aut-Fin : ( n : ℕ) ( p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( D : is-decidable ( sim-Eq-Rel ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( this-third-thing n p) ( map-quotient-loop-Fin n p (this-third-thing n p)))) → ( k k' : Fin 2) → Id ( map-inv-equiv ( that-thing n) ( quotient-map-quotient-Fin (n +ℕ 2) (this-third-thing n p))) ( k) → Id ( map-inv-equiv ( that-thing n) ( quotient-map-quotient-Fin (n +ℕ 2) ( map-quotient-loop-Fin n p (this-third-thing n p)))) ( k') → Id ( map-equiv ( cases-map-quotient-aut-Fin n ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)) ( D)) ( quotient-map-quotient-Fin (n +ℕ 2) (this-third-thing n p))) ( quotient-map-quotient-Fin (n +ℕ 2) ( map-quotient-loop-Fin n p (this-third-thing n p))) cases-eq-map-quotient-aut-Fin n p (inl D) k k' q r = reflects-map-reflecting-map-Eq-Rel ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2)) ( D) cases-eq-map-quotient-aut-Fin n p (inr ND) (inl (inr star)) (inl (inr star)) q r = ex-falso ( ND ( map-equiv ( is-effective-is-set-quotient ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-set-Fin (n +ℕ 2)) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2)) ( is-set-quotient-equivalence-class ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( this-third-thing n p) ( map-quotient-loop-Fin n p (this-third-thing n p))) ( is-injective-map-equiv (inv-equiv (that-thing n)) (q ∙ inv r)))) cases-eq-map-quotient-aut-Fin n p (inr ND) (inl (inr star)) (inr star) q r = ( ap ( map-equiv (that-thing n)) ( ap (map-equiv (equiv-succ-Fin 2)) q ∙ inv r)) ∙ ( ap ( λ e → map-equiv e ( quotient-map-quotient-Fin (n +ℕ 2) ( map-quotient-loop-Fin n p (this-third-thing n p))))) ( right-inverse-law-equiv (that-thing n)) cases-eq-map-quotient-aut-Fin n p (inr ND) (inr star) (inl (inr star)) q r = ( ap ( map-equiv (that-thing n)) ( ap ( map-equiv (equiv-succ-Fin 2)) ( q) ∙ ( inv r))) ∙ ( ap ( λ e → map-equiv e ( quotient-map-quotient-Fin (n +ℕ 2) ( map-quotient-loop-Fin n p (this-third-thing n p))))) ( right-inverse-law-equiv (that-thing n)) cases-eq-map-quotient-aut-Fin n p (inr ND) (inr star) (inr star) q r = ex-falso ( ND ( map-equiv ( is-effective-is-set-quotient ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-set-Fin (n +ℕ 2)) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2)) ( is-set-quotient-equivalence-class ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( this-third-thing n p) ( map-quotient-loop-Fin n p (this-third-thing n p))) ( is-injective-map-equiv (inv-equiv (that-thing n)) (q ∙ inv r)))) eq-map-quotient-aut-Fin : (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → Id ( map-equiv ( map-quotient-aut-Fin n ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p))) ( quotient-map-quotient-Fin (n +ℕ 2) (this-third-thing n p))) ( quotient-map-quotient-Fin (n +ℕ 2) ( map-quotient-loop-Fin n p (this-third-thing n p))) eq-map-quotient-aut-Fin n p = cases-eq-map-quotient-aut-Fin n p ( is-decidable-R (n +ℕ 2) star ( raise-UU-Fin-Fin (n +ℕ 2)) ( this-third-thing n p) ( map-quotient-loop-Fin n p (this-third-thing n p))) ( map-inv-equiv ( that-thing n) ( quotient-map-quotient-Fin (n +ℕ 2) (this-third-thing n p))) ( map-inv-equiv ( that-thing n) ( quotient-map-quotient-Fin (n +ℕ 2) ( map-quotient-loop-Fin n p (this-third-thing n p)))) ( refl) ( refl) eq-map-quotient-aut-loop-equiv-is-set-quotient : (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → Id ( map-quotient-aut-Fin n ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p))) ( pr1 (center (is-contr-equiv-quotient n p))) eq-map-quotient-aut-loop-equiv-is-set-quotient n p = eq-equiv-eq-one-value-equiv-is-set-quotient ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2))) ( quotient-set-Fin (n +ℕ 2)) ( quotient-reflecting-map-quotient-Fin (n +ℕ 2)) ( is-set-quotient-equivalence-class ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( inv-equiv (that-thing n)) ( map-quotient-loop-Fin n p) ( λ {x} {y} → preserves-R-invertible-action-D-equiv ( n +ℕ 2) ( raise-UU-Fin-Fin (n +ℕ 2)) ( raise-UU-Fin-Fin (n +ℕ 2)) ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)) ( x) ( y)) ( map-equiv ( map-quotient-aut-Fin n ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)))) ( this-third-thing n p) ( eq-map-quotient-aut-Fin n p) ( is-equiv-map-equiv (quotient-loop-Fin n p)) ( is-equiv-map-equiv ( map-quotient-aut-Fin n ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( p)))) eq-quotient-delooping-sign-loop-sign-homomorphism : (n : ℕ) → Id ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( quotient-delooping-sign-loop n) ( hom-inv-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( hom-symmetric-group-equiv-Set ( Fin-Set 2) ( quotient-set-Fin (n +ℕ 2)) ( that-thing n))) ( sign-homomorphism ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( hom-inv-symmetric-group-equiv-Set ( Fin-Set (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( compute-raise-Fin l1 (n +ℕ 2)))) eq-quotient-delooping-sign-loop-sign-homomorphism n = map-inv-equiv ( equiv-ap-emb ( restriction-generating-subset-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( is-transposition-permutation-Prop {l2 = l1}) ( tr ( λ s → is-generating-subset-Group ( symmetric-Group (raise l1 (Fin (n +ℕ 2)) , s)) ( is-transposition-permutation-Prop)) ( eq-is-prop (is-prop-is-set (raise l1 (Fin (n +ℕ 2))))) ( is-generated-transposition-symmetric-Fin-Level ( n +ℕ 2) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))))) ( eq-htpy ( λ (f , s) → apply-universal-property-trunc-Prop s ( Id-Prop (set-Group (loop-group-Set (quotient-set-Fin (n +ℕ 2)))) ( map-emb ( restriction-generating-subset-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( is-transposition-permutation-Prop) ( tr ( λ s₁ → is-generating-subset-Group ( symmetric-Group (raise l1 (Fin (n +ℕ 2)) , s₁)) ( is-transposition-permutation-Prop)) ( eq-is-prop (is-prop-is-set (raise l1 (Fin (n +ℕ 2))))) ( is-generated-transposition-symmetric-Fin-Level ( n +ℕ 2) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( quotient-delooping-sign-loop n) ( hom-inv-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)))) ( f , s)) ( map-emb ( restriction-generating-subset-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( is-transposition-permutation-Prop) ( tr ( λ s₁ → is-generating-subset-Group ( symmetric-Group (raise l1 (Fin (n +ℕ 2)) , s₁)) ( is-transposition-permutation-Prop)) ( eq-is-prop (is-prop-is-set (raise l1 (Fin (n +ℕ 2))))) ( is-generated-transposition-symmetric-Fin-Level ( n +ℕ 2) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( hom-symmetric-group-equiv-Set ( Fin-Set 2) ( quotient-set-Fin (n +ℕ 2)) ( that-thing n))) ( sign-homomorphism (n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( hom-inv-symmetric-group-equiv-Set ( Fin-Set (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( compute-raise-Fin l1 (n +ℕ 2)))) ( f , s))) λ (Y , q) → ( eq-map-restriction-generating-subset-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( is-transposition-permutation-Prop) ( tr ( λ s₁ → is-generating-subset-Group ( symmetric-Group (raise l1 (Fin (n +ℕ 2)) , s₁)) ( is-transposition-permutation-Prop)) ( eq-is-prop (is-prop-is-set (raise l1 (Fin (n +ℕ 2))))) ( is-generated-transposition-symmetric-Fin-Level ( n +ℕ 2) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( quotient-delooping-sign-loop n) ( hom-inv-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)))) ( f , s)) ∙ ( htpy-eq-hom-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( id-hom-Group (loop-group-Set (quotient-set-Fin (n +ℕ 2)))) ( comp-hom-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( hom-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)))) ( inv ( is-retr-hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)))) ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ ( inv ( eq-equiv ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( f))) ( eq-is-prop is-prop-type-trunc-Prop))) ∙ ( ap ( map-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)))) ( eq-quotient-delooping-sign-loop-equiv-is-set-quotient n ( inv ( eq-equiv ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( f))) ∙ ( inv ( eq-map-quotient-aut-loop-equiv-is-set-quotient n ( inv ( eq-equiv ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( f)))))) ∙ ( ap ( λ g → map-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( map-quotient-aut-Fin n g)) ( commutative-inv-map-hom-symmetric-group-loop-group-Set ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( eq-equiv ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( f)) ( pr2 (raise-Fin-Set l1 (n +ℕ 2))) ( pr2 (raise-Fin-Set l1 (n +ℕ 2))) ∙ ( ap inv-equiv ( ap ( map-hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2))) ( ap ( eq-equiv ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2)))) ( inv (inv-inv-equiv f)) ∙ ( inv ( commutativity-inv-eq-equiv ( raise l1 (Fin (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2))) ( inv-equiv f)))) ∙ ( htpy-eq-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( hom-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2)))) ( id-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))) ( is-sec-hom-inv-symmetric-group-loop-group-Set ( raise-Fin-Set l1 (n +ℕ 2))) ( inv-equiv f) ∙ ( ap inv-equiv (inv q) ∙ ( own-inverse-is-involution ( is-involution-map-transposition Y))))))) ∙ ( ap ( map-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)))) ( ap ( map-quotient-aut-Fin n) ( own-inverse-is-involution ( is-involution-map-transposition Y)) ∙ ( eq-map-quotient-aut-fin-transposition n Y ∙ ( ap ( λ e → (that-thing n) ∘e (e ∘e inv-equiv ( that-thing n))) ( inv ( eq-sign-homomorphism-transposition ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv) ( map-equiv ( equiv-universes-2-Element-Decidable-Subtype ( Fin (n +ℕ 2)) ( l1) ( lzero)) ( transposition-conjugation-equiv {l4 = l1} ( raise l1 (Fin (n +ℕ 2))) ( Fin (n +ℕ 2)) ( inv-equiv (compute-raise-Fin l1 (n +ℕ 2))) ( Y)))) ∙ ( ap ( map-hom-Group ( symmetric-Group ( set-UU-Fin (n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( symmetric-Group (Fin-Set 2)) ( sign-homomorphism ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( inv ( eq-equiv-universes-transposition ( Fin (n +ℕ 2)) ( l1) ( lzero) ( transposition-conjugation-equiv ( raise l1 (Fin (n +ℕ 2))) ( Fin (n +ℕ 2)) ( inv-equiv (compute-raise-Fin l1 (n +ℕ 2))) ( Y))) ∙ ( eq-htpy-equiv ( correct-transposition-conjugation-equiv ( raise l1 (Fin (n +ℕ 2))) ( Fin (n +ℕ 2)) ( inv-equiv (compute-raise-Fin l1 (n +ℕ 2))) ( Y)) ∙ ( associative-comp-equiv ( inv-equiv ( inv-equiv ( compute-raise-Fin l1 (n +ℕ 2)))) ( transposition Y) ( inv-equiv ( compute-raise-Fin l1 (n +ℕ 2))) ∙ ( ap ( λ e → ( inv-equiv ( compute-raise-Fin l1 (n +ℕ 2))) ∘e ( transposition Y ∘e e)) ( inv-inv-equiv ( compute-raise-Fin l1 (n +ℕ 2))) ∙ ( ap ( λ e → ( inv-equiv ( compute-raise-Fin l1 (n +ℕ 2))) ∘e ( e ∘e compute-raise-Fin l1 (n +ℕ 2))) ( q))))))))))) ∙ ( inv ( eq-map-restriction-generating-subset-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( is-transposition-permutation-Prop) ( tr ( λ s → is-generating-subset-Group ( symmetric-Group (raise l1 (Fin (n +ℕ 2)) , s)) ( is-transposition-permutation-Prop)) ( eq-is-prop ( is-prop-is-set (raise l1 (Fin (n +ℕ 2))))) ( is-generated-transposition-symmetric-Fin-Level ( n +ℕ 2) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( hom-symmetric-group-equiv-Set ( Fin-Set 2) ( quotient-set-Fin (n +ℕ 2)) ( that-thing n))) ( sign-homomorphism ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( hom-inv-symmetric-group-equiv-Set ( Fin-Set (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( compute-raise-Fin l1 (n +ℕ 2)))) ( f , s))))))))) eq-quotient-delooping-loop-UU-Fin-Group : (n : ℕ) → Id ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set ( quotient-set-Fin (n +ℕ 2)) ( raise-Set l4 (Fin-Set 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))))) ( quotient-delooping-sign-loop n)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group l4 2) ( quotient-delooping-sign (n +ℕ 2))) ( hom-iso-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2))))) eq-quotient-delooping-loop-UU-Fin-Group n = eq-pair-Σ ( eq-htpy ( λ p → ap ( λ r → eq-pair-Σ r (eq-is-prop is-prop-type-trunc-Prop)) ( ap inv ( inv ( compute-eq-equiv ( raise l4 (Fin 2)) ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( raise l4 (Fin 2)) ( equiv-eq ( inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)))) ∘e ( inv-equiv ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n)))) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))) ∙ ( ap ( _∙ eq-counting-equivalence-class-R n) ( inv ( compute-eq-equiv ( raise l4 (Fin 2)) ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( inv-equiv ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))) ( equiv-eq ( inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop)))))) ∙ ( ap ( _∙ ( eq-equiv ( equivalence-class ( R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( equivalence-class ( R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( equiv-eq ( inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop))))))) ( inv ( commutativity-inv-eq-equiv ( equivalence-class ( R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( raise l4 (Fin 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n)))) ∙ ( ap ( λ e → inv (eq-counting-equivalence-class-R n) ∙ ( map-equiv e ( inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop)))))) ( left-inverse-law-equiv equiv-univalence)))))) ∙ ( distributive-inv-concat ( inv (eq-counting-equivalence-class-R n) ∙ ( inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop))))) ( eq-counting-equivalence-class-R n) ∙ ( ap ( inv (eq-counting-equivalence-class-R n) ∙_) ( distributive-inv-concat ( inv (eq-counting-equivalence-class-R n)) ( inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)))) ∙ ( ap ( _∙ inv (inv (eq-counting-equivalence-class-R n))) ( inv-inv ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop)))) ∙ ( ap ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop)) ∙_) ( inv-inv (eq-counting-equivalence-class-R n)))))))) ∙ ( ( ap ( eq-pair-Σ ( inv (eq-counting-equivalence-class-R n) ∙ ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)) ∙ ( eq-counting-equivalence-class-R n)))) ( eq-is-prop (is-trunc-Id (is-prop-type-trunc-Prop _ _))) ∙ ( inv ( compute-eq-pair-Σ ( pr2 (Fin-UU-Fin l4 2)) ( mere-equiv-D/R-fin-2 ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2)) ( star)) ( pr2 (Fin-UU-Fin l4 2)) ( inv (eq-counting-equivalence-class-R n)) ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)) ∙ ( eq-counting-equivalence-class-R n)) ( eq-is-prop is-prop-type-trunc-Prop) ( _)) ∙ ( ap ( eq-pair-Σ ( inv (eq-counting-equivalence-class-R n)) ( eq-is-prop is-prop-type-trunc-Prop) ∙_) ( inv ( compute-eq-pair-Σ ( mere-equiv-D/R-fin-2 ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2)) ( star)) ( mere-equiv-D/R-fin-2 ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2)) ( star)) ( pr2 (Fin-UU-Fin l4 2)) ( ap ( equivalence-class ∘ R (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop))) ( eq-counting-equivalence-class-R n) ( eq-is-prop is-prop-type-trunc-Prop) ( eq-is-prop is-prop-type-trunc-Prop)) ∙ ( ap ( _∙ ( eq-pair-Σ ( eq-equiv ( equivalence-class ( R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) ( raise l4 (Fin 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))) ( eq-is-prop is-prop-type-trunc-Prop))) ( ap ( λ w → eq-pair-Σ (pr1 w) (pr2 w)) { y = pair-eq-Σ ( ap ( map-quotient-delooping-sign (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop)))} ( eq-pair-Σ ( inv ( ap-pair-eq-Σ ( UU-Fin l1 (n +ℕ 2)) ( map-quotient-delooping-sign (n +ℕ 2)) ( Fin-UU-Fin l1 (n +ℕ 2)) ( Fin-UU-Fin l1 (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop)))) ( eq-is-prop ( is-trunc-Id (is-prop-type-trunc-Prop _ _)))) ∙ issec-pair-eq-Σ ( map-quotient-delooping-sign ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2))) ( map-quotient-delooping-sign ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2))) ( ap ( map-quotient-delooping-sign (n +ℕ 2)) ( eq-pair-Σ p ( eq-is-prop is-prop-type-trunc-Prop))))))))) ∙ ( ap ( _∙ ( ap ( map-quotient-delooping-sign (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop)) ∙ ( eq-pair-Σ ( eq-counting-equivalence-class-R n) ( eq-is-prop is-prop-type-trunc-Prop)))) ( ap ( eq-pair-Σ (inv (eq-counting-equivalence-class-R n))) ( eq-is-prop (is-trunc-Id (is-prop-type-trunc-Prop _ _))) ∙ ( inv ( inv-eq-pair-Σ ( mere-equiv-D/R-fin-2 ( n +ℕ 2) ( Fin-UU-Fin l1 (n +ℕ 2)) ( star)) ( pr2 (Fin-UU-Fin l4 2)) ( eq-counting-equivalence-class-R n) ( eq-is-prop is-prop-type-trunc-Prop)))) ∙ ( inv ( eq-tr-type-Ω ( eq-pair-Σ ( eq-counting-equivalence-class-R n) ( eq-is-prop is-prop-type-trunc-Prop)) ( ap (map-quotient-delooping-sign (n +ℕ 2)) ( eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop))))))))) ( eq-is-prop ( is-prop-preserves-mul-Semigroup ( semigroup-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( semigroup-Group (abstract-group-Concrete-Group (UU-Fin-Group l4 2))) ( pr1 ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group l4 2) ( quotient-delooping-sign (n +ℕ 2))) ( hom-iso-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))))))) symmetric-abstract-UU-fin-group-quotient-hom : (n : ℕ) → type-hom-Group ( symmetric-Group (Fin-Set 2)) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) symmetric-abstract-UU-fin-group-quotient-hom n = comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set ( quotient-set-Fin (n +ℕ 2)) ( raise-Set l4 (Fin-Set 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))))) ( hom-inv-symmetric-group-loop-group-Set (quotient-set-Fin (n +ℕ 2)))) ( hom-symmetric-group-equiv-Set ( Fin-Set 2) ( quotient-set-Fin (n +ℕ 2)) ( that-thing n)) eq-quotient-delooping-sign-homomorphism : (n : ℕ) → Id ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group l4 2) ( quotient-delooping-sign (n +ℕ 2))) ( hom-inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( symmetric-abstract-UU-fin-group-quotient-hom n) ( sign-homomorphism ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( hom-inv-symmetric-group-equiv-Set ( Fin-Set (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( compute-raise-Fin l1 (n +ℕ 2)))) eq-quotient-delooping-sign-homomorphism n = ( ap ( λ f → comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( f) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( inv (eq-quotient-delooping-loop-UU-Fin-Group n))) ∙ ( associative-comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set ( quotient-set-Fin (n +ℕ 2)) ( raise-Set l4 (Fin-Set 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))))) ( quotient-delooping-sign-loop n) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ∙ ( ap ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set ( quotient-set-Fin (n +ℕ 2)) ( raise-Set l4 (Fin-Set 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n)))))) ( eq-quotient-delooping-sign-loop-sign-homomorphism n) ∙ ( eq-pair-Σ ( refl) ( eq-is-prop ( is-prop-preserves-mul-Semigroup ( semigroup-Group (symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))) ( semigroup-Group ( abstract-group-Concrete-Group (UU-Fin-Group l4 2))) ( pr1 ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group ( abstract-group-Concrete-Group ( UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set ( quotient-set-Fin (n +ℕ 2)) ( raise-Set l4 (Fin-Set 2)) ( compute-raise-Fin l4 2 ∘e inv-equiv (that-thing n))))) ( hom-inv-symmetric-group-loop-group-Set ( quotient-set-Fin (n +ℕ 2)))) ( hom-symmetric-group-equiv-Set ( Fin-Set 2) ( quotient-set-Fin (n +ℕ 2)) ( that-thing n))) ( sign-homomorphism ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( hom-inv-symmetric-group-equiv-Set (Fin-Set (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( compute-raise-Fin l1 (n +ℕ 2))))))))))
General case for the construction of the delooping of sign homomorphism (Proposition 22)
module _ { l1 l2 : Level} ( Q : (n : ℕ) → UU-Fin l1 n → UU-Fin l2 2) ( equiv-Q-fin-fin-2 : (n : ℕ) → leq-ℕ 2 n → Fin 2 ≃ ( type-UU-Fin 2 ( Q n (raise l1 (Fin n) , unit-trunc-Prop (compute-raise-Fin l1 n))))) ( Q-transposition-swap : (n : ℕ) → ( Y : 2-Element-Decidable-Subtype l1 (raise-Fin l1 (n +ℕ 2))) → ( x : type-UU-Fin 2 ( Q ( n +ℕ 2) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) → ¬ ( x ＝ ( map-equiv ( univalent-action-equiv ( mere-equiv-Prop (Fin (n +ℕ 2))) ( type-UU-Fin 2 ∘ Q (n +ℕ 2)) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( raise l1 (Fin (n +ℕ 2)) , unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))) ( transposition Y)) ( x)))) where private equiv-Q-equivalence-class : (n : ℕ) (X : UU-Fin l1 n) → type-UU-Fin 2 (Q n X) ≃ equivalence-class (Id-Eq-Rel (set-UU-Fin 2 (Q n X))) equiv-Q-equivalence-class n X = equiv-uniqueness-set-quotient ( Id-Eq-Rel (set-UU-Fin 2 (Q n X))) ( set-UU-Fin 2 (Q n X)) ( id-reflecting-map-Id-Eq-Rel (set-UU-Fin 2 (Q n X))) ( is-set-quotient-id-Id-Eq-Rel (set-UU-Fin 2 (Q n X))) ( equivalence-class-Set (Id-Eq-Rel (set-UU-Fin 2 (Q n X)))) ( quotient-reflecting-map-equivalence-class ( Id-Eq-Rel (set-UU-Fin 2 (Q n X)))) ( is-set-quotient-equivalence-class ( Id-Eq-Rel (set-UU-Fin 2 (Q n X)))) equiv-fin-2-equivalence-class : (n : ℕ) (X : UU-Fin l1 n) → leq-ℕ 2 n → Fin n ≃ type-UU-Fin n X → Fin 2 ≃ equivalence-class (Id-Eq-Rel (set-UU-Fin 2 (Q n X))) equiv-fin-2-equivalence-class n X H h = tr ( λ Y → Fin 2 ≃ equivalence-class (Id-Eq-Rel (set-UU-Fin 2 (Q n Y)))) ( eq-pair-Σ ( eq-equiv (raise l1 (Fin n)) (type-UU-Fin n X) ( h ∘e inv-equiv (compute-raise-Fin l1 n))) ( eq-is-prop is-prop-type-trunc-Prop)) ( equiv-Q-equivalence-class n ( raise l1 (Fin n) , unit-trunc-Prop (compute-raise-Fin l1 n)) ∘e equiv-Q-fin-fin-2 n H) delooping-sign : (n : ℕ) → hom-Concrete-Group (UU-Fin-Group l1 n) (UU-Fin-Group (lsuc l2) 2) delooping-sign = quotient-delooping-sign ( λ n X → type-UU-Fin 2 (Q n X)) ( λ n X → Id-Eq-Rel (set-UU-Fin 2 (Q n X))) ( λ n _ X → has-decidable-equality-has-cardinality 2 (pr2 (Q n X))) ( equiv-fin-2-equivalence-class) ( λ n _ → map-equiv (equiv-Q-fin-fin-2 (n +ℕ 2) star) (zero-Fin 1)) ( λ n Y → Q-transposition-swap n Y ( pr1 (equiv-Q-fin-fin-2 (n +ℕ 2) star) (zero-Fin 1))) eq-delooping-sign-homomorphism : (n : ℕ) → Id ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group (lsuc l2) 2) ( delooping-sign (n +ℕ 2))) ( hom-inv-iso-Group ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( symmetric-abstract-UU-fin-group-quotient-hom ( λ n X → type-UU-Fin 2 (Q n X)) ( λ n X → Id-Eq-Rel (set-UU-Fin 2 (Q n X))) ( λ n _ X → has-decidable-equality-has-cardinality 2 (pr2 (Q n X))) ( equiv-fin-2-equivalence-class) ( λ n _ → pr1 (equiv-Q-fin-fin-2 (n +ℕ 2) star) (zero-Fin 1)) ( λ n Y → Q-transposition-swap n Y ( pr1 (equiv-Q-fin-fin-2 (n +ℕ 2) star) (zero-Fin 1))) ( n)) ( sign-homomorphism ( n +ℕ 2) ( Fin (n +ℕ 2) , unit-trunc-Prop id-equiv))) ( hom-inv-symmetric-group-equiv-Set ( Fin-Set (n +ℕ 2)) ( raise-Fin-Set l1 (n +ℕ 2)) ( compute-raise-Fin l1 (n +ℕ 2)))) eq-delooping-sign-homomorphism = eq-quotient-delooping-sign-homomorphism ( λ n X → type-UU-Fin 2 (Q n X)) ( λ n X → Id-Eq-Rel (set-UU-Fin 2 (Q n X))) ( λ n _ X → has-decidable-equality-has-cardinality 2 (pr2 (Q n X))) ( equiv-fin-2-equivalence-class) ( λ n _ → pr1 (equiv-Q-fin-fin-2 (n +ℕ 2) star) (zero-Fin 1)) ( λ n Y → Q-transposition-swap n Y ( pr1 (equiv-Q-fin-fin-2 (n +ℕ 2) star) (zero-Fin 1)))
See also
- Definition of the delooping of the sign homomorphism based on Cartier
finite-group-theory.cartier-delooping-sign-homomorphism. - Definition of the delooping of the sign homomorphism based on Simpson
finite-group-theory.simpson-delooping-sign-homomorphism.
References
- Mangel É. and Rijke E. "Delooping the sign homomorphism in univalent mathematics".