Transport along and action on equivalences (#706)

UniMath · Sep 11, 2023 · a0c49ae · a0c49ae
1 parent 1f4c008
commit a0c49ae
Show file tree

Hide file tree

Showing 198 changed files with 694 additions and 321 deletions.
diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md
@@ -28,7 +28,7 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 ```
 

diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -37,7 +37,7 @@ open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.negation
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import univalent-combinatorics.standard-finite-types

diff --git a/src/elementary-number-theory/cofibonacci.lagda.md b/src/elementary-number-theory/cofibonacci.lagda.md
@@ -22,7 +22,7 @@ open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 

diff --git a/src/elementary-number-theory/congruence-integers.lagda.md b/src/elementary-number-theory/congruence-integers.lagda.md
@@ -22,7 +22,7 @@ open import foundation.binary-relations
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 

diff --git a/src/elementary-number-theory/congruence-natural-numbers.lagda.md b/src/elementary-number-theory/congruence-natural-numbers.lagda.md
@@ -19,7 +19,7 @@ open import foundation.binary-relations
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import univalent-combinatorics.standard-finite-types

diff --git a/src/elementary-number-theory/distance-natural-numbers.lagda.md b/src/elementary-number-theory/distance-natural-numbers.lagda.md
@@ -19,7 +19,7 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

diff --git a/src/elementary-number-theory/divisibility-integers.lagda.md b/src/elementary-number-theory/divisibility-integers.lagda.md
@@ -27,7 +27,7 @@ open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositional-maps
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

diff --git a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
@@ -23,7 +23,7 @@ open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositional-maps
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-empty-type
 open import foundation.unit-type
 open import foundation.universe-levels

diff --git a/src/elementary-number-theory/fibonacci-sequence.lagda.md b/src/elementary-number-theory/fibonacci-sequence.lagda.md
@@ -17,7 +17,7 @@ open import elementary-number-theory.relatively-prime-natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
-open import foundation.transport
+open import foundation.transport-along-identifications
 ```
 
 </details>

diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
@@ -35,7 +35,7 @@ open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-empty-type
 open import foundation.unit-type
 open import foundation.universe-levels

diff --git a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md
@@ -24,7 +24,7 @@ open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

diff --git a/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md
@@ -30,7 +30,7 @@ open import foundation.empty-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 

diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md
@@ -19,7 +19,7 @@ open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

diff --git a/src/elementary-number-theory/powers-of-two.lagda.md b/src/elementary-number-theory/powers-of-two.lagda.md
@@ -21,7 +21,7 @@ open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-types
 open import foundation.split-surjective-maps
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types

diff --git a/src/elementary-number-theory/prime-numbers.lagda.md b/src/elementary-number-theory/prime-numbers.lagda.md
@@ -28,7 +28,7 @@ open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

diff --git a/src/elementary-number-theory/reduced-integer-fractions.lagda.md b/src/elementary-number-theory/reduced-integer-fractions.lagda.md
@@ -26,7 +26,7 @@ open import foundation.equality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 

diff --git a/src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md b/src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md
@@ -20,7 +20,7 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 

diff --git a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
@@ -22,7 +22,7 @@ open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositions
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 ```

diff --git a/...elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md b/...elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md
@@ -31,7 +31,7 @@ open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.subtypes
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-coproduct-types
 open import foundation.type-arithmetic-empty-type
 open import foundation.type-arithmetic-unit-type

diff --git a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md b/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-families-over-subuniverses
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
@@ -27,9 +28,8 @@ open import foundation.mere-equivalences
 open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
-open import foundation.univalence-action-on-equivalences
 open import foundation.universe-levels
 
 open import group-theory.concrete-groups
@@ -57,7 +57,7 @@ module _
   { l : Level}
   where
 
-  not-even-difference-univalent-action-equiv :
+  not-even-difference-action-equiv-family-on-subuniverse :
     (n : ℕ) (Y : 2-Element-Decidable-Subtype l (raise-Fin l (n +ℕ 2))) →
     ¬ ( sim-Equivalence-Relation
       ( even-difference-orientation-Complete-Undirected-Graph
@@ -69,7 +69,7 @@ module _
         ( star)
         ( transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-equiv-family-on-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( orientation-Complete-Undirected-Graph (n +ℕ 2))
           ( raise l (Fin (n +ℕ 2)) ,
@@ -79,7 +79,7 @@ module _
           ( transposition Y))
         ( orientation-aut-count
           (n +ℕ 2 , compute-raise l (Fin (n +ℕ 2))) star (transposition Y))))
-  not-even-difference-univalent-action-equiv n =
+  not-even-difference-action-equiv-family-on-subuniverse n =
     tr
       ( λ f →
         ( Y : 2-Element-Decidable-Subtype l
@@ -110,14 +110,14 @@ module _
           preserves-id-equiv-orientation-complete-undirected-graph-equiv
             ( n +ℕ 2)}
         { y =
-          ( univalent-action-equiv
+          ( action-equiv-family-on-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2))) ,
-          ( preserves-id-equiv-univalent-action-equiv
+          ( preserves-id-equiv-action-equiv-family-on-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv
+          ( is-contr-preserves-id-action-equiv-family-on-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2))
             ( is-set-orientation-Complete-Undirected-Graph (n +ℕ 2)))))
@@ -135,7 +135,7 @@ module _
       ( equiv-fin-2-quotient-sign-equiv-Fin)
       ( λ n →
         orientation-aut-count (n +ℕ 2 , compute-raise l (Fin (n +ℕ 2))) (star))
-      ( not-even-difference-univalent-action-equiv)
+      ( not-even-difference-action-equiv-family-on-subuniverse)
 
   eq-cartier-delooping-sign-homomorphism :
     (n : ℕ) →
@@ -176,7 +176,7 @@ module _
               orientation-aut-count
                 ( n +ℕ 2 , compute-raise l (Fin (n +ℕ 2)))
                 ( star))
-            ( not-even-difference-univalent-action-equiv)
+            ( not-even-difference-action-equiv-family-on-subuniverse)
             ( n))
           ( sign-homomorphism
             ( n +ℕ 2)
@@ -194,7 +194,7 @@ module _
       ( equiv-fin-2-quotient-sign-equiv-Fin)
       ( λ n →
         orientation-aut-count (n +ℕ 2 , compute-raise l (Fin (n +ℕ 2))) (star))
-      ( not-even-difference-univalent-action-equiv)
+      ( not-even-difference-action-equiv-family-on-subuniverse)
 ```
 
 ## References

diff --git a/src/finite-group-theory/concrete-quaternion-group.lagda.md b/src/finite-group-theory/concrete-quaternion-group.lagda.md
@@ -13,7 +13,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.isolated-points
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import univalent-combinatorics.complements-isolated-points

diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
@@ -18,6 +18,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-families-over-subuniverses
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-maps
 open import foundation.contractible-types
@@ -47,12 +48,11 @@ open import foundation.propositions
 open import foundation.raising-universe-levels
 open import foundation.reflecting-maps-equivalence-relations
 open import foundation.sets
-open import foundation.transport
+open import foundation.transport-along-identifications
 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
 
@@ -129,7 +129,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-equiv-family-on-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( D (n +ℕ 2))
           ( raise l1 (Fin (n +ℕ 2)) ,
@@ -165,13 +165,15 @@ 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-equiv-family-on-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)
+      preserves-id-equiv-action-equiv-family-on-subuniverse
+        ( mere-equiv-Prop (Fin n))
+        ( D n)
 
     preserves-R-invertible-action-D-equiv :
       ( n : ℕ) →
@@ -184,7 +186,7 @@ module _
           ( 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
+      Ind-action-equiv-family-on-subuniverse (mere-equiv-Prop (Fin n)) (D n) X
         ( λ Y f →
           ( a a' : D n X) →
           ( sim-Equivalence-Relation (R n X) a a' ↔
@@ -1098,7 +1100,7 @@ module _
             ( λ r → eq-pair-Σ r (eq-is-prop is-prop-type-trunc-Prop))
             ( ap inv
               ( inv
-                ( compute-eq-equiv
+                ( compute-eq-equiv-comp-equiv
                   ( raise l4 (Fin 2))
                   ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2))))
                   ( raise l4 (Fin 2))
@@ -1113,7 +1115,7 @@ module _
                 ( ap
                   ( _∙ eq-counting-equivalence-class-R n)
                   ( inv
-                    ( compute-eq-equiv
+                    ( compute-eq-equiv-comp-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))))
@@ -1488,7 +1490,7 @@ module _
             unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) →
     ¬ ( x ＝
         ( map-equiv
-          ( univalent-action-equiv
+          ( action-equiv-family-on-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( type-UU-Fin 2 ∘ Q (n +ℕ 2))
             ( raise l1 (Fin (n +ℕ 2)) ,

diff --git a/src/finite-group-theory/orbits-permutations.lagda.md b/src/finite-group-theory/orbits-permutations.lagda.md
@@ -48,7 +48,7 @@ open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.repetitions-of-values
 open import foundation.sets
-open import foundation.transport
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels