refactoring

src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md

@@ -17,6 +17,7 @@ open import finite-group-theory.finite-type-groups
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
+open import foundation.action-on-equivalences-type-families
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
@@ -28,8 +29,8 @@ open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.transport
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
-open import foundation.univalence-action-on-equivalences
 open import foundation.universe-levels
 
 open import group-theory.concrete-groups
@@ -69,7 +70,7 @@ module _
         ( star)
         ( transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-on-equivalences-family-of-types-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( orientation-Complete-Undirected-Graph (n +ℕ 2))
           ( raise l (Fin (n +ℕ 2)) ,
@@ -110,17 +111,19 @@ module _
           preserves-id-equiv-orientation-complete-undirected-graph-equiv
             ( n +ℕ 2)}
         { y =
-          ( univalent-action-equiv
+          ( action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2))) ,
-          ( preserves-id-equiv-univalent-action-equiv
+          ( compute-id-equiv-action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( orientation-Complete-Undirected-Graph (n +ℕ 2))
-            ( is-set-orientation-Complete-Undirected-Graph (n +ℕ 2)))))
+          ( is-contr-equiv' _
+            ( distributive-Π-Σ)
+            ( is-contr-Π
+              ( unique-action-on-equivalences-family-of-types-subuniverse
+                  ( mere-equiv-Prop (Fin (n +ℕ 2)))
+                  ( orientation-Complete-Undirected-Graph (n +ℕ 2)))))))
       ( not-even-difference-orientation-aut-transposition-count
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -18,7 +18,9 @@ open import finite-group-theory.permutations
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
+open import foundation.action-on-equivalences-type-families
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.commuting-squares-of-maps
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -30,6 +32,7 @@ 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-induction
 open import foundation.equivalence-relations
 open import foundation.equivalences
 open import foundation.function-extensionality
@@ -52,7 +55,6 @@ 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
 
@@ -120,7 +122,8 @@ module _
     D ( n +ℕ 2)
       ( raise-Fin l1 (n +ℕ 2),
         unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))
-  ( not-R-transposition-fin-succ-succ : (n : ℕ) →
+  ( not-R-transposition-fin-succ-succ :
+    (n : ℕ) →
     ( Y : 2-Element-Decidable-Subtype l1 (raise-Fin l1 (n +ℕ 2))) →
     ¬ ( sim-Eq-Rel
       ( R
@@ -129,7 +132,7 @@ module _
           unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))
       ( quotient-aut-succ-succ-Fin n (transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-on-equivalences-family-of-types-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( D (n +ℕ 2))
           ( raise l1 (Fin (n +ℕ 2)) ,
@@ -165,13 +168,17 @@ module _
       (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)
+      action-on-equivalences-family-of-types-subuniverse
+        ( 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)
+      compute-id-equiv-action-on-equivalences-family-of-types-subuniverse
+        ( mere-equiv-Prop (Fin n))
+        ( D n)
 
     preserves-R-invertible-action-D-equiv :
       ( n : ℕ) →
@@ -183,14 +190,29 @@ module _
           ( 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
+    preserves-R-invertible-action-D-equiv n X =
+      ind-equiv-subuniverse
+        ( mere-equiv-Prop (Fin 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')
+            sim-Eq-Rel
+              ( R n Y)
+              ( map-equiv (invertible-action-D-equiv n X Y f) a)
+              ( map-equiv (invertible-action-D-equiv n X Y f) a')))
+        ( λ a a' →
+          ( iff-equiv
+            ( equiv-binary-tr
+              ( sim-Eq-Rel (R n X))
+              ( inv
+                ( ap
+                  ( λ g → map-equiv g a)
+                  ( preserves-id-equiv-invertible-action-D-equiv n X)))
+              ( inv
+                ( ap
+                  ( λ g → map-equiv g a')
+                  ( preserves-id-equiv-invertible-action-D-equiv n X))))))
 
     raise-UU-Fin-Fin : (n : ℕ) → UU-Fin l1 n
     pr1 (raise-UU-Fin-Fin n) = raise l1 (Fin n)
@@ -1488,7 +1510,7 @@ module _
             unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) →
     ¬ ( x ＝
         ( map-equiv
-          ( univalent-action-equiv
+          ( action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( type-UU-Fin 2 ∘ Q (n +ℕ 2))
             ( raise l1 (Fin (n +ℕ 2)) ,

src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md

@@ -21,6 +21,7 @@ open import finite-group-theory.permutations
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
+open import foundation.action-on-equivalences-type-families
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -42,8 +43,8 @@ open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.sets
 open import foundation.transport
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
-open import foundation.univalence-action-on-equivalences
 open import foundation.universe-levels
 
 open import group-theory.concrete-groups
@@ -681,7 +682,7 @@ module _
           unit-trunc-Prop (compute-raise-Fin l (n +ℕ 2))))
       ( sign-comp-aut-succ-succ-Fin n (transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-on-equivalences-family-of-types-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( λ X → Fin (n +ℕ 2) ≃ pr1 X)
           ( raise l (Fin (n +ℕ 2)) ,
@@ -714,20 +715,19 @@ module _
           simpson-comp-equiv (n +ℕ 2) ,
           preserves-id-equiv-simpson-comp-equiv (n +ℕ 2)}
         { y =
-          ( univalent-action-equiv
+          ( action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) ,
-            ( preserves-id-equiv-univalent-action-equiv
+            ( compute-id-equiv-action-on-equivalences-family-of-types-subuniverse
               ( mere-equiv-Prop (Fin (n +ℕ 2)))
               ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X)
-            ( λ X →
-              is-set-equiv-is-set
-                ( is-set-Fin (n +ℕ 2))
-                ( is-set-type-UU-Fin (n +ℕ 2) X)))))
+          ( is-contr-equiv' _
+            ( distributive-Π-Σ)
+            ( is-contr-Π
+              ( unique-action-on-equivalences-family-of-types-subuniverse
+                ( mere-equiv-Prop (Fin (n +ℕ 2)))
+                ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X))))))
       ( not-sign-comp-transposition-count
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 

src/foundation-core.lagda.md

@@ -24,7 +24,6 @@ open import foundation-core.embeddings public
 open import foundation-core.empty-types public
 open import foundation-core.endomorphisms public
 open import foundation-core.equality-dependent-pair-types public
-open import foundation-core.equivalence-induction public
 open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
 open import foundation-core.fibers-of-maps public

src/foundation.lagda.md

@@ -10,6 +10,7 @@ open import foundation.0-images-of-maps public
 open import foundation.0-maps public
 open import foundation.1-types public
 open import foundation.2-types public
+open import foundation.action-on-equivalences-type-families public
 open import foundation.action-on-identifications-binary-functions public
 open import foundation.action-on-identifications-dependent-functions public
 open import foundation.action-on-identifications-functions public
@@ -246,6 +247,7 @@ open import foundation.subtype-identity-principle public
 open import foundation.subtypes public
 open import foundation.subuniverses public
 open import foundation.surjective-maps public
+open import foundation.symmetric-binary-relations public
 open import foundation.symmetric-difference public
 open import foundation.symmetric-identity-types public
 open import foundation.symmetric-operations public
@@ -281,7 +283,6 @@ open import foundation.uniqueness-truncation public
 open import foundation.unit-type public
 open import foundation.unital-binary-operations public
 open import foundation.univalence public
-open import foundation.univalence-action-on-equivalences public
 open import foundation.univalence-implies-function-extensionality public
 open import foundation.univalent-type-families public
 open import foundation.universal-property-booleans public