diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md index 536b969aa3..b94ea9b729 100644 --- 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 index 19ad5b7dc7..ad127678d2 100755 --- 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 index e80bd5387e..8d1f91db9b 100644 --- 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 index 51d82b086d..9844348d01 100644 --- 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 index 732c75a31d..57781d53a3 100644 --- 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 index 4aa61b2b9e..0426593e35 100644 --- 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 index e570a1a875..b6c1fc7453 100644 --- 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 index 97ce7e55af..869a1a4189 100644 --- 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 index ed4d4e50cf..634cc34706 100644 --- 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 ``` diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md index b05cff6d00..992aa4a2fa 100644 --- 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 index 8fa61c143e..2dc2e9236a 100644 --- 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 index 32b773f17b..8b4fdaaa35 100644 --- 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 index 2955f6bf44..aa92163af9 100644 --- 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 index d1b2c00db1..9efb3ca6ba 100644 --- 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 index ad4ce088ba..00cb8b2065 100644 --- 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 index a6dd71808f..06aa1843e5 100644 --- 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 index 61c91bb897..fbf54cb39d 100644 --- 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 index d238bcd5ca..6c3c272478 100644 --- 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/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md b/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md index e392a72dba..3e7b58ad9d 100644 --- a/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md +++ b/src/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 index 0271529c3a..5c0505d499 100644 --- 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 index 0c66d78790..d03507a4e9 100644 --- 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 index 6e0e2e613d..5e28858730 100644 --- 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 index bd6ec99e84..fb5cbb2b6e 100644 --- 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 diff --git a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md index 24684b9e42..f85e3e3227 100644 --- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md +++ b/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-families-over-subuniverses open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.coproduct-types @@ -41,9 +42,8 @@ open import foundation.negation open import foundation.propositional-truncations open import foundation.raising-universe-levels open import foundation.sets -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 @@ -673,7 +673,7 @@ module _ Fin (n +ℕ 2) ≃ raise l (Fin (n +ℕ 2)) sign-comp-aut-succ-succ-Fin n = _∘e compute-raise l (Fin (n +ℕ 2)) - not-univalent-action-equiv-transposition : + not-action-equiv-family-on-subuniverse-transposition : ( n : ℕ) → ( Y : 2-Element-Decidable-Subtype l ( raise-Fin l (n +ℕ 2))) → @@ -683,7 +683,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-equiv-family-on-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( λ X → Fin (n +ℕ 2) ≃ pr1 X) ( raise l (Fin (n +ℕ 2)) , @@ -692,7 +692,7 @@ module _ unit-trunc-Prop (compute-raise-Fin l (n +ℕ 2))) ( transposition Y)) ( sign-comp-aut-succ-succ-Fin n (transposition Y)))) - not-univalent-action-equiv-transposition n = + not-action-equiv-family-on-subuniverse-transposition n = tr ( λ f → ( Y : 2-Element-Decidable-Subtype l @@ -716,14 +716,14 @@ module _ simpson-comp-equiv (n +ℕ 2) , preserves-id-equiv-simpson-comp-equiv (n +ℕ 2)} { y = - ( univalent-action-equiv + ( action-equiv-family-on-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) , - ( preserves-id-equiv-univalent-action-equiv + ( preserves-id-equiv-action-equiv-family-on-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 + ( is-contr-preserves-id-action-equiv-family-on-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) ( λ X → @@ -743,7 +743,7 @@ module _ ( λ n _ → is-decidable-sign-comp-Equivalence-Relation n) ( equiv-fin-2-quotient-sign-comp-equiv-Fin) ( sign-comp-aut-succ-succ-Fin) - ( not-univalent-action-equiv-transposition) + ( not-action-equiv-family-on-subuniverse-transposition) eq-simpson-delooping-sign-homomorphism : (n : ℕ) → @@ -779,7 +779,7 @@ module _ ( λ n H → is-decidable-sign-comp-Equivalence-Relation n) ( equiv-fin-2-quotient-sign-comp-equiv-Fin) ( sign-comp-aut-succ-succ-Fin) - ( not-univalent-action-equiv-transposition) + ( not-action-equiv-family-on-subuniverse-transposition) ( n)) ( sign-homomorphism ( n +ℕ 2) @@ -795,7 +795,7 @@ module _ ( λ n _ → is-decidable-sign-comp-Equivalence-Relation n) ( equiv-fin-2-quotient-sign-comp-equiv-Fin) ( sign-comp-aut-succ-succ-Fin) - ( not-univalent-action-equiv-transposition) + ( not-action-equiv-family-on-subuniverse-transposition) ``` ## References diff --git a/src/finite-group-theory/transpositions.lagda.md b/src/finite-group-theory/transpositions.lagda.md index ccebbd1f04..6e2f1f1ff4 100644 --- a/src/finite-group-theory/transpositions.lagda.md +++ b/src/finite-group-theory/transpositions.lagda.md @@ -40,7 +40,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.raising-universe-levels open import foundation.sets -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.univalence diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index db9d5bf817..6c53df4bc0 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -47,7 +47,7 @@ open import foundation-core.sets public open import foundation-core.singleton-induction public open import foundation-core.small-types public open import foundation-core.subtypes public -open import foundation-core.transport public +open import foundation-core.transport-along-identifications public open import foundation-core.truncated-maps public open import foundation-core.truncated-types public open import foundation-core.truncation-levels public diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md index f9309add78..e56ad2bd90 100644 --- a/src/foundation-core/contractible-types.lagda.md +++ b/src/foundation-core/contractible-types.lagda.md @@ -18,7 +18,7 @@ open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.retractions -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/dependent-identifications.lagda.md b/src/foundation-core/dependent-identifications.lagda.md index 9a5da82082..55178798aa 100644 --- a/src/foundation-core/dependent-identifications.lagda.md +++ b/src/foundation-core/dependent-identifications.lagda.md @@ -10,7 +10,7 @@ module foundation-core.dependent-identifications where open import foundation.universe-levels open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` @@ -26,10 +26,11 @@ identification tr B p u ＝ v, ``` -where `tr` is the [transport](foundation-core.transport.md) function. Dependent -identifications also satisfy groupoid laws, which are formulated appropriately -as dependent identifications. The groupoid laws for dependent identifications -are proven in +where `tr` is the +[transport](foundation-core.transport-along-identifications.md) function. +Dependent identifications also satisfy groupoid laws, which are formulated +appropriately as dependent identifications. The groupoid laws for dependent +identifications are proven in [`foundation.dependent-identifications`](foundation.dependent-identifications.md). ## Definition diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md index 1e4bb29d48..f80cefffdd 100644 --- a/src/foundation-core/equality-dependent-pair-types.lagda.md +++ b/src/foundation-core/equality-dependent-pair-types.lagda.md @@ -15,7 +15,7 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md index cd073f11df..788aea7aef 100644 --- a/src/foundation-core/fibers-of-maps.lagda.md +++ b/src/foundation-core/fibers-of-maps.lagda.md @@ -16,7 +16,7 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/functoriality-dependent-function-types.lagda.md b/src/foundation-core/functoriality-dependent-function-types.lagda.md index b2d10f0ab2..38efcd3954 100644 --- a/src/foundation-core/functoriality-dependent-function-types.lagda.md +++ b/src/foundation-core/functoriality-dependent-function-types.lagda.md @@ -26,7 +26,7 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.path-split-maps -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md index d07321c3d6..acfba966fb 100644 --- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation-core/functoriality-dependent-pair-types.lagda.md @@ -18,7 +18,7 @@ open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md index 389be5b157..591cf6bcf6 100644 --- a/src/foundation-core/homotopies.lagda.md +++ b/src/foundation-core/homotopies.lagda.md @@ -15,7 +15,7 @@ open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.function-types open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md index ff9084fa8b..abe72f3028 100644 --- a/src/foundation-core/identity-types.lagda.md +++ b/src/foundation-core/identity-types.lagda.md @@ -49,27 +49,27 @@ width equals sign `＝`. The following table lists files that are about identity types and operations on identifications in arbitrary types. -| Concept | File | -| ------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------- | -| Action on identifications of binary functions | [`foundation.action-on-identifications-binary-functions`](foundation.action-on-identifications-binary-functions.md) | -| Action on identifications of dependent functions | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) | -| Action on identifications of functions | [`foundation.action-on-identifications-functions`](foundation.action-on-identifications-functions.md) | -| Binary transport | [`foundation.binary-transport`](foundation.binary-transport.md) | -| Commuting squares of identifications | [`foundation.commuting-squares-of-identifications`](foundation.commuting-squares-of-identifications.md) | -| Dependent identifications (foundation) | [`foundation.dependent-identifications`](foundation.dependent-identifications.md) | -| Dependent identifications (foundation-core) | [`foundation-core.dependent-identifications`](foundation-core.dependent-identifications.md) | -| The fundamental theorem of identity types | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md) | -| Hexagons of identifications | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md) | -| Identity systems | [`foundation.identity-systems`](foundation.identity-systems.md) | -| The identity type (foundation) | [`foundation.identity-types`](foundation.identity-types.md) | -| The identity type (foundation-core) | [`foundation-core.identity-types`](foundation-core.identity-types.md) | -| Large identity types | [`foundation.large-identity-types`](foundation.large-identity-types.md) | -| Path algebra | [`foundation.path-algebra`](foundation.path-algebra.md) | -| Symmetric identity types | [`foundation.symmetric-identity-types`](foundation.symmetric-identity-types.md) | -| Torsorial type families | [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) | -| Transport (foundation) | [`foundation.transport`](foundation.transport.md) | -| Transport (foundation-core) | [`foundation-core.transport`](foundation-core.transport.md) | -| The universal property of identity types | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) | +| Concept | File | +| ------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------- | +| Action on identifications of binary functions | [`foundation.action-on-identifications-binary-functions`](foundation.action-on-identifications-binary-functions.md) | +| Action on identifications of dependent functions | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) | +| Action on identifications of functions | [`foundation.action-on-identifications-functions`](foundation.action-on-identifications-functions.md) | +| Binary transport | [`foundation.binary-transport`](foundation.binary-transport.md) | +| Commuting squares of identifications | [`foundation.commuting-squares-of-identifications`](foundation.commuting-squares-of-identifications.md) | +| Dependent identifications (foundation) | [`foundation.dependent-identifications`](foundation.dependent-identifications.md) | +| Dependent identifications (foundation-core) | [`foundation-core.dependent-identifications`](foundation-core.dependent-identifications.md) | +| The fundamental theorem of identity types | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md) | +| Hexagons of identifications | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md) | +| Identity systems | [`foundation.identity-systems`](foundation.identity-systems.md) | +| The identity type (foundation) | [`foundation.identity-types`](foundation.identity-types.md) | +| The identity type (foundation-core) | [`foundation-core.identity-types`](foundation-core.identity-types.md) | +| Large identity types | [`foundation.large-identity-types`](foundation.large-identity-types.md) | +| Path algebra | [`foundation.path-algebra`](foundation.path-algebra.md) | +| Symmetric identity types | [`foundation.symmetric-identity-types`](foundation.symmetric-identity-types.md) | +| Torsorial type families | [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) | +| Transport along identifications (foundation) | [`foundation.transport-along-identifications`](foundation.transport-along-identifications.md) | +| Transport along identifications (foundation-core) | [`foundation-core.transport-along-identifications`](foundation-core.transport-along-identifications.md) | +| The universal property of identity types | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) | ## Definition diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md index 0e54842642..4351869f15 100644 --- a/src/foundation-core/propositions.lagda.md +++ b/src/foundation-core/propositions.lagda.md @@ -18,7 +18,7 @@ open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/singleton-induction.lagda.md b/src/foundation-core/singleton-induction.lagda.md index aa772e61a2..636f391214 100644 --- a/src/foundation-core/singleton-induction.lagda.md +++ b/src/foundation-core/singleton-induction.lagda.md @@ -16,7 +16,7 @@ open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.sections -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/small-types.lagda.md b/src/foundation-core/small-types.lagda.md index ec2e2c8072..a098c9dda4 100644 --- a/src/foundation-core/small-types.lagda.md +++ b/src/foundation-core/small-types.lagda.md @@ -15,7 +15,7 @@ open import foundation.logical-equivalences open import foundation.mere-equivalences open import foundation.propositional-truncations open import foundation.raising-universe-levels -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.univalence diff --git a/src/foundation-core/subtypes.lagda.md b/src/foundation-core/subtypes.lagda.md index 5ee7b28e79..316d695918 100644 --- a/src/foundation-core/subtypes.lagda.md +++ b/src/foundation-core/subtypes.lagda.md @@ -22,7 +22,7 @@ open import foundation-core.identity-types open import foundation-core.propositional-maps open import foundation-core.propositions open import foundation-core.sets -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import foundation-core.truncated-types open import foundation-core.truncation-levels ``` diff --git a/src/foundation-core/transport.lagda.md b/src/foundation-core/transport-along-identifications.lagda.md similarity index 89% rename from src/foundation-core/transport.lagda.md rename to src/foundation-core/transport-along-identifications.lagda.md index a39e2f1e21..176a78d957 100644 --- a/src/foundation-core/transport.lagda.md +++ b/src/foundation-core/transport-along-identifications.lagda.md @@ -1,7 +1,7 @@ -# Transport +# Transport along identifications ```agda -module foundation-core.transport where +module foundation-core.transport-along-identifications where ```
Imports @@ -22,7 +22,8 @@ element `b : B x`, we can **transport** the element `b` along the identification `p` to obtain an element `tr B p b : B y`. The fact that `tr B p` is an [equivalence](foundation-core.equivalences.md) is -recorded in [`foundation.transport`](foundation.transport.md). +recorded in +[`foundation.transport-along-identifications`](foundation.transport-along-identifications.md). ## Definition diff --git a/src/foundation-core/truncated-types.lagda.md b/src/foundation-core/truncated-types.lagda.md index 083ca3b4b2..bb510df533 100644 --- a/src/foundation-core/truncated-types.lagda.md +++ b/src/foundation-core/truncated-types.lagda.md @@ -22,7 +22,7 @@ open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.retractions -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import foundation-core.truncation-levels ``` diff --git a/src/foundation-core/univalence.lagda.md b/src/foundation-core/univalence.lagda.md index eb72470b0f..1192ecd6e2 100644 --- a/src/foundation-core/univalence.lagda.md +++ b/src/foundation-core/univalence.lagda.md @@ -16,7 +16,7 @@ open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ```
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index e6fdf16ce0..3868df37de 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -10,6 +10,8 @@ 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-families-over-subuniverses public +open import foundation.action-on-equivalences-functions 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 @@ -254,7 +256,8 @@ open import foundation.symmetric-identity-types public open import foundation.symmetric-operations public open import foundation.tight-apartness-relations public open import foundation.torsorial-type-families public -open import foundation.transport public +open import foundation.transport-along-equivalences public +open import foundation.transport-along-identifications public open import foundation.trivial-relaxed-sigma-decompositions public open import foundation.trivial-sigma-decompositions public open import foundation.truncated-equality public @@ -284,7 +287,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 diff --git a/src/foundation/univalence-action-on-equivalences.lagda.md b/src/foundation/action-on-equivalences-families-over-subuniverses.lagda.md similarity index 68% rename from src/foundation/univalence-action-on-equivalences.lagda.md rename to src/foundation/action-on-equivalences-families-over-subuniverses.lagda.md index cbf0b36566..fc3b20eb18 100644 --- a/src/foundation/univalence-action-on-equivalences.lagda.md +++ b/src/foundation/action-on-equivalences-families-over-subuniverses.lagda.md @@ -1,7 +1,7 @@ -# Univalent action on equivalences +# Action on equivalences in type families over subuniverses ```agda -module foundation.univalence-action-on-equivalences where +module foundation.action-on-equivalences-families-over-subuniverses where ```
Imports @@ -12,7 +12,7 @@ open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.sets open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels @@ -29,8 +29,10 @@ open import foundation-core.subtypes ## Ideas -Given a subuniverse `P`, any family of types `B` indexed by types of `P` has an -action on equivalences obtained by using the univalence axiom. +Given a [subuniverse](foundation.subuniverses.md) `P`, any family of types `B` +indexed by types of `P` has an +[action on equivalences](foundation.action-on-equivalences-functions.md) +obtained by using the [univalence axiom](foundation.univalence.md). ## Definition @@ -40,18 +42,19 @@ module _ ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3) where - univalent-action-equiv : + action-equiv-family-on-subuniverse : (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y - univalent-action-equiv X Y e = equiv-tr B (eq-equiv-subuniverse P e) + action-equiv-family-on-subuniverse X Y e = + equiv-tr B (eq-equiv-subuniverse P e) ``` ## Properties ```agda - preserves-id-equiv-univalent-action-equiv : + preserves-id-equiv-action-equiv-family-on-subuniverse : (X : type-subuniverse P) → - univalent-action-equiv X X id-equiv ＝ id-equiv - preserves-id-equiv-univalent-action-equiv X = + action-equiv-family-on-subuniverse X X id-equiv ＝ id-equiv + preserves-id-equiv-action-equiv-family-on-subuniverse X = ( ap (equiv-tr B) ( is-injective-map-equiv ( extensionality-subuniverse P X X) @@ -60,38 +63,41 @@ module _ ( id-equiv)))) ∙ ( equiv-tr-refl B) - Ind-univalent-action-path : + Ind-path-action-equiv-family-on-subuniverse : { l4 : Level} ( X : type-subuniverse P) ( F : (Y : type-subuniverse P) → B X ≃ B Y → UU l4) → F X id-equiv → ( Y : type-subuniverse P) (p : X ＝ Y) → F Y (equiv-tr B p) - Ind-univalent-action-path X F p .X refl = + Ind-path-action-equiv-family-on-subuniverse X F p .X refl = tr (F X) (inv (equiv-tr-refl B)) p - Ind-univalent-action-equiv : + Ind-action-equiv-family-on-subuniverse : { l4 : Level} ( X : type-subuniverse P) ( F : (Y : type-subuniverse P) → B X ≃ B Y → UU l4) → F X id-equiv → (Y : type-subuniverse P) (e : pr1 X ≃ pr1 Y) → - F Y (univalent-action-equiv X Y e) - Ind-univalent-action-equiv X F p Y e = - Ind-univalent-action-path X F p Y (eq-equiv-subuniverse P e) + F Y (action-equiv-family-on-subuniverse X Y e) + Ind-action-equiv-family-on-subuniverse X F p Y e = + Ind-path-action-equiv-family-on-subuniverse X F p Y + ( eq-equiv-subuniverse P e) - is-contr-preserves-id-action-equiv : + is-contr-preserves-id-action-equiv-family-on-subuniverse : ( (X : type-subuniverse P) → is-set (B X)) → is-contr ( Σ ( (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y) ( λ D → (X : type-subuniverse P) → D X X id-equiv ＝ id-equiv)) - pr1 (pr1 (is-contr-preserves-id-action-equiv H)) = univalent-action-equiv - pr2 (pr1 (is-contr-preserves-id-action-equiv H)) = - preserves-id-equiv-univalent-action-equiv - pr2 (is-contr-preserves-id-action-equiv H) (D , p) = + pr1 (pr1 (is-contr-preserves-id-action-equiv-family-on-subuniverse H)) = + action-equiv-family-on-subuniverse + pr2 (pr1 (is-contr-preserves-id-action-equiv-family-on-subuniverse H)) = + preserves-id-equiv-action-equiv-family-on-subuniverse + pr2 (is-contr-preserves-id-action-equiv-family-on-subuniverse H) (D , p) = eq-pair-Σ ( eq-htpy (λ X → eq-htpy (λ Y → eq-htpy (λ e → - lemma2 univalent-action-equiv D - (λ X → preserves-id-equiv-univalent-action-equiv X ∙ inv (p X)) + lemma2 action-equiv-family-on-subuniverse D + ( λ X → + preserves-id-equiv-action-equiv-family-on-subuniverse X ∙ inv (p X)) X Y e)))) ( eq-is-prop ( is-prop-Π diff --git a/src/foundation/action-on-equivalences-functions.lagda.md b/src/foundation/action-on-equivalences-functions.lagda.md new file mode 100644 index 0000000000..1fa32b1f30 --- /dev/null +++ b/src/foundation/action-on-equivalences-functions.lagda.md @@ -0,0 +1,162 @@ +# Action on equivalences of functions + +```agda +module foundation.action-on-equivalences-functions where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.equivalences +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.constant-maps +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +``` + +
+ +## Idea + +Applying the +[action on identifications](foundation.action-on-identifications-functions.md) +to [identifications](foundation-core.identity-types.md) arising from the +[univalence axiom](foundation.univalence.md) gives us the **action on +equivalences**. + +Alternatively, one can apply +[transport along identifications](foundation-core.transport-along-identifications.md) +to get +[transport along equivalences](foundation.transport-along-equivalences.md), but +luckily, these two notions coincide. + +## Definition + +```agda +action-equiv-function : + {l1 l2 : Level} {B : UU l2} (f : UU l1 → B) {X Y : UU l1} → + X ≃ Y → f X ＝ f Y +action-equiv-function f {X} {Y} e = ap f (eq-equiv X Y e) + +action-equiv-family : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + X ≃ Y → f X ≃ f Y +action-equiv-family f = equiv-eq ∘ action-equiv-function f + +map-action-equiv-family : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + X ≃ Y → f X → f Y +map-action-equiv-family f = map-equiv ∘ action-equiv-family f +``` + +## Properties + +### The identity function acts trivially on equivalences + +```agda +compute-action-equiv-family-id : + {l : Level} {X Y : UU l} (e : X ≃ Y) → (action-equiv-family id e) ＝ e +compute-action-equiv-family-id {l} {X} {Y} e = + (ap equiv-eq (ap-id (eq-equiv X Y e))) ∙ (is-section-eq-equiv e) +``` + +### The action on equivalences of a composite function is the composite of the actions + +```agda +distributive-action-equiv-function-comp : + {l1 l2 l3 : Level} {C : UU l3} (g : UU l2 → C) (f : UU l1 → UU l2) + {X Y : UU l1} → + action-equiv-function (g ∘ f) ~ + action-equiv-function g ∘ action-equiv-family f +distributive-action-equiv-function-comp g f {X} {Y} e = + ( ap-comp g f (eq-equiv X Y e)) ∙ + ( ap (ap g) (inv (is-retraction-eq-equiv (action-equiv-function f e)))) + +distributive-action-equiv-family-comp : + {l1 l2 l3 : Level} (g : UU l2 → UU l3) (f : UU l1 → UU l2) + {X Y : UU l1} → + action-equiv-family (g ∘ f) ~ + action-equiv-family g ∘ action-equiv-family f +distributive-action-equiv-family-comp g f {X} {Y} e = + ap equiv-eq (distributive-action-equiv-function-comp g f {X} {Y} e) +``` + +### The action on equivalences of any map preserves `id-equiv` + +```agda +compute-action-equiv-function-id-equiv : + {l1 l2 : Level} {B : UU l2} (f : UU l1 → B) (A : UU l1) → + (action-equiv-function f id-equiv) ＝ refl +compute-action-equiv-function-id-equiv f A = + ap (ap f) (compute-eq-equiv-id-equiv A) + +compute-action-equiv-family-id-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) (A : UU l1) → + (action-equiv-family f id-equiv) ＝ id-equiv +compute-action-equiv-family-id-equiv f A = + ap equiv-eq (compute-action-equiv-function-id-equiv f A) +``` + +### The action on equivalences of a constant map is constant + +```agda +compute-action-equiv-function-const : + {l1 l2 : Level} {B : UU l2} (b : B) {X Y : UU l1} + (e : X ≃ Y) → (action-equiv-function (const (UU l1) B b) e) ＝ refl +compute-action-equiv-function-const b {X} {Y} e = ap-const b (eq-equiv X Y e) + +compute-action-equiv-family-const : + {l1 l2 : Level} (B : UU l2) {X Y : UU l1} + (e : X ≃ Y) → (action-equiv-family (const (UU l1) (UU l2) B) e) ＝ id-equiv +compute-action-equiv-family-const B {X} {Y} e = + ap equiv-eq (compute-action-equiv-function-const B e) +``` + +### The action on equivalences of any map preserves composition of equivalences + +```agda +distributive-action-equiv-function-comp-equiv : + {l1 l2 : Level} {B : UU l2} (f : UU l1 → B) {X Y Z : UU l1} → + (e : X ≃ Y) (e' : Y ≃ Z) → + action-equiv-function f (e' ∘e e) ＝ + action-equiv-function f e ∙ action-equiv-function f e' +distributive-action-equiv-function-comp-equiv f {X} {Y} {Z} e e' = + ( ap (ap f) (inv (compute-eq-equiv-comp-equiv X Y Z e e'))) ∙ + ( ap-concat f (eq-equiv X Y e) (eq-equiv Y Z e')) + +distributive-action-equiv-family-comp-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y Z : UU l1} → + (e : X ≃ Y) (e' : Y ≃ Z) → + action-equiv-family f (e' ∘e e) ＝ + action-equiv-family f e' ∘e action-equiv-family f e +distributive-action-equiv-family-comp-equiv f e e' = + ( ap equiv-eq (distributive-action-equiv-function-comp-equiv f e e')) ∙ + ( inv + ( compute-equiv-eq-concat + ( action-equiv-function f e) + ( action-equiv-function f e'))) +``` + +### The action on equivalences of any map preserves inverses + +```agda +compute-action-equiv-function-inv-equiv : + {l1 l2 : Level} {B : UU l2} (f : UU l1 → B) {X Y : UU l1} + (e : X ≃ Y) → + action-equiv-function f (inv-equiv e) ＝ inv (action-equiv-function f e) +compute-action-equiv-function-inv-equiv f {X} {Y} e = + ( ap (ap f) (inv (commutativity-inv-eq-equiv X Y e))) ∙ + ( ap-inv f (eq-equiv X Y e)) + +compute-action-equiv-family-inv-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} + (e : X ≃ Y) → + action-equiv-family f (inv-equiv e) ＝ inv-equiv (action-equiv-family f e) +compute-action-equiv-family-inv-equiv f {X} {Y} e = + ( ap equiv-eq (compute-action-equiv-function-inv-equiv f e)) ∙ + ( inv (commutativity-inv-equiv-eq (f X) (f Y) (action-equiv-function f e))) +``` diff --git a/src/foundation/action-on-identifications-dependent-functions.lagda.md b/src/foundation/action-on-identifications-dependent-functions.lagda.md index e639d4d709..6db5aec11d 100644 --- a/src/foundation/action-on-identifications-dependent-functions.lagda.md +++ b/src/foundation/action-on-identifications-dependent-functions.lagda.md @@ -21,9 +21,9 @@ Given a dependent function `f : (x : A) → B x` and an [identification](foundation-core.identity-types.md) `p : x ＝ y` in `A`, we cannot directly compare the values `f x` and `f y`, since `f x` is an element of type `B x` while `f y` is an element of type `B y`. However, we can -[transport](foundation-core.transport.md) the value `f x` along `p` to obtain an -element of type `B y` that is comparable to the value `f y`. In other words, we -can consider the type of +[transport](foundation-core.transport-along-identifications.md) the value `f x` +along `p` to obtain an element of type `B y` that is comparable to the value +`f y`. In other words, we can consider the type of [dependent identifications](foundation-core.dependent-identifications.md) over `p` from `f x` to `f y`. The **dependent action on identifications** of `f` on `p` is a dependent identification diff --git a/src/foundation/action-on-identifications-functions.lagda.md b/src/foundation/action-on-identifications-functions.lagda.md index a270aa3f96..4fd28c92ed 100644 --- a/src/foundation/action-on-identifications-functions.lagda.md +++ b/src/foundation/action-on-identifications-functions.lagda.md @@ -12,7 +12,7 @@ open import foundation.universe-levels open import foundation-core.constant-maps open import foundation-core.function-types open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ```
@@ -46,7 +46,7 @@ ap-id : ap-id refl = refl ``` -### The action on identifications of a composite function is the composite of the actions on identifications +### The action on identifications of a composite function is the composite of the actions ```agda ap-comp : @@ -84,7 +84,7 @@ ap-concat-eq f p q .(p ∙ q) refl = ap-concat f p q ```agda ap-inv : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} - (p : x ＝ y) → (ap f (inv p)) ＝ (inv (ap f p)) + (p : x ＝ y) → ap f (inv p) ＝ inv (ap f p) ap-inv f refl = refl ``` diff --git a/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md b/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md index 5c05ab8072..ee7bbc9eb8 100644 --- a/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md +++ b/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md @@ -25,7 +25,7 @@ open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/arithmetic-law-product-and-pi-decompositions.lagda.md b/src/foundation/arithmetic-law-product-and-pi-decompositions.lagda.md index 021e304199..e15c29d921 100644 --- a/src/foundation/arithmetic-law-product-and-pi-decompositions.lagda.md +++ b/src/foundation/arithmetic-law-product-and-pi-decompositions.lagda.md @@ -25,7 +25,7 @@ open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/binary-transport.lagda.md b/src/foundation/binary-transport.lagda.md index 5de9ca3d4f..5ac3a40225 100644 --- a/src/foundation/binary-transport.lagda.md +++ b/src/foundation/binary-transport.lagda.md @@ -14,7 +14,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/cartesian-product-types.lagda.md b/src/foundation/cartesian-product-types.lagda.md index eefc3e3266..1c324495a7 100644 --- a/src/foundation/cartesian-product-types.lagda.md +++ b/src/foundation/cartesian-product-types.lagda.md @@ -14,7 +14,7 @@ open import foundation.subuniverses open import foundation.universe-levels open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/cones-over-cospans.lagda.md b/src/foundation/cones-over-cospans.lagda.md index 40e0417706..dcb1e94c20 100644 --- a/src/foundation/cones-over-cospans.lagda.md +++ b/src/foundation/cones-over-cospans.lagda.md @@ -18,7 +18,7 @@ open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/coproduct-decompositions.lagda.md b/src/foundation/coproduct-decompositions.lagda.md index e836a86eb1..179923170e 100644 --- a/src/foundation/coproduct-decompositions.lagda.md +++ b/src/foundation/coproduct-decompositions.lagda.md @@ -32,7 +32,7 @@ open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import univalent-combinatorics.equality-standard-finite-types open import univalent-combinatorics.standard-finite-types diff --git a/src/foundation/decidable-equality.lagda.md b/src/foundation/decidable-equality.lagda.md index 5be1de2683..c61914611a 100644 --- a/src/foundation/decidable-equality.lagda.md +++ b/src/foundation/decidable-equality.lagda.md @@ -28,7 +28,7 @@ open import foundation-core.injective-maps open import foundation-core.propositions open import foundation-core.retractions open import foundation-core.sets -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/decidable-equivalence-relations.lagda.md b/src/foundation/decidable-equivalence-relations.lagda.md index 91c206e11e..bb50065fb8 100644 --- a/src/foundation/decidable-equivalence-relations.lagda.md +++ b/src/foundation/decidable-equivalence-relations.lagda.md @@ -45,7 +45,7 @@ open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md index 12c92edd54..800ce600f6 100644 --- a/src/foundation/decidable-propositions.lagda.md +++ b/src/foundation/decidable-propositions.lagda.md @@ -34,7 +34,7 @@ open import foundation-core.propositions open import foundation-core.sets open import foundation-core.small-types open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import univalent-combinatorics.counting open import univalent-combinatorics.finite-types diff --git a/src/foundation/decidable-subtypes.lagda.md b/src/foundation/decidable-subtypes.lagda.md index ef938cc668..20472c465b 100644 --- a/src/foundation/decidable-subtypes.lagda.md +++ b/src/foundation/decidable-subtypes.lagda.md @@ -25,7 +25,7 @@ open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.injective-maps open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import foundation-core.truncated-types open import foundation-core.truncation-levels ``` diff --git a/src/foundation/dependent-binomial-theorem.lagda.md b/src/foundation/dependent-binomial-theorem.lagda.md index a502d6f2ef..e45ba02a02 100644 --- a/src/foundation/dependent-binomial-theorem.lagda.md +++ b/src/foundation/dependent-binomial-theorem.lagda.md @@ -14,7 +14,7 @@ open import foundation.dependent-pair-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-function-types open import foundation.raising-universe-levels -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-theoretic-principle-of-choice open import foundation.universal-property-coproduct-types open import foundation.universal-property-dependent-pair-types diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md index c94dc0698c..a2738f938a 100644 --- a/src/foundation/dependent-identifications.lagda.md +++ b/src/foundation/dependent-identifications.lagda.md @@ -10,7 +10,7 @@ open import foundation-core.dependent-identifications public ```agda open import foundation.dependent-pair-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.equivalences diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md index b956347b64..c62d92e0b0 100644 --- a/src/foundation/double-negation-modality.lagda.md +++ b/src/foundation/double-negation-modality.lagda.md @@ -12,7 +12,7 @@ open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators diff --git a/src/foundation/equality-cartesian-product-types.lagda.md b/src/foundation/equality-cartesian-product-types.lagda.md index e4bba6a073..04042db816 100644 --- a/src/foundation/equality-cartesian-product-types.lagda.md +++ b/src/foundation/equality-cartesian-product-types.lagda.md @@ -16,7 +16,7 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index 6398fdf073..4e3a6aae09 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -13,7 +13,7 @@ open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.dependent-identifications open import foundation.dependent-pair-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.function-types @@ -100,12 +100,12 @@ module _ {x y : X} (p : x ＝ y) → pair-eq-Σ (ap f p) ＝ ( ( ap (pr1 ∘ f) p) , - ( tr-subst B (pr1 ∘ f) p ∙ apd (λ x → pr2 (f x)) p)) + ( substitution-law-tr B (pr1 ∘ f) p ∙ apd (pr2 ∘ f) p)) pair-eq-Σ-ap refl = refl pr1-pair-eq-Σ-ap : {x y : X} (p : x ＝ y) → - pr1 (pair-eq-Σ (ap f p)) ＝ ap (λ x → pr1 (f x)) p + pr1 (pair-eq-Σ (ap f p)) ＝ ap (pr1 ∘ f) p pr1-pair-eq-Σ-ap refl = refl ``` diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md index 3d2de326e7..95464bc6a0 100644 --- a/src/foundation/equality-fibers-of-maps.lagda.md +++ b/src/foundation/equality-fibers-of-maps.lagda.md @@ -10,7 +10,7 @@ module foundation.equality-fibers-of-maps where 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 open import foundation.universe-levels open import foundation-core.equality-dependent-pair-types diff --git a/src/foundation/equivalence-relations.lagda.md b/src/foundation/equivalence-relations.lagda.md index d06d05ef3b..63a75e84f5 100644 --- a/src/foundation/equivalence-relations.lagda.md +++ b/src/foundation/equivalence-relations.lagda.md @@ -39,7 +39,7 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.sets -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/exclusive-disjunction.lagda.md b/src/foundation/exclusive-disjunction.lagda.md index e52f13f134..edb218f405 100644 --- a/src/foundation/exclusive-disjunction.lagda.md +++ b/src/foundation/exclusive-disjunction.lagda.md @@ -33,7 +33,7 @@ open import foundation-core.functoriality-dependent-function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import univalent-combinatorics.2-element-types open import univalent-combinatorics.equality-finite-types diff --git a/src/foundation/fiber-inclusions.lagda.md b/src/foundation/fiber-inclusions.lagda.md index 1c056ed907..391888d979 100644 --- a/src/foundation/fiber-inclusions.lagda.md +++ b/src/foundation/fiber-inclusions.lagda.md @@ -12,7 +12,7 @@ open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.faithful-maps open import foundation.fibers-of-maps -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universe-levels diff --git a/src/foundation/full-subtypes.lagda.md b/src/foundation/full-subtypes.lagda.md index da27a78574..57a9714080 100644 --- a/src/foundation/full-subtypes.lagda.md +++ b/src/foundation/full-subtypes.lagda.md @@ -16,7 +16,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.propositions open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/function-types.lagda.md b/src/foundation/function-types.lagda.md index a14e912eb0..cbafd7364a 100644 --- a/src/foundation/function-types.lagda.md +++ b/src/foundation/function-types.lagda.md @@ -16,7 +16,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/functoriality-coproduct-types.lagda.md b/src/foundation/functoriality-coproduct-types.lagda.md index 9a8b67cce7..a15dcf9bfc 100644 --- a/src/foundation/functoriality-coproduct-types.lagda.md +++ b/src/foundation/functoriality-coproduct-types.lagda.md @@ -35,7 +35,7 @@ open import foundation-core.identity-types open import foundation-core.injective-maps open import foundation-core.negation open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md index fd4fd354e3..992ba5daa3 100644 --- a/src/foundation/functoriality-dependent-function-types.lagda.md +++ b/src/foundation/functoriality-dependent-function-types.lagda.md @@ -14,7 +14,7 @@ open import foundation.dependent-pair-types open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.function-extensionality -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universal-property-unit-type open import foundation.universe-levels diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md index c13a0d0134..321df44322 100644 --- a/src/foundation/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation/functoriality-dependent-pair-types.lagda.md @@ -22,7 +22,7 @@ open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.pullbacks -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md index 79e6c497af..9603b06a46 100644 --- a/src/foundation/homotopies.lagda.md +++ b/src/foundation/homotopies.lagda.md @@ -24,7 +24,7 @@ open import foundation-core.function-types open import foundation-core.functoriality-dependent-function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.sections -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md index da6502913b..494a0cc6f6 100644 --- a/src/foundation/identity-systems.lagda.md +++ b/src/foundation/identity-systems.lagda.md @@ -16,7 +16,7 @@ open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.sections -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index c2a206f503..08c1deac5e 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -19,7 +19,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` @@ -37,27 +37,27 @@ is the least reflexive relation. The following table lists files that are about identity types and operations on identifications in arbitrary types. -| Concept | File | -| ------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------- | -| Action on identifications of binary functions | [`foundation.action-on-identifications-binary-functions`](foundation.action-on-identifications-binary-functions.md) | -| Action on identifications of dependent functions | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) | -| Action on identifications of functions | [`foundation.action-on-identifications-functions`](foundation.action-on-identifications-functions.md) | -| Binary transport | [`foundation.binary-transport`](foundation.binary-transport.md) | -| Commuting squares of identifications | [`foundation.commuting-squares-of-identifications`](foundation.commuting-squares-of-identifications.md) | -| Dependent identifications (foundation) | [`foundation.dependent-identifications`](foundation.dependent-identifications.md) | -| Dependent identifications (foundation-core) | [`foundation-core.dependent-identifications`](foundation-core.dependent-identifications.md) | -| The fundamental theorem of identity types | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md) | -| Hexagons of identifications | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md) | -| Identity systems | [`foundation.identity-systems`](foundation.identity-systems.md) | -| The identity type (foundation) | [`foundation.identity-types`](foundation.identity-types.md) | -| The identity type (foundation-core) | [`foundation-core.identity-types`](foundation-core.identity-types.md) | -| Large identity types | [`foundation.large-identity-types`](foundation.large-identity-types.md) | -| Path algebra | [`foundation.path-algebra`](foundation.path-algebra.md) | -| Symmetric identity types | [`foundation.symmetric-identity-types`](foundation.symmetric-identity-types.md) | -| Torsorial type families | [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) | -| Transport (foundation) | [`foundation.transport`](foundation.transport.md) | -| Transport (foundation-core) | [`foundation-core.transport`](foundation-core.transport.md) | -| The universal property of identity types | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) | +| Concept | File | +| ------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------- | +| Action on identifications of binary functions | [`foundation.action-on-identifications-binary-functions`](foundation.action-on-identifications-binary-functions.md) | +| Action on identifications of dependent functions | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) | +| Action on identifications of functions | [`foundation.action-on-identifications-functions`](foundation.action-on-identifications-functions.md) | +| Binary transport | [`foundation.binary-transport`](foundation.binary-transport.md) | +| Commuting squares of identifications | [`foundation.commuting-squares-of-identifications`](foundation.commuting-squares-of-identifications.md) | +| Dependent identifications (foundation) | [`foundation.dependent-identifications`](foundation.dependent-identifications.md) | +| Dependent identifications (foundation-core) | [`foundation-core.dependent-identifications`](foundation-core.dependent-identifications.md) | +| The fundamental theorem of identity types | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md) | +| Hexagons of identifications | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md) | +| Identity systems | [`foundation.identity-systems`](foundation.identity-systems.md) | +| The identity type (foundation) | [`foundation.identity-types`](foundation.identity-types.md) | +| The identity type (foundation-core) | [`foundation-core.identity-types`](foundation-core.identity-types.md) | +| Large identity types | [`foundation.large-identity-types`](foundation.large-identity-types.md) | +| Path algebra | [`foundation.path-algebra`](foundation.path-algebra.md) | +| Symmetric identity types | [`foundation.symmetric-identity-types`](foundation.symmetric-identity-types.md) | +| Torsorial type families | [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) | +| Transport along identifications (foundation) | [`foundation.transport-along-identifications`](foundation.transport-along-identifications.md) | +| Transport along identifications (foundation-core) | [`foundation-core.transport-along-identifications`](foundation-core.transport-along-identifications.md) | +| The universal property of identity types | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) | ## Properties diff --git a/src/foundation/induction-principle-propositional-truncation.lagda.md b/src/foundation/induction-principle-propositional-truncation.lagda.md index 803ab7d6a0..dafe752efa 100644 --- a/src/foundation/induction-principle-propositional-truncation.lagda.md +++ b/src/foundation/induction-principle-propositional-truncation.lagda.md @@ -12,7 +12,7 @@ open import foundation.universe-levels open import foundation-core.identity-types open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/isolated-points.lagda.md b/src/foundation/isolated-points.lagda.md index 9c4c806248..1ee694deca 100644 --- a/src/foundation/isolated-points.lagda.md +++ b/src/foundation/isolated-points.lagda.md @@ -35,7 +35,7 @@ open import foundation-core.injective-maps open import foundation-core.propositions open import foundation-core.sets open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/locally-small-types.lagda.md b/src/foundation/locally-small-types.lagda.md index dfcfb2b8d9..f16321383d 100644 --- a/src/foundation/locally-small-types.lagda.md +++ b/src/foundation/locally-small-types.lagda.md @@ -22,7 +22,7 @@ open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.small-types open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import foundation-core.truncated-types open import foundation-core.truncation-levels ``` diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md index ad50cd08da..a59314db2b 100644 --- a/src/foundation/partitions.lagda.md +++ b/src/foundation/partitions.lagda.md @@ -25,7 +25,7 @@ open import foundation.small-types open import foundation.subtype-identity-principle open import foundation.subtypes open import foundation.surjective-maps -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/foundation/perfect-images.lagda.md b/src/foundation/perfect-images.lagda.md index 35eb0ecba3..e05c373bc3 100644 --- a/src/foundation/perfect-images.lagda.md +++ b/src/foundation/perfect-images.lagda.md @@ -28,7 +28,7 @@ open import foundation-core.identity-types open import foundation-core.injective-maps open import foundation-core.propositional-maps open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/pointed-torsorial-type-families.lagda.md b/src/foundation/pointed-torsorial-type-families.lagda.md index ae36b9109a..2df25c9047 100644 --- a/src/foundation/pointed-torsorial-type-families.lagda.md +++ b/src/foundation/pointed-torsorial-type-families.lagda.md @@ -15,7 +15,7 @@ open import foundation.locally-small-types open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.sorial-type-families -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels diff --git a/src/foundation/products-unordered-pairs-of-types.lagda.md b/src/foundation/products-unordered-pairs-of-types.lagda.md index 01b4238bfb..5741e3ab94 100644 --- a/src/foundation/products-unordered-pairs-of-types.lagda.md +++ b/src/foundation/products-unordered-pairs-of-types.lagda.md @@ -11,7 +11,7 @@ open import foundation.dependent-pair-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-function-types open import foundation.symmetric-operations -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation.unordered-pairs open import foundation.unordered-pairs-of-types diff --git a/src/foundation/propositional-extensionality.lagda.md b/src/foundation/propositional-extensionality.lagda.md index b081d7b420..fcf3c588ce 100644 --- a/src/foundation/propositional-extensionality.lagda.md +++ b/src/foundation/propositional-extensionality.lagda.md @@ -15,7 +15,7 @@ open import foundation.logical-equivalences open import foundation.negation open import foundation.raising-universe-levels open import foundation.subtype-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.unit-type open import foundation.univalence diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 8342afce15..a202424801 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -23,7 +23,7 @@ open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.sets -open import foundation-core.transport +open import foundation-core.transport-along-identifications open import foundation-core.truncated-types open import foundation-core.truncation-levels ``` diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index ee18d81d39..a6de5dbca6 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -31,7 +31,7 @@ open import foundation-core.equality-dependent-pair-types open import foundation-core.function-types open import foundation-core.functoriality-dependent-function-types open import foundation-core.propositions -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/singleton-induction.lagda.md b/src/foundation/singleton-induction.lagda.md index 79b42d767f..ed4b0a5879 100644 --- a/src/foundation/singleton-induction.lagda.md +++ b/src/foundation/singleton-induction.lagda.md @@ -16,7 +16,7 @@ open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.sections -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/structure.lagda.md b/src/foundation/structure.lagda.md index 7010ef7209..8011baf8aa 100644 --- a/src/foundation/structure.lagda.md +++ b/src/foundation/structure.lagda.md @@ -14,7 +14,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/subuniverses.lagda.md b/src/foundation/subuniverses.lagda.md index 97f5866997..5c1d434904 100644 --- a/src/foundation/subuniverses.lagda.md +++ b/src/foundation/subuniverses.lagda.md @@ -20,7 +20,7 @@ open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/symmetric-difference.lagda.md b/src/foundation/symmetric-difference.lagda.md index 6ae37f58b1..6049da18de 100644 --- a/src/foundation/symmetric-difference.lagda.md +++ b/src/foundation/symmetric-difference.lagda.md @@ -21,7 +21,7 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.propositions open import foundation-core.subtypes -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/transport-along-equivalences.lagda.md b/src/foundation/transport-along-equivalences.lagda.md new file mode 100644 index 0000000000..ebf2304b5c --- /dev/null +++ b/src/foundation/transport-along-equivalences.lagda.md @@ -0,0 +1,195 @@ +# Transport along equivalences + +```agda +module foundation.transport-along-equivalences where +``` + +
Imports + +```agda +open import foundation.action-on-equivalences-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalence-extensionality +open import foundation.equivalence-induction +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.transport-along-identifications +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +``` + +
+ +## Idea + +Applying +[transport along identifications](foundation-core.transport-along-identifications.md) +to [identifications](foundation-core.identity-types.md) arising from the +[univalence axiom](foundation.univalence.md) gives us **transport along +equivalences**. + +Since transport defines [equivalences](foundation-core.equivalences.md) of +[fibers](foundation-core.fibers-of-maps.md), this gives us an _action on +equivalences_. Alternatively, we could apply the +[action on identifications](foundation.action-on-identifications-functions.md) +to get another +[action on equivalences](foundation.action-on-equivalences-functions.md), but +luckily, these two notions coincide. + +## Definition + +```agda +map-tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + X ≃ Y → f X → f Y +map-tr-equiv f {X} {Y} e = tr f (eq-equiv X Y e) + +is-equiv-map-tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} + (e : X ≃ Y) → is-equiv (map-tr-equiv f e) +is-equiv-map-tr-equiv f {X} {Y} e = is-equiv-tr f (eq-equiv X Y e) + +tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + X ≃ Y → f X ≃ f Y +pr1 (tr-equiv f e) = map-tr-equiv f e +pr2 (tr-equiv f e) = is-equiv-map-tr-equiv f e + +eq-tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + X ≃ Y → f X ＝ f Y +eq-tr-equiv f {X} {Y} = eq-equiv (f X) (f Y) ∘ tr-equiv f +``` + +### Transporting along `id-equiv` is the identity equivalence + +```agda +compute-map-tr-equiv-id-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X : UU l1} → + map-tr-equiv f id-equiv ＝ id +compute-map-tr-equiv-id-equiv f {X} = ap (tr f) (compute-eq-equiv-id-equiv X) + +compute-tr-equiv-id-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) {X : UU l1} → + tr-equiv f id-equiv ＝ id-equiv +compute-tr-equiv-id-equiv f {X} = + (ap (equiv-tr f) (compute-eq-equiv-id-equiv X)) ∙ (equiv-tr-refl f) +``` + +### Transport along equivalences preserves composition of equivalences + +```agda +distributive-map-tr-equiv-equiv-comp : + {l1 l2 : Level} (f : UU l1 → UU l2) + {X Y Z : UU l1} (e : X ≃ Y) (e' : Y ≃ Z) → + map-tr-equiv f (e' ∘e e) ~ (map-tr-equiv f e' ∘ map-tr-equiv f e) +distributive-map-tr-equiv-equiv-comp f {X} {Y} {Z} e e' x = + ( ap (λ p → tr f p x) (inv (compute-eq-equiv-comp-equiv X Y Z e e'))) ∙ + ( tr-concat (eq-equiv X Y e) (eq-equiv Y Z e') x) + +distributive-tr-equiv-equiv-comp : + {l1 l2 : Level} (f : UU l1 → UU l2) + {X Y Z : UU l1} (e : X ≃ Y) (e' : Y ≃ Z) → + tr-equiv f (e' ∘e e) ＝ (tr-equiv f e' ∘e tr-equiv f e) +distributive-tr-equiv-equiv-comp f {X} {Y} {Z} e e' = + eq-htpy-equiv (distributive-map-tr-equiv-equiv-comp f e e') +``` + +### Transporting along an equivalence and its inverse is just the identity + +```agda +is-section-map-tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) + {X Y : UU l1} (e : X ≃ Y) → + (map-tr-equiv f (inv-equiv e) ∘ map-tr-equiv f e) ~ id +is-section-map-tr-equiv f {X} {Y} e x = + ( ap + ( λ p → tr f p (map-tr-equiv f e x)) + ( inv (commutativity-inv-eq-equiv X Y e))) ∙ + ( is-retraction-inv-tr f (eq-equiv X Y e) x) + +is-retraction-map-tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) + {X Y : UU l1} (e : X ≃ Y) → + (map-tr-equiv f e ∘ map-tr-equiv f (inv-equiv e)) ~ id +is-retraction-map-tr-equiv f {X} {Y} e x = + ( ap + ( map-tr-equiv f e ∘ (λ p → tr f p x)) + ( inv (commutativity-inv-eq-equiv X Y e))) ∙ + ( is-section-inv-tr f (eq-equiv X Y e) x) +``` + +### Transposing transport along the inverse of an equivalence + +```agda +eq-transpose-map-tr-equiv : + {l1 l2 : Level} (f : UU l1 → UU l2) + {X Y : UU l1} (e : X ≃ Y) {u : f X} {v : f Y} → + v ＝ map-tr-equiv f e u → map-tr-equiv f (inv-equiv e) v ＝ u +eq-transpose-map-tr-equiv f e {u} p = + (ap (map-tr-equiv f (inv-equiv e)) p) ∙ (is-section-map-tr-equiv f e u) + +eq-transpose-map-tr-equiv' : + {l1 l2 : Level} (f : UU l1 → UU l2) + {X Y : UU l1} (e : X ≃ Y) {u : f X} {v : f Y} → + map-tr-equiv f e u ＝ v → u ＝ map-tr-equiv f (inv-equiv e) v +eq-transpose-map-tr-equiv' f e {u} p = + (inv (is-section-map-tr-equiv f e u)) ∙ (ap (map-tr-equiv f (inv-equiv e)) p) +``` + +### Substitution law for transport along equivalences + +```agda +substitution-map-tr-equiv : + {l1 l2 l3 : Level} (g : UU l2 → UU l3) (f : UU l1 → UU l2) {X Y : UU l1} + (e : X ≃ Y) → + map-tr-equiv g (action-equiv-family f e) ~ map-tr-equiv (g ∘ f) e +substitution-map-tr-equiv g f {X} {Y} e X' = + ( ap (λ p → tr g p X') (is-retraction-eq-equiv (action-equiv-function f e))) ∙ + ( substitution-law-tr g f (eq-equiv X Y e)) + +substitution-law-tr-equiv : + {l1 l2 l3 : Level} (g : UU l2 → UU l3) (f : UU l1 → UU l2) {X Y : UU l1} + (e : X ≃ Y) → tr-equiv g (action-equiv-family f e) ＝ tr-equiv (g ∘ f) e +substitution-law-tr-equiv g f e = + eq-htpy-equiv (substitution-map-tr-equiv g f e) +``` + +### Transporting along the action on equivalences of a function + +```agda +compute-map-tr-equiv-action-equiv-family : + {l1 l2 l3 l4 : Level} {B : UU l1 → UU l2} {D : UU l3 → UU l4} + (f : UU l1 → UU l3) (g : (X : UU l1) → B X → D (f X)) + {X Y : UU l1} (e : X ≃ Y) (X' : B X) → + map-tr-equiv D (action-equiv-family f e) (g X X') ＝ g Y (map-tr-equiv B e X') +compute-map-tr-equiv-action-equiv-family {D = D} f g {X} {Y} e X' = + ( ap + ( λ p → tr D p (g X X')) + ( is-retraction-eq-equiv (action-equiv-function f e))) ∙ + ( tr-ap f g (eq-equiv X Y e) X') +``` + +### Transport along equivalences and the action on equivalences in the universe coincide + +```agda +eq-tr-equiv-action-equiv-family : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + (e : X ≃ Y) → tr-equiv f e ＝ action-equiv-family f e +eq-tr-equiv-action-equiv-family f {X} = + ind-equiv X + ( λ Y e → tr-equiv f e ＝ action-equiv-family f e) + ( compute-tr-equiv-id-equiv f ∙ + inv (compute-action-equiv-family-id-equiv f X)) + +eq-map-tr-equiv-map-action-equiv-family : + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → + (e : X ≃ Y) → map-tr-equiv f e ＝ map-action-equiv-family f e +eq-map-tr-equiv-map-action-equiv-family f e = + ap map-equiv (eq-tr-equiv-action-equiv-family f e) +``` diff --git a/src/foundation/transport.lagda.md b/src/foundation/transport-along-identifications.lagda.md similarity index 90% rename from src/foundation/transport.lagda.md rename to src/foundation/transport-along-identifications.lagda.md index f1d2d9a9cb..7574aa5fe5 100644 --- a/src/foundation/transport.lagda.md +++ b/src/foundation/transport-along-identifications.lagda.md @@ -1,9 +1,9 @@ -# Transport +# Transport along identifications ```agda -module foundation.transport where +module foundation.transport-along-identifications where -open import foundation-core.transport public +open import foundation-core.transport-along-identifications public ```
Imports @@ -27,8 +27,9 @@ open import foundation-core.identity-types Given a type family `B` over `A`, an [identification](foundation-core.identity-types.md) `p : x ＝ y` in `A` and an -element `b : B x`, we can [**transport**](foundation-core.transport.md) the -element `b` along the identification `p` to obtain an element `tr B p b : B y`. +element `b : B x`, we can +[**transport**](foundation-core.transport-along-identifications.md) the element +`b` along the identification `p` to obtain an element `tr B p b : B y`. The fact that `tr B p` is an [equivalence](foundation-core.equivalences.md) is recorded in this file. @@ -66,10 +67,10 @@ module _ inv-tr : x ＝ y → B y → B x inv-tr p = tr B (inv p) - is-retraction-inv-tr : (p : x ＝ y) → ((inv-tr p) ∘ (tr B p)) ~ id + is-retraction-inv-tr : (p : x ＝ y) → (inv-tr p ∘ tr B p) ~ id is-retraction-inv-tr refl b = refl - is-section-inv-tr : (p : x ＝ y) → ((tr B p) ∘ (inv-tr p)) ~ id + is-section-inv-tr : (p : x ＝ y) → (tr B p ∘ inv-tr p) ~ id is-section-inv-tr refl b = refl is-equiv-tr : (p : x ＝ y) → is-equiv (tr B p) @@ -96,11 +97,11 @@ equiv-tr-refl B = refl ### Substitution law for transport ```agda -tr-subst : +substitution-law-tr : {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (B : A → UU l3) (f : X → A) {x y : X} (p : x ＝ y) {x' : B (f x)} → tr B (ap f p) x' ＝ tr (B ∘ f) p x' -tr-subst B f refl = refl +substitution-law-tr B f refl = refl ``` ### Coherences and algebraic identities for `tr²` diff --git a/src/foundation/type-theoretic-principle-of-choice.lagda.md b/src/foundation/type-theoretic-principle-of-choice.lagda.md index d463a83f92..95ed99731d 100644 --- a/src/foundation/type-theoretic-principle-of-choice.lagda.md +++ b/src/foundation/type-theoretic-principle-of-choice.lagda.md @@ -17,7 +17,7 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ```
diff --git a/src/foundation/univalence-implies-function-extensionality.lagda.md b/src/foundation/univalence-implies-function-extensionality.lagda.md index 893439fdd8..8380f86a8c 100644 --- a/src/foundation/univalence-implies-function-extensionality.lagda.md +++ b/src/foundation/univalence-implies-function-extensionality.lagda.md @@ -20,7 +20,7 @@ open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.transport +open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md index 57b8b5ba84..09cc2fddf1 100644 --- a/src/foundation/univalence.lagda.md +++ b/src/foundation/univalence.lagda.md @@ -143,18 +143,18 @@ eq-equiv-fam {B = B} {C} = map-inv-is-equiv (is-equiv-equiv-eq-fam B C) ### Computations with univalence ```agda -compute-equiv-eq : +compute-equiv-eq-concat : {l : Level} {A B C : UU l} (p : A ＝ B) (q : B ＝ C) → ((equiv-eq q) ∘e (equiv-eq p)) ＝ equiv-eq (p ∙ q) -compute-equiv-eq refl refl = eq-equiv-eq-map-equiv refl +compute-equiv-eq-concat refl refl = eq-equiv-eq-map-equiv refl -compute-eq-equiv : +compute-eq-equiv-comp-equiv : {l : Level} (A B C : UU l) (f : A ≃ B) (g : B ≃ C) → ((eq-equiv A B f) ∙ (eq-equiv B C g)) ＝ eq-equiv A C (g ∘e f) -compute-eq-equiv A B C f g = +compute-eq-equiv-comp-equiv A B C f g = is-injective-map-equiv ( equiv-univalence) - ( ( inv ( compute-equiv-eq (eq-equiv A B f) (eq-equiv B C g))) ∙ + ( ( inv ( compute-equiv-eq-concat (eq-equiv A B f) (eq-equiv B C g))) ∙ ( ( ap ( λ e → (map-equiv e g) ∘e (equiv-eq (eq-equiv A B f))) ( right-inverse-law-equiv equiv-univalence)) ∙ diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md index 5d2e7960cc..8297c1c7a7 100644 --- a/src/foundation/univalent-type-families.lagda.md +++ b/src/foundation/univalent-type-families.lagda.md @@ -7,7 +7,7 @@ module foundation.univalent-type-families where
Imports ```agda -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.equivalences diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index 6f57b0faf3..e1a7bdc62e 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -14,7 +14,7 @@ open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.slice open import foundation.surjective-maps -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.contractible-maps diff --git a/src/foundation/universal-property-set-quotients.lagda.md b/src/foundation/universal-property-set-quotients.lagda.md index 57a6363862..c6f5f29b9a 100644 --- a/src/foundation/universal-property-set-quotients.lagda.md +++ b/src/foundation/universal-property-set-quotients.lagda.md @@ -25,7 +25,7 @@ open import foundation.propositional-truncations open import foundation.reflecting-maps-equivalence-relations open import foundation.sets open import foundation.surjective-maps -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universal-property-image open import foundation.universe-levels @@ -426,11 +426,11 @@ module _ α : Σ (A → Prop l2) (reflects-Equivalence-Relation R) α = pair ( prop-Equivalence-Relation R x) - ( λ r → - eq-iff - ( transitive-Equivalence-Relation R _ _ _ r) - ( transitive-Equivalence-Relation R _ _ _ - ( symmetric-Equivalence-Relation R _ _ r))) + ( λ r → + eq-iff + ( transitive-Equivalence-Relation R _ _ _ r) + ( transitive-Equivalence-Relation R _ _ _ + ( symmetric-Equivalence-Relation R _ _ r))) P : type-Set B → Prop l2 P = map-inv-is-equiv (Q (Prop-Set l2)) α compute-P : @@ -460,7 +460,7 @@ module _ ( reflects-map-reflecting-map-Equivalence-Relation R q ( map-inv-equiv ( compute-P (pr1 v)) - ( inv-tr (λ b → type-Prop (P b)) (pr2 v) p))) ∙ + ( inv-tr (type-Prop ∘ P) (pr2 v) p))) ∙ ( pr2 v))) is-contr-total-P : is-contr (Σ (type-Set B) (λ b → type-Prop (P b))) is-contr-total-P = pair center-total-P contraction-total-P diff --git a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md index 309e845787..74009d5e07 100644 --- a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md +++ b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md @@ -17,7 +17,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import graph-theory.enriched-undirected-graphs diff --git a/src/graph-theory/equivalences-undirected-graphs.lagda.md b/src/graph-theory/equivalences-undirected-graphs.lagda.md index 9384fb8e0b..8b5f0a65af 100644 --- a/src/graph-theory/equivalences-undirected-graphs.lagda.md +++ b/src/graph-theory/equivalences-undirected-graphs.lagda.md @@ -20,7 +20,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels open import foundation.unordered-pairs diff --git a/src/graph-theory/fibers-directed-graphs.lagda.md b/src/graph-theory/fibers-directed-graphs.lagda.md index 2325a19107..3b7917dec1 100644 --- a/src/graph-theory/fibers-directed-graphs.lagda.md +++ b/src/graph-theory/fibers-directed-graphs.lagda.md @@ -14,7 +14,7 @@ open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/graph-theory/morphisms-undirected-graphs.lagda.md b/src/graph-theory/morphisms-undirected-graphs.lagda.md index 99a555ded8..1989176172 100644 --- a/src/graph-theory/morphisms-undirected-graphs.lagda.md +++ b/src/graph-theory/morphisms-undirected-graphs.lagda.md @@ -19,7 +19,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation.unordered-pairs diff --git a/src/graph-theory/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md index cab82a2c23..f7b5cbd8f5 100644 --- a/src/graph-theory/undirected-graphs.lagda.md +++ b/src/graph-theory/undirected-graphs.lagda.md @@ -10,7 +10,7 @@ module graph-theory.undirected-graphs where open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation.unordered-pairs diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md index aaa002c9ce..ba9655d22f 100644 --- a/src/graph-theory/walks-directed-graphs.lagda.md +++ b/src/graph-theory/walks-directed-graphs.lagda.md @@ -24,7 +24,7 @@ open import foundation.identity-types open import foundation.injective-maps open import foundation.negation open import foundation.raising-universe-levels -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import graph-theory.directed-graphs diff --git a/src/group-theory/concrete-group-actions.lagda.md b/src/group-theory/concrete-group-actions.lagda.md index bc5108da26..fe407ed17e 100644 --- a/src/group-theory/concrete-group-actions.lagda.md +++ b/src/group-theory/concrete-group-actions.lagda.md @@ -9,7 +9,7 @@ module group-theory.concrete-group-actions where ```agda open import foundation.function-types open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.concrete-groups diff --git a/src/group-theory/homomorphisms-concrete-group-actions.lagda.md b/src/group-theory/homomorphisms-concrete-group-actions.lagda.md index b86eae7b09..62057b8e87 100644 --- a/src/group-theory/homomorphisms-concrete-group-actions.lagda.md +++ b/src/group-theory/homomorphisms-concrete-group-actions.lagda.md @@ -16,7 +16,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.concrete-group-actions diff --git a/src/group-theory/loop-groups-sets.lagda.md b/src/group-theory/loop-groups-sets.lagda.md index 88d3ea96c6..75f9b3f857 100644 --- a/src/group-theory/loop-groups-sets.lagda.md +++ b/src/group-theory/loop-groups-sets.lagda.md @@ -120,7 +120,7 @@ module _ map-hom-symmetric-group-loop-group-Set X X pr2 hom-symmetric-group-loop-group-Set p q = ( ap equiv-eq (distributive-inv-concat p q)) ∙ - ( inv (compute-equiv-eq (inv q) (inv p))) + ( inv (compute-equiv-eq-concat (inv q) (inv p))) hom-inv-symmetric-group-loop-group-Set : type-hom-Group (symmetric-Group X) (loop-group-Set X) @@ -129,7 +129,9 @@ module _ pr2 hom-inv-symmetric-group-loop-group-Set f g = ( ap ( inv) - ( inv (compute-eq-equiv (type-Set X) (type-Set X) (type-Set X) g f))) ∙ + ( inv + ( compute-eq-equiv-comp-equiv + ( type-Set X) (type-Set X) (type-Set X) g f))) ∙ ( distributive-inv-concat ( eq-equiv (type-Set X) (type-Set X) g) ( eq-equiv (type-Set X) (type-Set X) f)) diff --git a/src/group-theory/normal-subgroups.lagda.md b/src/group-theory/normal-subgroups.lagda.md index e15991d6ce..83ab47f2a5 100644 --- a/src/group-theory/normal-subgroups.lagda.md +++ b/src/group-theory/normal-subgroups.lagda.md @@ -20,7 +20,7 @@ open import foundation.large-binary-relations open import foundation.propositions open import foundation.subtype-identity-principle open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.congruence-relations-groups diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md index ce8d9ca758..9b5cac7222 100644 --- a/src/group-theory/subgroups.lagda.md +++ b/src/group-theory/subgroups.lagda.md @@ -25,7 +25,7 @@ open import foundation.propositions open import foundation.sets open import foundation.subtype-identity-principle open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.groups diff --git a/src/group-theory/torsors.lagda.md b/src/group-theory/torsors.lagda.md index ef5005aa18..80d946b9c0 100644 --- a/src/group-theory/torsors.lagda.md +++ b/src/group-theory/torsors.lagda.md @@ -21,7 +21,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtype-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.concrete-groups diff --git a/src/group-theory/transitive-concrete-group-actions.lagda.md b/src/group-theory/transitive-concrete-group-actions.lagda.md index dd3eac590f..2d589c0391 100644 --- a/src/group-theory/transitive-concrete-group-actions.lagda.md +++ b/src/group-theory/transitive-concrete-group-actions.lagda.md @@ -21,7 +21,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.concrete-group-actions diff --git a/src/higher-group-theory/higher-group-actions.lagda.md b/src/higher-group-theory/higher-group-actions.lagda.md index 3e339c1a9f..92a3590986 100644 --- a/src/higher-group-theory/higher-group-actions.lagda.md +++ b/src/higher-group-theory/higher-group-actions.lagda.md @@ -8,7 +8,7 @@ module higher-group-theory.higher-group-actions where ```agda open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import higher-group-theory.higher-groups diff --git a/src/higher-group-theory/homomorphisms-higher-group-actions.lagda.md b/src/higher-group-theory/homomorphisms-higher-group-actions.lagda.md index 6d2ee91be6..5929ab0dbc 100644 --- a/src/higher-group-theory/homomorphisms-higher-group-actions.lagda.md +++ b/src/higher-group-theory/homomorphisms-higher-group-actions.lagda.md @@ -12,7 +12,7 @@ open import foundation.equivalences open import foundation.function-extensionality open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import higher-group-theory.higher-group-actions diff --git a/src/linear-algebra/vectors.lagda.md b/src/linear-algebra/vectors.lagda.md index 991d0a620a..ae492a1cef 100644 --- a/src/linear-algebra/vectors.lagda.md +++ b/src/linear-algebra/vectors.lagda.md @@ -21,7 +21,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.raising-universe-levels open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.unit-type diff --git a/src/lists/functoriality-lists.lagda.md b/src/lists/functoriality-lists.lagda.md index 62b9b8f9c9..fe70813734 100644 --- a/src/lists/functoriality-lists.lagda.md +++ b/src/lists/functoriality-lists.lagda.md @@ -16,7 +16,7 @@ open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import linear-algebra.functoriality-vectors diff --git a/src/lists/permutation-lists.lagda.md b/src/lists/permutation-lists.lagda.md index 32fb571f8d..875d7f1700 100644 --- a/src/lists/permutation-lists.lagda.md +++ b/src/lists/permutation-lists.lagda.md @@ -16,7 +16,7 @@ open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import linear-algebra.functoriality-vectors diff --git a/src/lists/permutation-vectors.lagda.md b/src/lists/permutation-vectors.lagda.md index 16572742fd..ae8d72e68a 100644 --- a/src/lists/permutation-vectors.lagda.md +++ b/src/lists/permutation-vectors.lagda.md @@ -22,7 +22,7 @@ open import foundation.function-types open import foundation.functoriality-coproduct-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 linear-algebra.functoriality-vectors diff --git a/src/lists/sort-by-insertion-vectors.lagda.md b/src/lists/sort-by-insertion-vectors.lagda.md index 2f9c6c74e3..6f756f9386 100644 --- a/src/lists/sort-by-insertion-vectors.lagda.md +++ b/src/lists/sort-by-insertion-vectors.lagda.md @@ -18,7 +18,7 @@ open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functoriality-coproduct-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/order-theory/finitely-graded-posets.lagda.md b/src/order-theory/finitely-graded-posets.lagda.md index 2b684e743a..7534d942df 100644 --- a/src/order-theory/finitely-graded-posets.lagda.md +++ b/src/order-theory/finitely-graded-posets.lagda.md @@ -24,7 +24,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/organic-chemistry/ethane.lagda.md b/src/organic-chemistry/ethane.lagda.md index 74afce7451..a284da7eff 100644 --- a/src/organic-chemistry/ethane.lagda.md +++ b/src/organic-chemistry/ethane.lagda.md @@ -23,7 +23,7 @@ open import foundation.identity-types open import foundation.injective-maps open import foundation.propositional-truncations open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels open import foundation.unordered-pairs diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md index aabd238396..adab6dcfbc 100644 --- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md @@ -26,7 +26,7 @@ open import foundation.monomorphisms open import foundation.propositions open import foundation.sets open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.type-arithmetic-dependent-pair-types diff --git a/src/orthogonal-factorization-systems/function-classes.lagda.md b/src/orthogonal-factorization-systems/function-classes.lagda.md index 56e789dbf9..9c30c83a67 100644 --- a/src/orthogonal-factorization-systems/function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/function-classes.lagda.md @@ -14,7 +14,7 @@ open import foundation.function-types open import foundation.identity-types open import foundation.propositions open import foundation.pullback-squares -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels ``` diff --git a/src/orthogonal-factorization-systems/local-families.lagda.md b/src/orthogonal-factorization-systems/local-families.lagda.md index eeea9e9704..fa92bac793 100644 --- a/src/orthogonal-factorization-systems/local-families.lagda.md +++ b/src/orthogonal-factorization-systems/local-families.lagda.md @@ -23,7 +23,7 @@ open import foundation.identity-types open import foundation.propositions open import foundation.retractions open import foundation.sections -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-function-types open import foundation.type-arithmetic-unit-type open import foundation.unit-type diff --git a/src/orthogonal-factorization-systems/local-maps.lagda.md b/src/orthogonal-factorization-systems/local-maps.lagda.md index cf854ead40..14a6b71b46 100644 --- a/src/orthogonal-factorization-systems/local-maps.lagda.md +++ b/src/orthogonal-factorization-systems/local-maps.lagda.md @@ -23,7 +23,7 @@ open import foundation.identity-types open import foundation.propositions open import foundation.retractions open import foundation.sections -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-function-types open import foundation.type-arithmetic-unit-type open import foundation.unit-type diff --git a/src/orthogonal-factorization-systems/open-modalities.lagda.md b/src/orthogonal-factorization-systems/open-modalities.lagda.md index 5e1ffc17e0..45a170fa4c 100644 --- a/src/orthogonal-factorization-systems/open-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/open-modalities.lagda.md @@ -14,7 +14,7 @@ open import foundation.function-extensionality open import foundation.identity-types open import foundation.locally-small-types open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import orthogonal-factorization-systems.higher-modalities diff --git a/src/polytopes/abstract-polytopes.lagda.md b/src/polytopes/abstract-polytopes.lagda.md index 02b69a6446..a490cdeffd 100644 --- a/src/polytopes/abstract-polytopes.lagda.md +++ b/src/polytopes/abstract-polytopes.lagda.md @@ -17,7 +17,7 @@ open import foundation.identity-types open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels diff --git a/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md index e550494571..9350b7af52 100644 --- a/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md +++ b/src/ring-theory/ideals-generated-by-subsets-rings.lagda.md @@ -17,7 +17,7 @@ open import foundation.logical-equivalences open import foundation.powersets open import foundation.propositional-truncations open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.unions-subtypes open import foundation.universe-levels diff --git a/src/ring-theory/integer-multiples-of-elements-rings.lagda.md b/src/ring-theory/integer-multiples-of-elements-rings.lagda.md index 6dae1f60d1..5f2d652de3 100644 --- a/src/ring-theory/integer-multiples-of-elements-rings.lagda.md +++ b/src/ring-theory/integer-multiples-of-elements-rings.lagda.md @@ -15,7 +15,7 @@ open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions open import foundation.coproduct-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/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md index 8ae0db4466..2eebe34272 100644 --- a/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md +++ b/src/ring-theory/left-ideals-generated-by-subsets-rings.lagda.md @@ -18,7 +18,7 @@ open import foundation.powersets 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.unions-subtypes open import foundation.universe-levels diff --git a/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md b/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md index c0819f3d2f..38d5ceeffb 100644 --- a/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md +++ b/src/ring-theory/right-ideals-generated-by-subsets-rings.lagda.md @@ -18,7 +18,7 @@ open import foundation.powersets 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.unions-subtypes open import foundation.universe-levels diff --git a/src/set-theory/cumulative-hierarchy.lagda.md b/src/set-theory/cumulative-hierarchy.lagda.md index a499a76770..6ce0932a89 100644 --- a/src/set-theory/cumulative-hierarchy.lagda.md +++ b/src/set-theory/cumulative-hierarchy.lagda.md @@ -27,7 +27,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.raising-universe-levels open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.unit-type open import foundation.universe-levels diff --git a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md index 8ddb767df3..3a83b52b38 100644 --- a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md +++ b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md @@ -22,7 +22,7 @@ open import foundation.relaxed-sigma-decompositions open import foundation.sigma-closed-subuniverses open import foundation.sigma-decomposition-subuniverse open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice diff --git a/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md index fd7f92f200..f308e753bc 100644 --- a/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md +++ b/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md @@ -22,7 +22,7 @@ open import foundation.relaxed-sigma-decompositions open import foundation.sigma-closed-subuniverses open import foundation.sigma-decomposition-subuniverse open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.unit-type open import foundation.univalence diff --git a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md index 9c146364e4..03ad6b59e3 100644 --- a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md +++ b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md @@ -20,7 +20,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-dependent-pair-types diff --git a/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md b/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md index 6cc067707a..d581585b1f 100644 --- a/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md +++ b/src/species/dirichlet-exponentials-species-of-types-in-subuniverses.lagda.md @@ -20,7 +20,7 @@ open import foundation.pi-decompositions-subuniverse open import foundation.product-decompositions open import foundation.propositions open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.univalence open import foundation.universe-levels diff --git a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md index 6a966673f9..71bdd90718 100644 --- a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md +++ b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md @@ -19,7 +19,7 @@ open import foundation.product-decompositions open import foundation.product-decompositions-subuniverse open import foundation.propositions open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type diff --git a/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md index 11c167bc6e..f848a96a4f 100644 --- a/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md +++ b/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md @@ -22,7 +22,7 @@ open import foundation.sigma-closed-subuniverses open import foundation.sigma-decomposition-subuniverse open import foundation.small-types open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice diff --git a/src/species/species-of-types-in-subuniverses.lagda.md b/src/species/species-of-types-in-subuniverses.lagda.md index 890975d154..1ef1c85fec 100644 --- a/src/species/species-of-types-in-subuniverses.lagda.md +++ b/src/species/species-of-types-in-subuniverses.lagda.md @@ -13,7 +13,7 @@ open import foundation.equivalences open import foundation.function-types open import foundation.propositions open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/species/species-of-types.lagda.md b/src/species/species-of-types.lagda.md index 585fc15a8c..ceb687541f 100644 --- a/src/species/species-of-types.lagda.md +++ b/src/species/species-of-types.lagda.md @@ -9,7 +9,7 @@ module species.species-of-types where ```agda open import foundation.cartesian-product-types open import foundation.equivalences -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels ``` diff --git a/src/structured-types/pointed-maps.lagda.md b/src/structured-types/pointed-maps.lagda.md index 76986cc813..ec9b8563f6 100644 --- a/src/structured-types/pointed-maps.lagda.md +++ b/src/structured-types/pointed-maps.lagda.md @@ -13,7 +13,7 @@ open import foundation.constant-maps 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 open import structured-types.pointed-dependent-functions diff --git a/src/synthetic-homotopy-theory/26-descent.lagda.md b/src/synthetic-homotopy-theory/26-descent.lagda.md index 0db3a07d53..b5f0f3c13d 100644 --- a/src/synthetic-homotopy-theory/26-descent.lagda.md +++ b/src/synthetic-homotopy-theory/26-descent.lagda.md @@ -30,7 +30,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.pullbacks open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-theoretic-principle-of-choice open import foundation.univalence open import foundation.universe-levels diff --git a/src/synthetic-homotopy-theory/26-id-pushout.lagda.md b/src/synthetic-homotopy-theory/26-id-pushout.lagda.md index dd8365d954..1b7e25ccc4 100644 --- a/src/synthetic-homotopy-theory/26-id-pushout.lagda.md +++ b/src/synthetic-homotopy-theory/26-id-pushout.lagda.md @@ -22,7 +22,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universal-property-identity-types open import foundation.universe-levels diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index b33a747e72..71067c794a 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -16,7 +16,7 @@ open import foundation.identity-types open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import structured-types.pointed-types diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md index 1c6f3f5ea4..fd04ca5e1f 100644 --- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md @@ -19,7 +19,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans diff --git a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md index 96775f12df..2017650ebe 100644 --- a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md @@ -12,7 +12,7 @@ open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.pullbacks -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md index 5eebd4008d..a2096ced2b 100644 --- a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md @@ -24,7 +24,7 @@ open import foundation.identity-systems open import foundation.identity-types open import foundation.injective-maps open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md index c59d13aae4..073a8f2feb 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md @@ -20,7 +20,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.pullbacks -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md index d3bca48c18..fd85921d9e 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md @@ -23,7 +23,7 @@ open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md b/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md index 15f9bbe907..4a56bcd36b 100644 --- a/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md @@ -17,7 +17,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-function-types open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.descent-circle diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md index 0c85533f60..a99bdc3c45 100644 --- a/src/synthetic-homotopy-theory/descent-circle.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md @@ -25,7 +25,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels @@ -121,8 +121,8 @@ module _ ### Canonical descent data for a family over the circle A type family over the circle gives rise to its canonical descent data, obtained -by evaluation at `base` and [transporting](foundation-core.transport.md) along -`loop`. +by evaluation at `base` and +[transporting](foundation-core.transport-along-identifications.md) along `loop`. ```agda ev-descent-data-circle : diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index e8a9010429..0280f9eac0 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -11,7 +11,7 @@ open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types open import foundation.function-types open import foundation.functoriality-dependent-pair-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans diff --git a/src/synthetic-homotopy-theory/free-loops.lagda.md b/src/synthetic-homotopy-theory/free-loops.lagda.md index 5e83bb9173..9fe6f480e3 100644 --- a/src/synthetic-homotopy-theory/free-loops.lagda.md +++ b/src/synthetic-homotopy-theory/free-loops.lagda.md @@ -16,7 +16,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels ``` diff --git a/src/synthetic-homotopy-theory/interval-type.lagda.md b/src/synthetic-homotopy-theory/interval-type.lagda.md index 52c072070b..1492581343 100644 --- a/src/synthetic-homotopy-theory/interval-type.lagda.md +++ b/src/synthetic-homotopy-theory/interval-type.lagda.md @@ -15,7 +15,7 @@ open import foundation.equivalences open import foundation.function-extensionality open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels ``` diff --git a/src/synthetic-homotopy-theory/multiplication-circle.lagda.md b/src/synthetic-homotopy-theory/multiplication-circle.lagda.md index 4fb8d2102a..9e1ac9c52c 100644 --- a/src/synthetic-homotopy-theory/multiplication-circle.lagda.md +++ b/src/synthetic-homotopy-theory/multiplication-circle.lagda.md @@ -13,7 +13,7 @@ open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import structured-types.pointed-homotopies diff --git a/src/synthetic-homotopy-theory/sections-descent-circle.lagda.md b/src/synthetic-homotopy-theory/sections-descent-circle.lagda.md index e1d3cac8c3..6db8ae32e0 100644 --- a/src/synthetic-homotopy-theory/sections-descent-circle.lagda.md +++ b/src/synthetic-homotopy-theory/sections-descent-circle.lagda.md @@ -23,7 +23,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.path-algebra -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.descent-circle diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md index 58cf49bf18..51084e96be 100644 --- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md @@ -25,7 +25,7 @@ open import foundation.identity-systems open import foundation.identity-types open import foundation.injective-maps open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/synthetic-homotopy-theory/suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-pointed-types.lagda.md index af23cf6315..66d7735858 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-pointed-types.lagda.md @@ -23,7 +23,7 @@ open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 8779ed0686..517d08df40 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -24,7 +24,7 @@ open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 5c424520d6..940f31faf7 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -28,7 +28,8 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.raising-universe-levels open import foundation.sets -open import foundation.transport +open import foundation.structure-identity-principle +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.universe-levels diff --git a/src/synthetic-homotopy-theory/universal-property-circle.lagda.md b/src/synthetic-homotopy-theory/universal-property-circle.lagda.md index 71abc58f61..769e039acb 100644 --- a/src/synthetic-homotopy-theory/universal-property-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-circle.lagda.md @@ -22,7 +22,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.sections -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.free-loops diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md index 5379230ecb..aa892fc08a 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md @@ -23,7 +23,7 @@ open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md index 77cd4006aa..6974a7afa2 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md @@ -23,7 +23,7 @@ open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type diff --git a/src/trees/bases-directed-trees.lagda.md b/src/trees/bases-directed-trees.lagda.md index fa49199117..62493b1ade 100644 --- a/src/trees/bases-directed-trees.lagda.md +++ b/src/trees/bases-directed-trees.lagda.md @@ -21,7 +21,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.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-empty-type open import foundation.universe-levels diff --git a/src/trees/directed-trees.lagda.md b/src/trees/directed-trees.lagda.md index 8c72d592d4..629fb4c5bb 100644 --- a/src/trees/directed-trees.lagda.md +++ b/src/trees/directed-trees.lagda.md @@ -25,7 +25,7 @@ open import foundation.isolated-points open import foundation.negation 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-dependent-pair-types open import foundation.type-arithmetic-empty-type diff --git a/src/trees/elementhood-relation-w-types.lagda.md b/src/trees/elementhood-relation-w-types.lagda.md index 4205e542be..df5c81a9b4 100644 --- a/src/trees/elementhood-relation-w-types.lagda.md +++ b/src/trees/elementhood-relation-w-types.lagda.md @@ -10,7 +10,7 @@ module trees.elementhood-relation-w-types where 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 open import trees.elementhood-relation-coalgebras-polynomial-endofunctors diff --git a/src/trees/enriched-directed-trees.lagda.md b/src/trees/enriched-directed-trees.lagda.md index 57fbf3744d..570286771d 100644 --- a/src/trees/enriched-directed-trees.lagda.md +++ b/src/trees/enriched-directed-trees.lagda.md @@ -20,7 +20,7 @@ open import foundation.identity-types open import foundation.isolated-points open import foundation.negation open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import graph-theory.directed-graphs diff --git a/src/trees/equivalences-directed-trees.lagda.md b/src/trees/equivalences-directed-trees.lagda.md index 89badad851..c508da1874 100644 --- a/src/trees/equivalences-directed-trees.lagda.md +++ b/src/trees/equivalences-directed-trees.lagda.md @@ -19,7 +19,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.subtype-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import graph-theory.equivalences-directed-graphs diff --git a/src/trees/equivalences-enriched-directed-trees.lagda.md b/src/trees/equivalences-enriched-directed-trees.lagda.md index e24e0e65d7..c796443d76 100644 --- a/src/trees/equivalences-enriched-directed-trees.lagda.md +++ b/src/trees/equivalences-enriched-directed-trees.lagda.md @@ -20,7 +20,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.enriched-directed-trees diff --git a/src/trees/extensional-w-types.lagda.md b/src/trees/extensional-w-types.lagda.md index d53f7b4c1a..3a8887dc5d 100644 --- a/src/trees/extensional-w-types.lagda.md +++ b/src/trees/extensional-w-types.lagda.md @@ -22,7 +22,7 @@ open import foundation.identity-types open import foundation.propositional-truncations open import foundation.propositions open import foundation.slice -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalent-type-families open import foundation.universe-levels diff --git a/src/trees/functoriality-combinator-directed-trees.lagda.md b/src/trees/functoriality-combinator-directed-trees.lagda.md index b181907762..62ecdf2b9c 100644 --- a/src/trees/functoriality-combinator-directed-trees.lagda.md +++ b/src/trees/functoriality-combinator-directed-trees.lagda.md @@ -14,7 +14,7 @@ open import foundation.dependent-pair-types open import foundation.function-types open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.combinator-directed-trees diff --git a/src/trees/functoriality-w-types.lagda.md b/src/trees/functoriality-w-types.lagda.md index d2327b6b22..6a32e1a93e 100644 --- a/src/trees/functoriality-w-types.lagda.md +++ b/src/trees/functoriality-w-types.lagda.md @@ -19,7 +19,7 @@ open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositional-maps -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.truncated-maps open import foundation.truncated-types open import foundation.truncation-levels diff --git a/src/trees/induction-w-types.lagda.md b/src/trees/induction-w-types.lagda.md index bf924b6e13..1805b55311 100644 --- a/src/trees/induction-w-types.lagda.md +++ b/src/trees/induction-w-types.lagda.md @@ -15,7 +15,7 @@ open import foundation.function-extensionality open import foundation.function-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 trees.elementhood-relation-w-types diff --git a/src/trees/morphisms-directed-trees.lagda.md b/src/trees/morphisms-directed-trees.lagda.md index f4cb1d987a..eea276a027 100644 --- a/src/trees/morphisms-directed-trees.lagda.md +++ b/src/trees/morphisms-directed-trees.lagda.md @@ -17,7 +17,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.negation -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-empty-type open import foundation.universe-levels diff --git a/src/trees/morphisms-enriched-directed-trees.lagda.md b/src/trees/morphisms-enriched-directed-trees.lagda.md index ea3167e9b1..c6618ae770 100644 --- a/src/trees/morphisms-enriched-directed-trees.lagda.md +++ b/src/trees/morphisms-enriched-directed-trees.lagda.md @@ -14,7 +14,7 @@ open import foundation.dependent-pair-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.enriched-directed-trees diff --git a/src/trees/polynomial-endofunctors.lagda.md b/src/trees/polynomial-endofunctors.lagda.md index 96be64542a..d2d8d3280d 100644 --- a/src/trees/polynomial-endofunctors.lagda.md +++ b/src/trees/polynomial-endofunctors.lagda.md @@ -16,7 +16,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels ``` diff --git a/src/trees/ranks-of-elements-w-types.lagda.md b/src/trees/ranks-of-elements-w-types.lagda.md index 4ef53cb626..1efe2269d1 100644 --- a/src/trees/ranks-of-elements-w-types.lagda.md +++ b/src/trees/ranks-of-elements-w-types.lagda.md @@ -15,7 +15,7 @@ open import foundation.identity-types open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.elementhood-relation-w-types diff --git a/src/trees/rooted-morphisms-directed-trees.lagda.md b/src/trees/rooted-morphisms-directed-trees.lagda.md index 2b46217d61..aad2dd69aa 100644 --- a/src/trees/rooted-morphisms-directed-trees.lagda.md +++ b/src/trees/rooted-morphisms-directed-trees.lagda.md @@ -18,7 +18,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.subtype-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.bases-directed-trees diff --git a/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md b/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md index 1836a44f6d..f876ff518a 100644 --- a/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md +++ b/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md @@ -12,7 +12,7 @@ open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.enriched-directed-trees diff --git a/src/trees/small-multisets.lagda.md b/src/trees/small-multisets.lagda.md index 3388a2abad..33175f9ad2 100644 --- a/src/trees/small-multisets.lagda.md +++ b/src/trees/small-multisets.lagda.md @@ -18,7 +18,7 @@ open import foundation.identity-types open import foundation.propositions open import foundation.small-types open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels diff --git a/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md b/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md index 9b9453ec89..0c7f181af9 100644 --- a/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md +++ b/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md @@ -23,7 +23,7 @@ open import foundation.identity-types open import foundation.isolated-points open import foundation.negation open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-empty-type open import foundation.universe-levels diff --git a/src/trees/underlying-trees-of-elements-of-w-types.lagda.md b/src/trees/underlying-trees-of-elements-of-w-types.lagda.md index 2a196afe79..6579f766cd 100644 --- a/src/trees/underlying-trees-of-elements-of-w-types.lagda.md +++ b/src/trees/underlying-trees-of-elements-of-w-types.lagda.md @@ -19,7 +19,7 @@ open import foundation.identity-types open import foundation.isolated-points open import foundation.negation open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import graph-theory.directed-graphs diff --git a/src/trees/undirected-trees.lagda.md b/src/trees/undirected-trees.lagda.md index 539065d90d..b9317cfec2 100644 --- a/src/trees/undirected-trees.lagda.md +++ b/src/trees/undirected-trees.lagda.md @@ -20,7 +20,7 @@ open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import graph-theory.paths-undirected-graphs diff --git a/src/trees/universal-multiset.lagda.md b/src/trees/universal-multiset.lagda.md index 126ca1365c..274f1dfe83 100644 --- a/src/trees/universal-multiset.lagda.md +++ b/src/trees/universal-multiset.lagda.md @@ -13,7 +13,7 @@ open import foundation.identity-types open import foundation.raising-universe-levels open import foundation.small-types open import foundation.small-universes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import trees.functoriality-w-types diff --git a/src/trees/w-types.lagda.md b/src/trees/w-types.lagda.md index 76777c1305..eeae83e192 100644 --- a/src/trees/w-types.lagda.md +++ b/src/trees/w-types.lagda.md @@ -19,7 +19,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.propositional-truncations open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.type-theoretic-principle-of-choice diff --git a/src/type-theories/dependent-type-theories.lagda.md b/src/type-theories/dependent-type-theories.lagda.md index 9fb662749e..3c9f43e8b1 100644 --- a/src/type-theories/dependent-type-theories.lagda.md +++ b/src/type-theories/dependent-type-theories.lagda.md @@ -17,7 +17,7 @@ open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels ``` diff --git a/src/type-theories/fibered-dependent-type-theories.lagda.md b/src/type-theories/fibered-dependent-type-theories.lagda.md index fef7eb8f07..a5da36d53a 100644 --- a/src/type-theories/fibered-dependent-type-theories.lagda.md +++ b/src/type-theories/fibered-dependent-type-theories.lagda.md @@ -13,7 +13,7 @@ open import foundation.action-on-identifications-functions 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 open import type-theories.dependent-type-theories diff --git a/src/type-theories/sections-dependent-type-theories.lagda.md b/src/type-theories/sections-dependent-type-theories.lagda.md index 57a5c18782..339dc4c6e7 100644 --- a/src/type-theories/sections-dependent-type-theories.lagda.md +++ b/src/type-theories/sections-dependent-type-theories.lagda.md @@ -10,7 +10,7 @@ module type-theories.sections-dependent-type-theories where ```agda open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import type-theories.dependent-type-theories diff --git a/src/type-theories/simple-type-theories.lagda.md b/src/type-theories/simple-type-theories.lagda.md index 227dc224ff..98461a1a5e 100644 --- a/src/type-theories/simple-type-theories.lagda.md +++ b/src/type-theories/simple-type-theories.lagda.md @@ -13,7 +13,7 @@ open import foundation.action-on-identifications-functions open import foundation.function-types open import foundation.homotopies open import foundation.identity-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels ``` diff --git a/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md b/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md index 4f925227c3..335deed2c7 100644 --- a/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md @@ -34,7 +34,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.univalence open import foundation.universe-levels diff --git a/src/univalent-combinatorics/2-element-subtypes.lagda.md b/src/univalent-combinatorics/2-element-subtypes.lagda.md index 5ba14b8c22..d41430d2f4 100644 --- a/src/univalent-combinatorics/2-element-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-subtypes.lagda.md @@ -24,7 +24,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-coproduct-types open import foundation.unit-type open import foundation.universe-levels diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index ae036a1d18..68e6cf1568 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -37,7 +37,7 @@ open import foundation.propositions open import foundation.raising-universe-levels open import foundation.sets open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-empty-type diff --git a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md index 7da51e828b..a6e6581dd9 100644 --- a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md @@ -26,7 +26,7 @@ open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.sections -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-unit-type diff --git a/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md b/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md index f916a53857..a93706de19 100644 --- a/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md +++ b/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md @@ -22,7 +22,7 @@ open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types open import foundation.iterated-cartesian-product-types -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels diff --git a/src/univalent-combinatorics/decidable-subtypes.lagda.md b/src/univalent-combinatorics/decidable-subtypes.lagda.md index 90a64f18aa..66b79ec69f 100644 --- a/src/univalent-combinatorics/decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/decidable-subtypes.lagda.md @@ -22,7 +22,7 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import univalent-combinatorics.decidable-dependent-pair-types diff --git a/src/univalent-combinatorics/dependent-pair-types.lagda.md b/src/univalent-combinatorics/dependent-pair-types.lagda.md index cf8877984e..f0e9351cf6 100644 --- a/src/univalent-combinatorics/dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/dependent-pair-types.lagda.md @@ -25,7 +25,7 @@ open import foundation.propositions open import foundation.sections open import foundation.sets 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-dependent-pair-types open import foundation.universe-levels diff --git a/src/univalent-combinatorics/equivalences-cubes.lagda.md b/src/univalent-combinatorics/equivalences-cubes.lagda.md index 89f968dd7a..f71497fe95 100644 --- a/src/univalent-combinatorics/equivalences-cubes.lagda.md +++ b/src/univalent-combinatorics/equivalences-cubes.lagda.md @@ -19,7 +19,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.universe-levels open import univalent-combinatorics.cubes diff --git a/src/univalent-combinatorics/fibers-of-maps.lagda.md b/src/univalent-combinatorics/fibers-of-maps.lagda.md index 1e80f22eaa..1779e20173 100644 --- a/src/univalent-combinatorics/fibers-of-maps.lagda.md +++ b/src/univalent-combinatorics/fibers-of-maps.lagda.md @@ -21,7 +21,7 @@ open import foundation.identity-types open import foundation.propositional-truncations open import foundation.propositions open import foundation.sections -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index 2791564474..4fa2bac999 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -32,7 +32,7 @@ open import foundation.raising-universe-levels open import foundation.sets open import foundation.subtypes open import foundation.subuniverses -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-empty-type open import foundation.unit-type diff --git a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md index c964610d74..97718030aa 100644 --- a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md +++ b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md @@ -48,7 +48,7 @@ open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels diff --git a/src/univalent-combinatorics/pi-finite-types.lagda.md b/src/univalent-combinatorics/pi-finite-types.lagda.md index d2bbfc548b..1ee3a422e5 100644 --- a/src/univalent-combinatorics/pi-finite-types.lagda.md +++ b/src/univalent-combinatorics/pi-finite-types.lagda.md @@ -46,7 +46,7 @@ open import foundation.set-truncations open import foundation.sets open import foundation.subtypes open import foundation.surjective-maps -open import foundation.transport +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.type-arithmetic-coproduct-types diff --git a/src/universal-algebra/terms-over-signatures.lagda.md b/src/universal-algebra/terms-over-signatures.lagda.md index 48f19c048d..8a5cf6febf 100644 --- a/src/universal-algebra/terms-over-signatures.lagda.md +++ b/src/universal-algebra/terms-over-signatures.lagda.md @@ -14,7 +14,7 @@ open import foundation.action-on-identifications-functions 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.unit-type open import foundation.universe-levels