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 5c0505d499..7a1ba6b3a1 100644 --- a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md @@ -17,7 +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-equivalences-type-families-over-subuniverses open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types @@ -29,6 +29,7 @@ open import foundation.negation open import foundation.propositional-truncations open import foundation.raising-universe-levels open import foundation.transport-along-identifications +open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type open import foundation.universe-levels @@ -69,7 +70,7 @@ module _ ( star) ( transposition Y)) ( map-equiv - ( action-equiv-family-on-subuniverse + ( action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( orientation-Complete-Undirected-Graph (n +ℕ 2)) ( raise l (Fin (n +ℕ 2)) , @@ -110,17 +111,19 @@ module _ preserves-id-equiv-orientation-complete-undirected-graph-equiv ( n +ℕ 2)} { y = - ( action-equiv-family-on-subuniverse + ( action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( orientation-Complete-Undirected-Graph (n +ℕ 2))) , - ( preserves-id-equiv-action-equiv-family-on-subuniverse + ( compute-id-equiv-action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( orientation-Complete-Undirected-Graph (n +ℕ 2)))} ( eq-is-contr - ( 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))))) + ( is-contr-equiv' _ + ( distributive-Π-Σ) + ( is-contr-Π + ( unique-action-equiv-family-over-subuniverse + ( mere-equiv-Prop (Fin (n +ℕ 2))) + ( orientation-Complete-Undirected-Graph (n +ℕ 2))))))) ( not-even-difference-orientation-aut-transposition-count (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star)) diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index 5e28858730..0df76282fe 100644 --- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md @@ -18,8 +18,9 @@ open import finite-group-theory.permutations open import finite-group-theory.sign-homomorphism open import finite-group-theory.transpositions -open import foundation.action-on-equivalences-families-over-subuniverses +open import foundation.action-on-equivalences-type-families-over-subuniverses open import foundation.action-on-identifications-functions +open import foundation.binary-transport open import foundation.commuting-squares-of-maps open import foundation.contractible-types open import foundation.coproduct-types @@ -31,6 +32,7 @@ open import foundation.empty-types open import foundation.equality-dependent-pair-types open import foundation.equivalence-classes open import foundation.equivalence-extensionality +open import foundation.equivalence-induction open import foundation.equivalence-relations open import foundation.equivalences open import foundation.function-extensionality @@ -129,7 +131,7 @@ module _ unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2)))) ( quotient-aut-succ-succ-Fin n (transposition Y)) ( map-equiv - ( action-equiv-family-on-subuniverse + ( action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( D (n +ℕ 2)) ( raise l1 (Fin (n +ℕ 2)) , @@ -146,9 +148,8 @@ module _ eq-counting-equivalence-class-R : (n : ℕ) → - Id - ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) - ( raise (l2 ⊔ lsuc l3) (Fin 2)) + equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2))) ＝ + raise (l2 ⊔ lsuc l3) (Fin 2) eq-counting-equivalence-class-R n = eq-equiv ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2)))) @@ -165,34 +166,57 @@ 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 = - action-equiv-family-on-subuniverse (mere-equiv-Prop (Fin n)) (D n) + action-equiv-family-over-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-action-equiv-family-on-subuniverse + compute-id-equiv-action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin n)) ( D n) - preserves-R-invertible-action-D-equiv : - ( n : ℕ) → - ( X X' : UU-Fin l1 n) - ( e : type-UU-Fin n X ≃ type-UU-Fin n X') → - ( a a' : D n X) → - ( sim-Equivalence-Relation (R n X) a a' ↔ - sim-Equivalence-Relation - ( R n X') - ( map-equiv (invertible-action-D-equiv n X X' e) a) - ( map-equiv (invertible-action-D-equiv n X X' e) a')) - preserves-R-invertible-action-D-equiv n X X' = - Ind-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' ↔ - sim-Equivalence-Relation (R n Y) (map-equiv f a) (map-equiv f a'))) - ( λ a a' → id , id) - ( X') + abstract + preserves-R-invertible-action-D-equiv : + ( n : ℕ) → + ( X X' : UU-Fin l1 n) + ( e : type-UU-Fin n X ≃ type-UU-Fin n X') → + ( a a' : D n X) → + ( sim-Equivalence-Relation (R n X) a a' ↔ + sim-Equivalence-Relation + ( R n X') + ( map-equiv (invertible-action-D-equiv n X X' e) a) + ( map-equiv (invertible-action-D-equiv n X X' e) a')) + preserves-R-invertible-action-D-equiv n X = + ind-equiv-subuniverse + ( mere-equiv-Prop (Fin n)) + ( X) + ( λ Y f → + ( a a' : D n X) → + ( sim-Equivalence-Relation (R n X) a a' ↔ + sim-Equivalence-Relation + ( R n Y) + ( map-equiv (invertible-action-D-equiv n X Y f) a) + ( map-equiv (invertible-action-D-equiv n X Y f) a'))) + ( λ a a' → + ( binary-tr + ( sim-Equivalence-Relation (R n X)) + ( inv + ( htpy-eq-equiv + ( preserves-id-equiv-invertible-action-D-equiv n X) + ( a))) + ( inv + ( htpy-eq-equiv + ( preserves-id-equiv-invertible-action-D-equiv n X) + ( a')))) , + ( binary-tr + ( sim-Equivalence-Relation (R n X)) + ( htpy-eq-equiv + ( preserves-id-equiv-invertible-action-D-equiv n X) + ( a)) + ( htpy-eq-equiv + ( preserves-id-equiv-invertible-action-D-equiv n X) + ( a')))) raise-UU-Fin-Fin : (n : ℕ) → UU-Fin l1 n pr1 (raise-UU-Fin-Fin n) = raise l1 (Fin n) @@ -1490,7 +1514,7 @@ module _ unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) → ¬ ( x ＝ ( map-equiv - ( action-equiv-family-on-subuniverse + ( action-equiv-family-over-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/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md index f85e3e3227..7a90598c0b 100644 --- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md @@ -21,7 +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-equivalences-type-families-over-subuniverses open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.coproduct-types @@ -43,6 +43,7 @@ open import foundation.propositional-truncations open import foundation.raising-universe-levels open import foundation.sets open import foundation.transport-along-identifications +open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type open import foundation.universe-levels @@ -683,7 +684,7 @@ module _ unit-trunc-Prop (compute-raise-Fin l (n +ℕ 2)))) ( sign-comp-aut-succ-succ-Fin n (transposition Y)) ( map-equiv - ( action-equiv-family-on-subuniverse + ( action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( λ X → Fin (n +ℕ 2) ≃ pr1 X) ( raise l (Fin (n +ℕ 2)) , @@ -716,20 +717,19 @@ module _ simpson-comp-equiv (n +ℕ 2) , preserves-id-equiv-simpson-comp-equiv (n +ℕ 2)} { y = - ( action-equiv-family-on-subuniverse + ( action-equiv-family-over-subuniverse ( mere-equiv-Prop (Fin (n +ℕ 2))) ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) , - ( preserves-id-equiv-action-equiv-family-on-subuniverse + ( compute-id-equiv-action-equiv-family-over-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-family-on-subuniverse - ( mere-equiv-Prop (Fin (n +ℕ 2))) - ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) - ( λ X → - is-set-equiv-is-set - ( is-set-Fin (n +ℕ 2)) - ( is-set-type-UU-Fin (n +ℕ 2) X))))) + ( is-contr-equiv' _ + ( distributive-Π-Σ) + ( is-contr-Π + ( unique-action-equiv-family-over-subuniverse + ( mere-equiv-Prop (Fin (n +ℕ 2))) + ( λ Y → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) Y)))))) ( not-sign-comp-transposition-count (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star)) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 8096470e1a..606923be30 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -10,8 +10,10 @@ 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-equivalences-functions-out-of-subuniverses public +open import foundation.action-on-equivalences-type-families public +open import foundation.action-on-equivalences-type-families-over-subuniverses 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 @@ -251,6 +253,7 @@ open import foundation.subtype-identity-principle public open import foundation.subtypes public open import foundation.subuniverses public open import foundation.surjective-maps public +open import foundation.symmetric-binary-relations public open import foundation.symmetric-difference public open import foundation.symmetric-identity-types public open import foundation.symmetric-operations public @@ -295,6 +298,7 @@ open import foundation.universal-property-coproduct-types public open import foundation.universal-property-dependent-pair-types public open import foundation.universal-property-empty-type public open import foundation.universal-property-fiber-products public +open import foundation.universal-property-identity-systems public open import foundation.universal-property-identity-types public open import foundation.universal-property-image public open import foundation.universal-property-maybe public diff --git a/src/foundation/action-on-equivalences-families-over-subuniverses.lagda.md b/src/foundation/action-on-equivalences-families-over-subuniverses.lagda.md deleted file mode 100644 index fc3b20eb18..0000000000 --- a/src/foundation/action-on-equivalences-families-over-subuniverses.lagda.md +++ /dev/null @@ -1,144 +0,0 @@ -# Action on equivalences in type families over subuniverses - -```agda -module foundation.action-on-equivalences-families-over-subuniverses where -``` - -
Imports - -```agda -open import foundation.action-on-identifications-functions -open import foundation.dependent-pair-types -open import foundation.function-extensionality -open import foundation.sets -open import foundation.subuniverses -open import foundation.transport-along-identifications -open import foundation.univalence -open import foundation.universe-levels - -open import foundation-core.contractible-types -open import foundation-core.equality-dependent-pair-types -open import foundation-core.equivalences -open import foundation-core.identity-types -open import foundation-core.injective-maps -open import foundation-core.propositions -open import foundation-core.subtypes -``` - -
- -## Ideas - -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 - -```agda -module _ - { l1 l2 l3 : Level} - ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3) - where - - action-equiv-family-on-subuniverse : - (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y - action-equiv-family-on-subuniverse X Y e = - equiv-tr B (eq-equiv-subuniverse P e) -``` - -## Properties - -```agda - preserves-id-equiv-action-equiv-family-on-subuniverse : - (X : type-subuniverse P) → - 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) - ( is-section-map-inv-is-equiv - ( is-equiv-equiv-eq-subuniverse P X X) - ( id-equiv)))) ∙ - ( equiv-tr-refl B) - - 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-path-action-equiv-family-on-subuniverse X F p .X refl = - tr (F X) (inv (equiv-tr-refl B)) p - - 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 (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-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-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 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-Π - ( λ X → - is-set-type-Set - ( B X ≃ B X , is-set-equiv-is-set (H X) (H X)) - ( D X X id-equiv) - ( id-equiv)))) - where - lemma1 : - (f g : (X Y : UU l1) → (pX : is-in-subuniverse P X) → - ( pY : is-in-subuniverse P Y) → X ＝ Y → - B (X , pX) ≃ B (Y , pY)) → - ( (X : UU l1) (pX : is-in-subuniverse P X) - (pX' : is-in-subuniverse P X) → - f X X pX pX' refl ＝ g X X pX pX' refl) → - ( X Y : UU l1) (pX : is-in-subuniverse P X) - ( pY : is-in-subuniverse P Y) (p : X ＝ Y) → - f X Y pX pY p ＝ g X Y pX pY p - lemma1 f g h X .X pX pX' refl = h X pX pX' - lemma2 : - ( f g : (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y) → - ( (X : type-subuniverse P) → f X X id-equiv ＝ g X X id-equiv) → - ( X Y : type-subuniverse P) (e : pr1 X ≃ pr1 Y) → - f X Y e ＝ g X Y e - lemma2 f g h X Y e = - tr - ( λ e' → f X Y e' ＝ g X Y e') - ( is-section-map-inv-is-equiv (univalence (pr1 X) (pr1 Y)) e) - ( lemma1 - ( λ X Y pX pY p → f (X , pX) (Y , pY) (equiv-eq p)) - ( λ X Y pX pY p → g (X , pX) (Y , pY) (equiv-eq p)) - ( λ X pX pX' → - tr - ( λ p → f (X , pX) (X , p) id-equiv ＝ - g (X , pX) (X , p) id-equiv) - ( eq-is-prop (is-prop-is-in-subtype P X)) - ( h ( X , pX))) - ( pr1 X) - ( pr1 Y) - ( pr2 X) - ( pr2 Y) - ( eq-equiv (pr1 X) (pr1 Y) e)) -``` diff --git a/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md b/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md new file mode 100644 index 0000000000..e1ce00fc21 --- /dev/null +++ b/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md @@ -0,0 +1,77 @@ +# The action on equivalences of functions out of subuniverses + +```agda +module foundation.action-on-equivalences-functions-out-of-subuniverses where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalence-induction +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.subuniverses +open import foundation.universe-levels +``` + +
+ +## Idea + +Consider a [subuniverse](foundation.subuniverses.md) `P` of `𝒰` and a map +`f : P → B` from the subuniverse `P` into some type `B`. Then `f` has an +**action on equivalences** + +```text + (X ≃ Y) → (f X ＝ f Y) +``` + +which is uniquely determined by the +[identification](foundation-core.identity-types.md) +`action-equiv f id-equiv ＝ refl`. The action on equivalences fits in a +[commuting square](foundation.commuting-squares-of-maps.md) of maps + +```text + ap f + (X = Y) ---------------> (f X = f Y) + | | + equiv-eq | | id + V V + (X ≃ Y) ---------------> (f X = f Y) + action-equiv f +``` + +## Definitions + +```agda +module _ + {l1 l2 l3 : Level} (P : subuniverse l1 l2) + {B : UU l3} (f : type-subuniverse P → B) + where + + abstract + unique-action-equiv-function-subuniverse : + (X : type-subuniverse P) → + is-contr + ( Σ ( (Y : type-subuniverse P) → equiv-subuniverse P X Y → f X ＝ f Y) + ( λ h → h X id-equiv ＝ refl)) + unique-action-equiv-function-subuniverse X = + is-contr-map-ev-id-equiv-subuniverse P X + ( λ Y e → f X ＝ f Y) + ( refl) + + action-equiv-function-subuniverse : + (X Y : type-subuniverse P) → equiv-subuniverse P X Y → f X ＝ f Y + action-equiv-function-subuniverse X Y = + ap f ∘ eq-equiv-subuniverse P + + compute-action-equiv-function-subuniverse-id-equiv : + (X : type-subuniverse P) → + action-equiv-function-subuniverse X X id-equiv ＝ refl + compute-action-equiv-function-subuniverse-id-equiv X = + ap (ap f) (compute-eq-equiv-id-equiv-subuniverse P) +``` diff --git a/src/foundation/action-on-equivalences-functions.lagda.md b/src/foundation/action-on-equivalences-functions.lagda.md index 1fa32b1f30..704c34b224 100644 --- a/src/foundation/action-on-equivalences-functions.lagda.md +++ b/src/foundation/action-on-equivalences-functions.lagda.md @@ -8,13 +8,14 @@ module foundation.action-on-equivalences-functions where ```agda open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalence-induction 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 ``` @@ -37,70 +38,32 @@ 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 +module _ + {l1 l2 : Level} {B : UU l2} (f : UU l1 → B) + where + + abstract + unique-action-equiv-function : + (X : UU l1) → + is-contr + ( Σ ((Y : UU l1) → X ≃ Y → f X ＝ f Y) (λ h → h X id-equiv ＝ refl)) + unique-action-equiv-function X = + is-contr-map-ev-id-equiv + ( λ Y e → f X ＝ f Y) + ( refl) + + action-equiv-function : + {X Y : UU l1} → X ≃ Y → f X ＝ f Y + action-equiv-function {X} {Y} e = ap f (eq-equiv X Y e) + + compute-action-equiv-function-id-equiv : + (X : UU l1) → action-equiv-function id-equiv ＝ refl + compute-action-equiv-function-id-equiv X = + ap (ap f) (compute-eq-equiv-id-equiv X) ``` ## 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 @@ -108,12 +71,6 @@ 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 @@ -127,18 +84,6 @@ distributive-action-equiv-function-comp-equiv : 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 @@ -151,12 +96,4 @@ compute-action-equiv-function-inv-equiv : 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-equivalences-type-families-over-subuniverses.lagda.md b/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md new file mode 100644 index 0000000000..8d9235e946 --- /dev/null +++ b/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md @@ -0,0 +1,95 @@ +# Action on equivalences in type families over subuniverses + +```agda +module foundation.action-on-equivalences-type-families-over-subuniverses where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.equivalence-induction +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.subuniverses +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.equivalences +open import foundation-core.identity-types +``` + +
+ +## Ideas + +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). + +## Definitions + +### The action on equivalences of a family of types over a subuniverse + +```agda +module _ + { l1 l2 l3 : Level} + ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3) + where + + abstract + unique-action-equiv-family-over-subuniverse : + (X : type-subuniverse P) → + is-contr + ( fiber (ev-id-equiv-subuniverse P X {λ Y e → B X ≃ B Y}) id-equiv) + unique-action-equiv-family-over-subuniverse X = + is-contr-map-ev-id-equiv-subuniverse P X (λ Y e → B X ≃ B Y) id-equiv + + action-equiv-family-over-subuniverse : + (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y + action-equiv-family-over-subuniverse X Y = + equiv-eq ∘ ap B ∘ eq-equiv-subuniverse P + + compute-id-equiv-action-equiv-family-over-subuniverse : + (X : type-subuniverse P) → + action-equiv-family-over-subuniverse X X id-equiv ＝ id-equiv + compute-id-equiv-action-equiv-family-over-subuniverse X = + ap (equiv-eq ∘ ap B) (compute-eq-equiv-id-equiv-subuniverse P) +``` + +## Properties + +### The action on equivalences of a family of types over a subuniverse fits in a commuting square with `equiv-eq` + +We claim that the square + +```text + ap B + (X ＝ Y) --------> (B X ＝ B Y) + | | + equiv-eq | | equiv-eq + V V + (X ≃ Y) ---------> (B X ≃ B Y). + B +``` + +commutes for any two types `X Y : type-subuniverse P` and any family of types +`B` over the subuniverse `P`. + +```agda +coherence-square-action-equiv-family-over-subuniverse : + {l1 l2 l3 : Level} (P : subuniverse l1 l2) (B : type-subuniverse P → UU l3) → + (X Y : type-subuniverse P) → + coherence-square-maps + ( ap B {X} {Y}) + ( equiv-eq-subuniverse P X Y) + ( equiv-eq) + ( action-equiv-family-over-subuniverse P B X Y) +coherence-square-action-equiv-family-over-subuniverse + P B X .X refl = + compute-id-equiv-action-equiv-family-over-subuniverse P B X +``` diff --git a/src/foundation/action-on-equivalences-type-families.lagda.md b/src/foundation/action-on-equivalences-type-families.lagda.md new file mode 100644 index 0000000000..2fa7aff0f7 --- /dev/null +++ b/src/foundation/action-on-equivalences-type-families.lagda.md @@ -0,0 +1,185 @@ +# Action on equivalences of type families + +```agda +module foundation.action-on-equivalences-type-families where +``` + +
Imports + +```agda +open import foundation.action-on-equivalences-functions +open import foundation.action-on-identifications-functions +open import foundation.commuting-squares-of-maps +open import foundation.constant-maps +open import foundation.equivalence-induction +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.equivalences +``` + +
+ +## Ideas + +Any family of types `B : 𝒰 → 𝒱` over a universe `𝒰` has an **action on +equivalences** + +```text + (A ≃ B) → P A ≃ P B +``` + +obtained by [equivalence induction](foundation.equivalence-induction.md). The +acion on equivalences of a type family `B` on a universe `𝒰` is uniquely +determined by the identification `B id-equiv ＝ id-equiv`, and fits in a +[commuting square](foundation.commuting-squares-of-maps.md) + +```text + ap B + (X ＝ Y) --------> (B X ＝ B Y) + | | + equiv-eq | | equiv-eq + V V + (X ≃ Y) ---------> (B X ≃ B Y). + B +``` + +Note that in general -- in particular in our general constructions below -- we +need the univalence axiom to construct the action on equivalences of a family of +types. However, for many specific type families that are defined in terms of the +basic type constructors, we can construct the action on equivalences directly +without invoking the univalence axiom. + +## Definitions + +### The action on equivalences of a family of types over a universe + +```agda +module _ + {l1 l2 : Level} (B : UU l1 → UU l2) + where + + abstract + unique-action-equiv-family : + {X : UU l1} → + is-contr (fiber (ev-id-equiv (λ Y e → B X ≃ B Y)) id-equiv) + unique-action-equiv-family = + is-contr-map-ev-id-equiv (λ Y e → B _ ≃ B Y) id-equiv + + action-equiv-family : + {X Y : UU l1} → (X ≃ Y) → B X ≃ B Y + action-equiv-family {X} {Y} = + equiv-eq ∘ action-equiv-function B + + compute-action-equiv-family-id-equiv : + {X : UU l1} → + action-equiv-family {X} {X} id-equiv ＝ id-equiv + compute-action-equiv-family-id-equiv {X} = + ap equiv-eq (compute-action-equiv-function-id-equiv B X) + + map-action-equiv-family : {X Y : UU l1} → X ≃ Y → B X → B Y + map-action-equiv-family = map-equiv ∘ action-equiv-family +``` + +## Properties + +### The action on equivalences of a family of types over a universe fits in a commuting square with `equiv-eq` + +We claim that the square + +```text + ap B + (X ＝ Y) --------> (B X ＝ B Y) + | | + equiv-eq | | equiv-eq + V V + (X ≃ Y) ---------> (B X ≃ B Y). + B +``` + +commutes for any two types `X Y : 𝒰` and any type family `B` over `𝒰`. + +```agda +coherence-square-action-equiv-family : + {l1 l2 : Level} (B : UU l1 → UU l2) (X Y : UU l1) → + coherence-square-maps + ( ap B {X} {Y}) + ( equiv-eq) + ( equiv-eq) + ( action-equiv-family B) +coherence-square-action-equiv-family B X .X refl = + compute-action-equiv-family-id-equiv B +``` + +### 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 constant map is constant + +```agda +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 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 composition of equivalences + +```agda +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-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/axiom-of-choice.lagda.md b/src/foundation/axiom-of-choice.lagda.md index 54c5a7a8eb..9312e81445 100644 --- a/src/foundation/axiom-of-choice.lagda.md +++ b/src/foundation/axiom-of-choice.lagda.md @@ -21,7 +21,6 @@ open import foundation-core.equivalences open import foundation-core.fibers-of-maps 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.sets open import foundation-core.whiskering-homotopies diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md index 961d012bda..6e73fbb572 100644 --- a/src/foundation/binary-relations.lagda.md +++ b/src/foundation/binary-relations.lagda.md @@ -124,6 +124,17 @@ module _ is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R) ``` +### Morphisms of binary relations + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} + where + + hom-Relation : Relation l2 A → Relation l3 A → UU (l1 ⊔ l2 ⊔ l3) + hom-Relation R S = (x y : A) → R x y → S x y +``` + ## Properties ### Characterization of equality of binary relations diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md index b1f54b0fe3..9ddf15431b 100644 --- a/src/foundation/commuting-triangles-of-maps.lagda.md +++ b/src/foundation/commuting-triangles-of-maps.lagda.md @@ -11,10 +11,12 @@ open import foundation-core.commuting-triangles-of-maps public ```agda open import foundation.action-on-identifications-functions open import foundation.functoriality-dependent-function-types +open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels open import foundation-core.equivalences +open import foundation-core.function-types ``` @@ -50,13 +52,22 @@ module _ equiv-coherence-triangle-maps-inv-top : coherence-triangle-maps left right (map-equiv e) ≃ - coherence-triangle-maps' right left (map-inv-equiv e) + coherence-triangle-maps right left (map-inv-equiv e) equiv-coherence-triangle-maps-inv-top = - equiv-Π + ( equiv-inv-htpy + ( left ∘ (map-inv-equiv e)) + ( right)) ∘e + ( equiv-Π ( λ b → left (map-inv-equiv e b) ＝ right b) ( e) ( λ a → equiv-concat ( ap left (is-retraction-map-inv-equiv e a)) - ( right (map-equiv e a))) + ( right (map-equiv e a)))) + + coherence-triangle-maps-inv-top : + coherence-triangle-maps left right (map-equiv e) → + coherence-triangle-maps right left (map-inv-equiv e) + coherence-triangle-maps-inv-top = + map-equiv equiv-coherence-triangle-maps-inv-top ``` diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md index 800ce600f6..bc77976212 100644 --- a/src/foundation/decidable-propositions.lagda.md +++ b/src/foundation/decidable-propositions.lagda.md @@ -170,6 +170,10 @@ pr2 (iff-universes-Decidable-Prop l l' P) p = is-set-Decidable-Prop : {l : Level} → is-set (Decidable-Prop l) is-set-Decidable-Prop {l} = is-set-equiv bool equiv-bool-Decidable-Prop is-set-bool + +Decidable-Prop-Set : (l : Level) → Set (lsuc l) +pr1 (Decidable-Prop-Set l) = Decidable-Prop l +pr2 (Decidable-Prop-Set l) = is-set-Decidable-Prop ``` ### Extensionality of decidable propositions @@ -230,6 +234,13 @@ abstract is-decidable (type-Prop P) → is-finite (type-Prop P) is-finite-is-decidable-Prop P x = is-finite-count (count-is-decidable-Prop P x) + +is-finite-type-Decidable-Prop : + {l : Level} (P : Decidable-Prop l) → is-finite (type-Decidable-Prop P) +is-finite-type-Decidable-Prop P = + is-finite-is-decidable-Prop + ( prop-Decidable-Prop P) + ( is-decidable-Decidable-Prop P) ``` ### The type of decidable propositions of any universe level is finite diff --git a/src/foundation/equivalence-extensionality.lagda.md b/src/foundation/equivalence-extensionality.lagda.md index 3c07ca39f6..7d8ad2c455 100644 --- a/src/foundation/equivalence-extensionality.lagda.md +++ b/src/foundation/equivalence-extensionality.lagda.md @@ -10,6 +10,7 @@ module foundation.equivalence-extensionality where open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.fundamental-theorem-of-identity-types +open import foundation.identity-systems open import foundation.subtype-identity-principle open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels @@ -24,6 +25,7 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions +open import foundation-core.sections ``` @@ -88,3 +90,34 @@ module _ {e e' : A ≃ B} → (map-equiv e) ＝ (map-equiv e') → htpy-equiv e e' htpy-eq-map-equiv = htpy-eq ``` + +### Homotopy induction for homotopies between equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + abstract + Ind-htpy-equiv : + {l3 : Level} (e : A ≃ B) + (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) → + section + ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) → + h e (refl-htpy-equiv e)) + Ind-htpy-equiv e = + is-identity-system-is-torsorial e + ( refl-htpy-equiv e) + ( is-contr-total-htpy-equiv e) + + ind-htpy-equiv : + {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) → + P e (refl-htpy-equiv e) → (e' : A ≃ B) (H : htpy-equiv e e') → P e' H + ind-htpy-equiv e P = pr1 (Ind-htpy-equiv e P) + + compute-ind-htpy-equiv : + {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) + (p : P e (refl-htpy-equiv e)) → + ind-htpy-equiv e P p e (refl-htpy-equiv e) ＝ p + compute-ind-htpy-equiv e P = pr2 (Ind-htpy-equiv e P) +``` diff --git a/src/foundation/equivalence-induction.lagda.md b/src/foundation/equivalence-induction.lagda.md index 5fe4716a37..735792e8a7 100644 --- a/src/foundation/equivalence-induction.lagda.md +++ b/src/foundation/equivalence-induction.lagda.md @@ -2,53 +2,259 @@ ```agda module foundation.equivalence-induction where - -open import foundation-core.equivalence-induction public ```
Imports ```agda +open import foundation.contractible-maps +open import foundation.contractible-types open import foundation.dependent-pair-types +open import foundation.identity-systems +open import foundation.identity-types +open import foundation.subuniverses open import foundation.univalence +open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels +open import foundation-core.commuting-triangles-of-maps open import foundation-core.equivalences open import foundation-core.function-types +open import foundation-core.homotopies open import foundation-core.sections +open import foundation-core.singleton-induction ```
## Idea -Equivalence induction is a condition equivalent to the univalence axiom +**Equivalence induction** is the principle asserting that for any type family + +```text + P : (B : 𝒰) (e : A ≃ B) → 𝒰 +``` + +of types indexed by all [equivalences](foundation.equivalences.md) with domain +`A`, there is a [section](foundation.sections.md) of the evaluation map + +```text + ((B : 𝒰) (e : A ≃ B) → P B e) → P A id-equiv. +``` + +The principle of equivalence induction is equivalent to the +[univalence axiom](foundation.univalence.md). -## Theorem +By equivalence induction, it follows that any type family `P : 𝒰 → 𝒱` on the +universe has an +[action on equivalences](foundation.action-on-equivalences-type-families.md) + +```text + (A ≃ B) → P A ≃ P B. +``` + +## Statement ```agda -abstract - Ind-equiv : - {l1 l2 : Level} (A : UU l1) (P : (B : UU l1) (e : A ≃ B) → UU l2) → - section (ev-id P) - Ind-equiv A P = - IND-EQUIV-is-contr-total-equiv - ( is-contr-total-equiv A) - ( λ t → P (pr1 t) (pr2 t)) +module _ + {l1 : Level} {A : UU l1} + where + + ev-id-equiv : + {l : Level} (P : (B : UU l1) → (A ≃ B) → UU l) → + ((B : UU l1) (e : A ≃ B) → P B e) → P A id-equiv + ev-id-equiv P f = f A id-equiv + + equivalence-induction : + {l : Level} (P : (B : UU l1) (e : A ≃ B) → UU l) → UU (lsuc l1 ⊔ l) + equivalence-induction P = section (ev-id-equiv P) + + triangle-ev-id-equiv : + {l : Level} + (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → + coherence-triangle-maps + ( ev-point (A , id-equiv) {P}) + ( ev-id-equiv (λ X e → P (X , e))) + ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P}) + triangle-ev-id-equiv P f = refl +``` + +## Properties + +### Equivalence induction is equivalent to the contractibility of the total space of equivalences + +#### Contractibility of the total space of equivalences implies equivalence induction + +```agda +module _ + {l1 : Level} {A : UU l1} + where + + abstract + is-identity-system-is-contr-total-equiv : + is-contr (Σ (UU l1) (λ X → A ≃ X)) → + {l : Level} → + (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → + equivalence-induction (λ B e → P (B , e)) + is-identity-system-is-contr-total-equiv c P = + section-left-factor + ( ev-id-equiv (λ X e → P (X , e))) + ( ev-pair) + ( is-singleton-is-contr + ( A , id-equiv) + ( ( A , id-equiv) , + ( λ t → + ( inv (contraction c (A , id-equiv))) ∙ (contraction c t))) + ( P)) +``` + +#### Equivalence induction implies contractibility of the total space of equivalences + +```agda +module _ + {l1 : Level} {A : UU l1} + where + + abstract + is-contr-total-is-identity-system-equiv : + ( {l : Level} → is-identity-system l (λ X → A ≃ X) A id-equiv) → + is-contr (Σ (UU l1) (λ X → A ≃ X)) + is-contr-total-is-identity-system-equiv ind = + is-contr-is-singleton + ( Σ (UU l1) (λ X → A ≃ X)) + ( A , id-equiv) + ( λ P → section-comp + ( ev-id-equiv (λ X e → P (X , e))) + ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P}) + ( ind-Σ , refl-htpy) + ( ind (λ X e → P (X , e)))) +``` + +### Equivalence induction in a universe + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2) + where + + abstract + is-identity-system-equiv : section (ev-id-equiv P) + is-identity-system-equiv = + is-identity-system-is-contr-total-equiv + ( is-contr-total-equiv _) + ( λ t → P (pr1 t) (pr2 t)) + + ind-equiv : + P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e + ind-equiv p {B} = pr1 is-identity-system-equiv p B + + compute-ind-equiv : + (u : P A id-equiv) → ind-equiv u id-equiv ＝ u + compute-ind-equiv = pr2 is-identity-system-equiv +``` + +### Equivalence induction in a subuniverse + +```agda +module _ + {l1 l2 l3 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) + where + + ev-id-equiv-subuniverse : + {F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3} → + ((B : type-subuniverse P) (e : equiv-subuniverse P A B) → F B e) → + F A id-equiv + ev-id-equiv-subuniverse f = f A id-equiv + + triangle-ev-id-equiv-subuniverse : + (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → + coherence-triangle-maps + ( ev-point (A , id-equiv)) + ( ev-id-equiv-subuniverse {F}) + ( ev-pair) + triangle-ev-id-equiv-subuniverse F E = refl -ind-equiv : - {l1 l2 : Level} (A : UU l1) (P : (B : UU l1) (e : A ≃ B) → UU l2) → - P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e -ind-equiv A P p {B} = pr1 (Ind-equiv A P) p B + abstract + is-identity-system-equiv-subuniverse : + (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → + section (ev-id-equiv-subuniverse {F}) + is-identity-system-equiv-subuniverse = + is-identity-system-is-torsorial A id-equiv + ( is-contr-total-equiv-subuniverse P A) + + ind-equiv-subuniverse : + (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → + F A id-equiv → (B : type-subuniverse P) (e : equiv-subuniverse P A B) → + F B e + ind-equiv-subuniverse F = + pr1 (is-identity-system-equiv-subuniverse F) + + compute-ind-equiv-subuniverse : + (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → + (u : F A id-equiv) → + ind-equiv-subuniverse F u A id-equiv ＝ u + compute-ind-equiv-subuniverse F = + pr2 (is-identity-system-equiv-subuniverse F) ``` -## Corollaries +### The evaluation map `ev-id-equiv` is an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2) + where + + is-equiv-ev-id-equiv : is-equiv (ev-id-equiv P) + is-equiv-ev-id-equiv = + is-equiv-left-factor-htpy + ( ev-point (A , id-equiv)) + ( ev-id-equiv P) + ( ev-pair) + ( triangle-ev-id-equiv (λ u → P (pr1 u) (pr2 u))) + ( dependent-universal-property-contr-is-contr + ( A , id-equiv) + ( is-contr-total-equiv A) + ( λ u → P (pr1 u) (pr2 u))) + ( is-equiv-ev-pair) + + is-contr-map-ev-id-equiv : is-contr-map (ev-id-equiv P) + is-contr-map-ev-id-equiv = is-contr-map-is-equiv is-equiv-ev-id-equiv +``` + +### The evaluation map `ev-id-equiv-subuniverse` is an equivalence + +```agda +module _ + {l1 l2 l3 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) + (F : (Y : type-subuniverse P) (e : equiv-subuniverse P X Y) → UU l3) + where + + is-equiv-ev-id-equiv-subuniverse : + is-equiv (ev-id-equiv-subuniverse P X {F}) + is-equiv-ev-id-equiv-subuniverse = + is-equiv-left-factor-htpy + ( ev-point (X , id-equiv)) + ( ev-id-equiv-subuniverse P X) + ( ev-pair) + ( triangle-ev-id-equiv-subuniverse P X F) + ( dependent-universal-property-contr-is-contr + ( X , id-equiv) + ( is-contr-total-equiv-subuniverse P X) + ( λ E → F (pr1 E) (pr2 E))) + ( is-equiv-ev-pair) + + is-contr-map-ev-id-equiv-subuniverse : + is-contr-map (ev-id-equiv-subuniverse P X {F}) + is-contr-map-ev-id-equiv-subuniverse = + is-contr-map-is-equiv is-equiv-ev-id-equiv-subuniverse +``` ### Equivalence induction implies that postcomposing by an equivalence is an equivalence -Of course we already know this fact from function extensionality, but we prove -it again from equivalence induction so that we can prove that univalence implies -function extensionality. +Of course we already know that this fact follows from +[function extensionality](foundation.function-extensionality.md). However, we +prove it again from equivalence induction so that we can prove that +[univalence implies function extensionality](foundation.univalence-implies-function-extensionality.md). ```agda abstract @@ -56,5 +262,5 @@ abstract {l1 l2 : Level} {X Y : UU l1} (A : UU l2) (e : X ≃ Y) → is-equiv (postcomp A (map-equiv e)) is-equiv-postcomp-univalence {X = X} A = - ind-equiv X (λ Y e → is-equiv (postcomp A (map-equiv e))) is-equiv-id + ind-equiv (λ Y e → is-equiv (postcomp A (map-equiv e))) is-equiv-id ``` diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index 858b4a952c..47fb87b058 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -15,7 +15,6 @@ open import foundation.dependent-pair-types open import foundation.equivalence-extensionality open import foundation.function-extensionality open import foundation.functoriality-fibers-of-maps -open import foundation.identity-systems open import foundation.identity-types open import foundation.truncated-maps open import foundation.type-theoretic-principle-of-choice @@ -263,37 +262,6 @@ module _ equiv-is-equiv-right-factor-htpy e (f ∘ map-equiv e) refl-htpy ``` -### Homotopy induction for homotopies between equivalences - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} - where - - abstract - Ind-htpy-equiv : - {l3 : Level} (e : A ≃ B) - (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) → - section - ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) → - h e (refl-htpy-equiv e)) - Ind-htpy-equiv e = - Ind-identity-system e - ( refl-htpy-equiv e) - ( is-contr-total-htpy-equiv e) - - ind-htpy-equiv : - {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) → - P e (refl-htpy-equiv e) → (e' : A ≃ B) (H : htpy-equiv e e') → P e' H - ind-htpy-equiv e P = pr1 (Ind-htpy-equiv e P) - - compute-ind-htpy-equiv : - {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) - (p : P e (refl-htpy-equiv e)) → - ind-htpy-equiv e P p e (refl-htpy-equiv e) ＝ p - compute-ind-htpy-equiv e P = pr2 (Ind-htpy-equiv e P) -``` - ### The groupoid laws for equivalences #### Composition of equivalences is associative diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md index 105569dbae..b8664ccc3a 100644 --- a/src/foundation/homotopies.lagda.md +++ b/src/foundation/homotopies.lagda.md @@ -86,7 +86,7 @@ abstract {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) → FUNEXT f → IND-HTPY {l3 = l3} f IND-HTPY-FUNEXT {l3 = l3} {A = A} {B = B} f funext-f = - Ind-identity-system f + is-identity-system-is-torsorial f ( refl-htpy) ( is-contr-total-htpy f) @@ -95,7 +95,7 @@ abstract {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) → ({l : Level} → IND-HTPY {l3 = l} f) → FUNEXT f FUNEXT-IND-HTPY f ind-htpy-f = - fundamental-theorem-id-IND-identity-system f + fundamental-theorem-id-is-identity-system f ( refl-htpy) ( ind-htpy-f) ( λ g → htpy-eq) diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md index 494a0cc6f6..b3622001da 100644 --- a/src/foundation/identity-systems.lagda.md +++ b/src/foundation/identity-systems.lagda.md @@ -23,25 +23,39 @@ open import foundation-core.transport-along-identifications ## Idea -A unary identity system on a type `A` equipped with a point `a : A` consists of -a type family `B` over `A` equipped with a point `b : B a` that satisfies an -induction principle analogous to the induction principle of the identity type at -`a`. +A **(unary) identity system** on a type `A` equipped with a point `a : A` +consists of a type family `B` over `A` equipped with a point `b : B a` that +satisfies an induction principle analogous to the induction principle of the +[identity type](foundation.identity-types.md) at `a`. The +[dependent universal property of identity types](foundation.universal-property-identity-types.md) +also follows for identity systems. + +## Definitions + +### The predicate of being an identity system ```agda +ev-refl-identity-system : + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a) + {P : (x : A) (y : B x) → UU l3} → + ((x : A) (y : B x) → P x y) → P a b +ev-refl-identity-system b f = f _ b + module _ {l1 l2 : Level} (l : Level) {A : UU l1} (B : A → UU l2) (a : A) (b : B a) where - IND-identity-system : UU (l1 ⊔ l2 ⊔ lsuc l) - IND-identity-system = - ( P : (x : A) (y : B x) → UU l) → - section (λ (h : (x : A) (y : B x) → P x y) → h a b) + is-identity-system : UU (l1 ⊔ l2 ⊔ lsuc l) + is-identity-system = + (P : (x : A) (y : B x) → UU l) → section (ev-refl-identity-system b {P}) ``` ## Properties -### A type family over `A` is an identity system if and only if it is equivalent to the identity type +### A type family over `A` is an identity system if and only if its total space is contractible + +In [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) +we will start calling type families with contractible total space torsorial. ```agda module _ @@ -49,36 +63,36 @@ module _ where abstract - Ind-identity-system : - (is-contr-AB : is-contr (Σ A B)) → - {l : Level} → IND-identity-system l B a b - pr1 (Ind-identity-system is-contr-AB P) p x y = + is-identity-system-is-torsorial : + (H : is-contr (Σ A B)) → + {l : Level} → is-identity-system l B a b + pr1 (is-identity-system-is-torsorial H P) p x y = tr ( fam-Σ P) - ( eq-is-contr is-contr-AB) + ( eq-is-contr H) ( p) - pr2 (Ind-identity-system is-contr-AB P) p = + pr2 (is-identity-system-is-torsorial H P) p = ap ( λ t → tr (fam-Σ P) t p) ( eq-is-contr' - ( is-prop-is-contr is-contr-AB (pair a b) (pair a b)) - ( eq-is-contr is-contr-AB) + ( is-prop-is-contr H (pair a b) (pair a b)) + ( eq-is-contr H) ( refl)) abstract - is-contr-total-space-IND-identity-system : - ({l : Level} → IND-identity-system l B a b) → is-contr (Σ A B) - pr1 (pr1 (is-contr-total-space-IND-identity-system ind)) = a - pr2 (pr1 (is-contr-total-space-IND-identity-system ind)) = b - pr2 (is-contr-total-space-IND-identity-system ind) (pair x y) = - pr1 (ind (λ x' y' → (pair a b) ＝ (pair x' y'))) refl x y + is-torsorial-is-identity-system : + ({l : Level} → is-identity-system l B a b) → is-contr (Σ A B) + pr1 (pr1 (is-torsorial-is-identity-system H)) = a + pr2 (pr1 (is-torsorial-is-identity-system H)) = b + pr2 (is-torsorial-is-identity-system H) (pair x y) = + pr1 (H (λ x' y' → (pair a b) ＝ (pair x' y'))) refl x y abstract - fundamental-theorem-id-IND-identity-system : - ({l : Level} → IND-identity-system l B a b) → + fundamental-theorem-id-is-identity-system : + ({l : Level} → is-identity-system l B a b) → (f : (x : A) → a ＝ x → B x) → (x : A) → is-equiv (f x) - fundamental-theorem-id-IND-identity-system ind f = + fundamental-theorem-id-is-identity-system H f = fundamental-theorem-id - ( is-contr-total-space-IND-identity-system ind) + ( is-torsorial-is-identity-system H) ( f) ``` diff --git a/src/foundation/subuniverses.lagda.md b/src/foundation/subuniverses.lagda.md index 5c1d434904..07d686f36f 100644 --- a/src/foundation/subuniverses.lagda.md +++ b/src/foundation/subuniverses.lagda.md @@ -169,6 +169,12 @@ module _ {s t : type-subuniverse P} → equiv-subuniverse s t → s ＝ t eq-equiv-subuniverse {s} {t} = map-inv-is-equiv (is-equiv-equiv-eq-subuniverse s t) + + compute-eq-equiv-id-equiv-subuniverse : + {s : type-subuniverse P} → + eq-equiv-subuniverse {s} {s} (id-equiv {A = pr1 s}) ＝ refl + compute-eq-equiv-id-equiv-subuniverse = + is-retraction-map-inv-equiv (extensionality-subuniverse _ _) refl ``` ### Equivalences of families of types in a subuniverse diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md new file mode 100644 index 0000000000..c9688b1722 --- /dev/null +++ b/src/foundation/symmetric-binary-relations.lagda.md @@ -0,0 +1,198 @@ +# Symmetric binary relations + +```agda +module foundation.symmetric-binary-relations where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.equivalence-extensionality +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.symmetric-operations +open import foundation.transport-along-identifications +open import foundation.universe-levels +open import foundation.unordered-pairs + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A **symmetric binary relation** on a type `A` is a type family `R` over the type +of [unordered pairs](foundation.unordered-pairs.md) of elements of `A`. Given a +symmetric binary relation `R` on `A` and an equivalence of unordered pairs +`p ＝ q`, we have `R p ≃ R q`. In particular, we have + +```text + R ({x,y}) ≃ R ({y,x}) +``` + +for any two elements `x y : A`, where `{x,y}` is the _standard unordered pair_ +consisting of `x` and `y`. + +Note that a symmetric binary relation R on a type is just a +[symmetric operation](foundation.symmetric-operations.md) from `A` into a +universe `𝒰`. + +## Definitions + +### Symmetric binary relations + +```agda +Symmetric-Relation : + {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +Symmetric-Relation l2 A = symmetric-operation A (UU l2) +``` + +### Action on symmetries of symmetric binary relations + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (R : Symmetric-Relation l2 A) + where + + abstract + equiv-tr-Symmetric-Relation : + (p q : unordered-pair A) → Eq-unordered-pair p q → R p ≃ R q + equiv-tr-Symmetric-Relation p = + ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv + + compute-refl-equiv-tr-Symmetric-Relation : + (p : unordered-pair A) → + equiv-tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ＝ + id-equiv + compute-refl-equiv-tr-Symmetric-Relation p = + compute-refl-ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv + + htpy-compute-refl-equiv-tr-Symmetric-Relation : + (p : unordered-pair A) → + htpy-equiv + ( equiv-tr-Symmetric-Relation p p (refl-Eq-unordered-pair p)) + ( id-equiv) + htpy-compute-refl-equiv-tr-Symmetric-Relation p = + htpy-eq-equiv (compute-refl-equiv-tr-Symmetric-Relation p) + + abstract + tr-Symmetric-Relation : + (p q : unordered-pair A) → Eq-unordered-pair p q → R p → R q + tr-Symmetric-Relation p q e = + map-equiv (equiv-tr-Symmetric-Relation p q e) + + tr-inv-Symmetric-Relation : + (p q : unordered-pair A) → Eq-unordered-pair p q → R q → R p + tr-inv-Symmetric-Relation p q e = + map-inv-equiv (equiv-tr-Symmetric-Relation p q e) + + is-section-tr-inv-Symmetric-Relation : + (p q : unordered-pair A) (e : Eq-unordered-pair p q) → + tr-Symmetric-Relation p q e ∘ + tr-inv-Symmetric-Relation p q e ~ + id + is-section-tr-inv-Symmetric-Relation p q e = + is-section-map-inv-equiv (equiv-tr-Symmetric-Relation p q e) + + is-retraction-tr-inv-Symmetric-Relation : + (p q : unordered-pair A) (e : Eq-unordered-pair p q) → + tr-inv-Symmetric-Relation p q e ∘ + tr-Symmetric-Relation p q e ~ + id + is-retraction-tr-inv-Symmetric-Relation p q e = + is-retraction-map-inv-equiv (equiv-tr-Symmetric-Relation p q e) + + compute-refl-tr-Symmetric-Relation : + (p : unordered-pair A) → + tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ＝ id + compute-refl-tr-Symmetric-Relation p = + ap map-equiv (compute-refl-equiv-tr-Symmetric-Relation p) + + htpy-compute-refl-tr-Symmetric-Relation : + (p : unordered-pair A) → + tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ~ id + htpy-compute-refl-tr-Symmetric-Relation p = + htpy-eq (compute-refl-tr-Symmetric-Relation p) +``` + +### The underlying binary relation of a symmetric binary relation + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (R : Symmetric-Relation l2 A) + where + + relation-Symmetric-Relation : Relation l2 A + relation-Symmetric-Relation x y = R (standard-unordered-pair x y) + + equiv-symmetric-relation-Symmetric-Relation : + {x y : A} → + relation-Symmetric-Relation x y ≃ + relation-Symmetric-Relation y x + equiv-symmetric-relation-Symmetric-Relation {x} {y} = + equiv-tr-Symmetric-Relation R + ( standard-unordered-pair x y) + ( standard-unordered-pair y x) + ( swap-standard-unordered-pair x y) + + symmetric-relation-Symmetric-Relation : + {x y : A} → + relation-Symmetric-Relation x y → + relation-Symmetric-Relation y x + symmetric-relation-Symmetric-Relation = + map-equiv equiv-symmetric-relation-Symmetric-Relation +``` + +### The forgetful functor from binary relations to symmetric binary relations + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (R : Relation l2 A) + where + + symmetric-relation-Relation : Symmetric-Relation l2 A + symmetric-relation-Relation p = + Σ ( type-unordered-pair p) + ( λ i → + R (element-unordered-pair p i) (other-element-unordered-pair p i)) + + unit-symmetric-relation-Relation : + (x y : A) → R x y → + relation-Symmetric-Relation symmetric-relation-Relation x y + pr1 (unit-symmetric-relation-Relation x y r) = zero-Fin 1 + pr2 (unit-symmetric-relation-Relation x y r) = + tr + ( R x) + ( inv (compute-other-element-standard-unordered-pair x y (zero-Fin 1))) + ( r) +``` + +### Morphisms of symmetric binary relations + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} + where + + hom-Symmetric-Relation : + Symmetric-Relation l2 A → Symmetric-Relation l3 A → + UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3) + hom-Symmetric-Relation R S = + (p : unordered-pair A) → R p → S p + + hom-relation-hom-Symmetric-Relation : + (R : Symmetric-Relation l2 A) (S : Symmetric-Relation l3 A) → + hom-Symmetric-Relation R S → + hom-Relation + ( relation-Symmetric-Relation R) + ( relation-Symmetric-Relation S) + hom-relation-hom-Symmetric-Relation R S f x y = + f (standard-unordered-pair x y) +``` diff --git a/src/foundation/symmetric-operations.lagda.md b/src/foundation/symmetric-operations.lagda.md index 5e779b56c8..804aa8eaa0 100644 --- a/src/foundation/symmetric-operations.lagda.md +++ b/src/foundation/symmetric-operations.lagda.md @@ -9,9 +9,17 @@ module foundation.symmetric-operations where ```agda open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions +open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalence-extensionality +open import foundation.function-extensionality +open import foundation.function-types open import foundation.functoriality-coproduct-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.subtypes open import foundation.universal-property-propositional-truncation-into-sets open import foundation.universe-levels open import foundation.unordered-pairs @@ -56,14 +64,27 @@ module _ is-commutative : (A → A → B) → UU (l1 ⊔ l2) is-commutative f = (x y : A) → f x y ＝ f y x + +is-commutative-Prop : + {l1 l2 : Level} {A : UU l1} (B : Set l2) → + (A → A → type-Set B) → Prop (l1 ⊔ l2) +is-commutative-Prop B f = + Π-Prop _ (λ x → Π-Prop _ (λ y → Id-Prop B (f x y) (f y x))) ``` ### Commutative operations ```agda -symmetric-operation : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (lsuc lzero ⊔ l1 ⊔ l2) -symmetric-operation A B = unordered-pair A → B +module _ + {l1 l2 : Level} (A : UU l1) (B : UU l2) + where + + symmetric-operation : UU (lsuc lzero ⊔ l1 ⊔ l2) + symmetric-operation = unordered-pair A → B + + map-symmetric-operation : symmetric-operation → A → A → B + map-symmetric-operation f x y = + f (standard-unordered-pair x y) ``` ## Properties @@ -143,3 +164,144 @@ module _ p : Fin 2 → A p = pr2 (standard-unordered-pair x y) ``` + +### Characterization of equality of symmetric operations into sets + +```agda +module _ + {l1 l2 : Level} (A : UU l1) (B : Set l2) + (f : symmetric-operation A (type-Set B)) + where + + htpy-symmetric-operation-Set-Prop : + (g : symmetric-operation A (type-Set B)) → Prop (l1 ⊔ l2) + htpy-symmetric-operation-Set-Prop g = + Π-Prop A + ( λ x → + Π-Prop A + ( λ y → + Id-Prop B + ( map-symmetric-operation A (type-Set B) f x y) + ( map-symmetric-operation A (type-Set B) g x y))) + + htpy-symmetric-operation-Set : + (g : symmetric-operation A (type-Set B)) → UU (l1 ⊔ l2) + htpy-symmetric-operation-Set g = + type-Prop (htpy-symmetric-operation-Set-Prop g) + + center-total-htpy-symmetric-operation-Set : + Σ ( symmetric-operation A (type-Set B)) + ( htpy-symmetric-operation-Set) + pr1 center-total-htpy-symmetric-operation-Set = f + pr2 center-total-htpy-symmetric-operation-Set x y = refl + + contraction-total-htpy-symmetric-operation-Set : + ( t : + Σ ( symmetric-operation A (type-Set B)) + ( htpy-symmetric-operation-Set)) → + center-total-htpy-symmetric-operation-Set ＝ t + contraction-total-htpy-symmetric-operation-Set (g , H) = + eq-type-subtype + htpy-symmetric-operation-Set-Prop + ( eq-htpy + ( λ p → + apply-universal-property-trunc-Prop + ( is-surjective-standard-unordered-pair p) + ( Id-Prop B (f p) (g p)) + ( λ { (x , y , refl) → H x y}))) + + is-contr-total-htpy-symmetric-operation-Set : + is-contr + ( Σ ( symmetric-operation A (type-Set B)) + ( htpy-symmetric-operation-Set)) + pr1 is-contr-total-htpy-symmetric-operation-Set = + center-total-htpy-symmetric-operation-Set + pr2 is-contr-total-htpy-symmetric-operation-Set = + contraction-total-htpy-symmetric-operation-Set + + htpy-eq-symmetric-operation-Set : + (g : symmetric-operation A (type-Set B)) → + (f ＝ g) → htpy-symmetric-operation-Set g + htpy-eq-symmetric-operation-Set g refl x y = refl + + is-equiv-htpy-eq-symmetric-operation-Set : + (g : symmetric-operation A (type-Set B)) → + is-equiv (htpy-eq-symmetric-operation-Set g) + is-equiv-htpy-eq-symmetric-operation-Set = + fundamental-theorem-id + is-contr-total-htpy-symmetric-operation-Set + htpy-eq-symmetric-operation-Set + + extensionality-symmetric-operation-Set : + (g : symmetric-operation A (type-Set B)) → + (f ＝ g) ≃ htpy-symmetric-operation-Set g + pr1 (extensionality-symmetric-operation-Set g) = + htpy-eq-symmetric-operation-Set g + pr2 (extensionality-symmetric-operation-Set g) = + is-equiv-htpy-eq-symmetric-operation-Set g + + eq-htpy-symmetric-operation-Set : + (g : symmetric-operation A (type-Set B)) → + htpy-symmetric-operation-Set g → (f ＝ g) + eq-htpy-symmetric-operation-Set g = + map-inv-equiv (extensionality-symmetric-operation-Set g) +``` + +### The type of commutative operations into a set is equivalent to the type of symmetric operations + +```agda +module _ + {l1 l2 : Level} (A : UU l1) (B : Set l2) + where + + map-compute-symmetric-operation-Set : + symmetric-operation A (type-Set B) → Σ (A → A → type-Set B) is-commutative + pr1 (map-compute-symmetric-operation-Set f) = + map-symmetric-operation A (type-Set B) f + pr2 (map-compute-symmetric-operation-Set f) = + is-commutative-symmetric-operation f + + map-inv-compute-symmetric-operation-Set : + Σ (A → A → type-Set B) is-commutative → symmetric-operation A (type-Set B) + map-inv-compute-symmetric-operation-Set (f , H) = + symmetric-operation-is-commutative B f H + + is-section-map-inv-compute-symmetric-operation-Set : + ( map-compute-symmetric-operation-Set ∘ + map-inv-compute-symmetric-operation-Set) ~ id + is-section-map-inv-compute-symmetric-operation-Set (f , H) = + eq-type-subtype + ( is-commutative-Prop B) + ( eq-htpy + ( λ x → + eq-htpy + ( λ y → + compute-symmetric-operation-is-commutative B f H x y))) + + is-retraction-map-inv-compute-symmetric-operation-Set : + ( map-inv-compute-symmetric-operation-Set ∘ + map-compute-symmetric-operation-Set) ~ id + is-retraction-map-inv-compute-symmetric-operation-Set g = + eq-htpy-symmetric-operation-Set A B + ( map-inv-compute-symmetric-operation-Set + ( map-compute-symmetric-operation-Set g)) + ( g) + ( compute-symmetric-operation-is-commutative B + ( map-symmetric-operation A (type-Set B) g) + ( is-commutative-symmetric-operation g)) + + is-equiv-map-compute-symmetric-operation-Set : + is-equiv map-compute-symmetric-operation-Set + is-equiv-map-compute-symmetric-operation-Set = + is-equiv-is-invertible + map-inv-compute-symmetric-operation-Set + is-section-map-inv-compute-symmetric-operation-Set + is-retraction-map-inv-compute-symmetric-operation-Set + + compute-symmetric-operation-Set : + symmetric-operation A (type-Set B) ≃ Σ (A → A → type-Set B) is-commutative + pr1 compute-symmetric-operation-Set = + map-compute-symmetric-operation-Set + pr2 compute-symmetric-operation-Set = + is-equiv-map-compute-symmetric-operation-Set +``` diff --git a/src/foundation/transport-along-equivalences.lagda.md b/src/foundation/transport-along-equivalences.lagda.md index ebf2304b5c..316a911c17 100644 --- a/src/foundation/transport-along-equivalences.lagda.md +++ b/src/foundation/transport-along-equivalences.lagda.md @@ -8,12 +8,12 @@ module foundation.transport-along-equivalences where ```agda open import foundation.action-on-equivalences-functions +open import foundation.action-on-equivalences-type-families 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 @@ -182,10 +182,10 @@ 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 + ind-equiv ( λ 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)) + inv (compute-action-equiv-family-id-equiv f)) eq-map-tr-equiv-map-action-equiv-family : {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → diff --git a/src/foundation/universal-property-identity-systems.lagda.md b/src/foundation/universal-property-identity-systems.lagda.md new file mode 100644 index 0000000000..a31939e189 --- /dev/null +++ b/src/foundation/universal-property-identity-systems.lagda.md @@ -0,0 +1,98 @@ +# The universal property of identity systems + +```agda +module foundation.universal-property-identity-systems where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.identity-systems +open import foundation.torsorial-type-families +open import foundation.universal-property-dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.identity-types +``` + +
+ +## Idea + +A **(unary) identity system** on a type `A` equipped with a point `a : A` +consists of a type family `B` over `A` equipped with a point `b : B a` that +satisfies an induction principle analogous to the induction principle of the +[identity type](foundation.identity-types.md) at `a`. The +[dependent universal property of identity types](foundation.universal-property-identity-types.md) +also follows for identity systems. + +## Definition + +### The universal property of identity systems + +```agda +dependent-universal-property-identity-system : + {l1 l2 : Level} (l3 : Level) {A : UU l1} {B : A → UU l2} {a : A} (b : B a) → + UU (l1 ⊔ l2 ⊔ lsuc l3) +dependent-universal-property-identity-system l3 {A} {B} b = + (P : (x : A) (y : B x) → UU l3) → is-equiv (ev-refl-identity-system b {P}) +``` + +## Properties + +### A type family satisfies the dependent universal property of identity systems if and only if it is torsorial + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a) + where + + dependent-universal-property-identity-system-is-torsorial : + is-torsorial B → + {l3 : Level} → dependent-universal-property-identity-system l3 {A} {B} b + dependent-universal-property-identity-system-is-torsorial + H P = + is-equiv-left-factor + ( ev-refl-identity-system b) + ( ev-pair) + ( dependent-universal-property-contr-is-contr + ( a , b) + ( H) + ( λ u → P (pr1 u) (pr2 u))) + ( is-equiv-ev-pair) + + is-torsorial-dependent-universal-property-identity-system : + ({l3 : Level} → dependent-universal-property-identity-system l3 {A} {B} b) → + is-torsorial B + pr1 (is-torsorial-dependent-universal-property-identity-system H) = (a , b) + pr2 (is-torsorial-dependent-universal-property-identity-system H) u = + map-inv-is-equiv + ( H (λ x y → (a , b) ＝ (x , y))) + ( refl) + ( pr1 u) + ( pr2 u) +``` + +### A type family satisfies the dependent universal property of identity systems if and only if it is an identity system + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a) + where + + dependent-universal-property-identity-system-is-identity-system : + ({l : Level} → is-identity-system l {A} B a b) → + ({l : Level} → dependent-universal-property-identity-system l {A} {B} b) + dependent-universal-property-identity-system-is-identity-system H = + dependent-universal-property-identity-system-is-torsorial b + ( is-torsorial-is-identity-system a b H) + + is-identity-system-dependent-universal-property-identity-system : + ({l : Level} → dependent-universal-property-identity-system l {A} {B} b) → + ({l : Level} → is-identity-system l {A} B a b) + is-identity-system-dependent-universal-property-identity-system H P = + section-is-equiv (H P) +``` diff --git a/src/foundation/unordered-pairs-of-types.lagda.md b/src/foundation/unordered-pairs-of-types.lagda.md index 6819cbe635..491d79e352 100644 --- a/src/foundation/unordered-pairs-of-types.lagda.md +++ b/src/foundation/unordered-pairs-of-types.lagda.md @@ -71,7 +71,7 @@ module _ ## Properties -### Univalence for unordered pairs of types +### Extensionality of unordered pairs of types ```agda module _ diff --git a/src/foundation/unordered-pairs.lagda.md b/src/foundation/unordered-pairs.lagda.md index 30c68f06e7..e69737ea60 100644 --- a/src/foundation/unordered-pairs.lagda.md +++ b/src/foundation/unordered-pairs.lagda.md @@ -8,6 +8,9 @@ module foundation.unordered-pairs where ```agda open import foundation.action-on-identifications-functions +open import foundation.commuting-triangles-of-maps +open import foundation.contractible-maps +open import foundation.contractible-types open import foundation.decidable-equality open import foundation.dependent-pair-types open import foundation.existential-quantification @@ -17,9 +20,9 @@ open import foundation.homotopies open import foundation.mere-equivalences open import foundation.propositional-truncations open import foundation.structure-identity-principle +open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels -open import foundation-core.contractible-types open import foundation-core.coproduct-types open import foundation-core.embeddings open import foundation-core.equivalences @@ -125,21 +128,34 @@ Any two elements `x` and `y` in a type `A` define a standard unordered pair ```agda module _ - {l1 : Level} {A : UU l1} + {l1 : Level} {A : UU l1} (x y : A) where - element-standard-unordered-pair : (x y : A) → Fin 2 → A - element-standard-unordered-pair x y (inl (inr star)) = x - element-standard-unordered-pair x y (inr star) = y - - standard-unordered-pair : A → A → unordered-pair A - pr1 (standard-unordered-pair x y) = Fin-UU-Fin' 2 - pr2 (standard-unordered-pair x y) = element-standard-unordered-pair x y + element-standard-unordered-pair : Fin 2 → A + element-standard-unordered-pair (inl (inr star)) = x + element-standard-unordered-pair (inr star) = y + + standard-unordered-pair : unordered-pair A + pr1 standard-unordered-pair = Fin-UU-Fin' 2 + pr2 standard-unordered-pair = element-standard-unordered-pair + + other-element-standard-unordered-pair : Fin 2 → A + other-element-standard-unordered-pair (inl (inr star)) = y + other-element-standard-unordered-pair (inr star) = x + + compute-other-element-standard-unordered-pair : + (u : Fin 2) → + other-element-unordered-pair standard-unordered-pair u ＝ + other-element-standard-unordered-pair u + compute-other-element-standard-unordered-pair (inl (inr star)) = + ap element-standard-unordered-pair (compute-swap-Fin-two-ℕ (inl (inr star))) + compute-other-element-standard-unordered-pair (inr star) = + ap element-standard-unordered-pair (compute-swap-Fin-two-ℕ (inr star)) ``` ## Properties -### Equality of unordered pairs +### Extensionality of unordered pairs ```agda module _ @@ -150,7 +166,10 @@ module _ Eq-unordered-pair p q = Σ ( type-unordered-pair p ≃ type-unordered-pair q) ( λ e → - (element-unordered-pair p) ~ (element-unordered-pair q ∘ map-equiv e)) + coherence-triangle-maps + ( element-unordered-pair p) + ( element-unordered-pair q) + ( map-equiv e)) refl-Eq-unordered-pair : (p : unordered-pair A) → Eq-unordered-pair p p pr1 (refl-Eq-unordered-pair (pair X p)) = id-equiv-UU-Fin {k = 2} X @@ -211,6 +230,78 @@ module _ eq-Eq-refl-unordered-pair p = is-retraction-eq-Eq-unordered-pair p p refl ``` +### Induction on equality of unordered pairs + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (p : unordered-pair A) + (B : (q : unordered-pair A) → Eq-unordered-pair p q → UU l2) + where + + ev-refl-Eq-unordered-pair : + ((q : unordered-pair A) (e : Eq-unordered-pair p q) → B q e) → + B p (refl-Eq-unordered-pair p) + ev-refl-Eq-unordered-pair f = f p (refl-Eq-unordered-pair p) + + triangle-ev-refl-Eq-unordered-pair : + coherence-triangle-maps + ( ev-point (p , refl-Eq-unordered-pair p)) + ( ev-refl-Eq-unordered-pair) + ( ev-pair) + triangle-ev-refl-Eq-unordered-pair = refl-htpy + + abstract + is-equiv-ev-refl-Eq-unordered-pair : is-equiv ev-refl-Eq-unordered-pair + is-equiv-ev-refl-Eq-unordered-pair = + is-equiv-left-factor-htpy + ( ev-point (p , refl-Eq-unordered-pair p)) + ( ev-refl-Eq-unordered-pair) + ( ev-pair) + ( triangle-ev-refl-Eq-unordered-pair) + ( dependent-universal-property-contr-is-contr + ( p , refl-Eq-unordered-pair p) + ( is-contr-total-Eq-unordered-pair p) + ( λ u → B (pr1 u) (pr2 u))) + ( is-equiv-ev-pair) + + abstract + is-contr-map-ev-refl-Eq-unordered-pair : + is-contr-map ev-refl-Eq-unordered-pair + is-contr-map-ev-refl-Eq-unordered-pair = + is-contr-map-is-equiv is-equiv-ev-refl-Eq-unordered-pair + + abstract + ind-Eq-unordered-pair : + B p (refl-Eq-unordered-pair p) → + ((q : unordered-pair A) (e : Eq-unordered-pair p q) → B q e) + ind-Eq-unordered-pair u = + pr1 (center (is-contr-map-ev-refl-Eq-unordered-pair u)) + + compute-refl-ind-Eq-unordered-pair : + (u : B p (refl-Eq-unordered-pair p)) → + ind-Eq-unordered-pair u p (refl-Eq-unordered-pair p) ＝ u + compute-refl-ind-Eq-unordered-pair u = + pr2 (center (is-contr-map-ev-refl-Eq-unordered-pair u)) +``` + +### Inverting extensional equality of unordered pairs + +```agda +module _ + {l : Level} {A : UU l} (p q : unordered-pair A) + where + + inv-Eq-unordered-pair : + Eq-unordered-pair p q → Eq-unordered-pair q p + pr1 (inv-Eq-unordered-pair (e , H)) = inv-equiv e + pr2 (inv-Eq-unordered-pair (e , H)) = + coherence-triangle-maps-inv-top + ( element-unordered-pair p) + ( element-unordered-pair q) + ( e) + ( H) +``` + ### Mere equality of unordered pairs ```agda @@ -238,15 +329,25 @@ module _ ### A standard unordered pair `{x,y}` is equal to the standard unordered pair `{y,x}` ```agda -is-commutative-standard-unordered-pair : - {l : Level} {A : UU l} (x y : A) → - standard-unordered-pair x y ＝ standard-unordered-pair y x -is-commutative-standard-unordered-pair x y = - eq-Eq-unordered-pair - ( standard-unordered-pair x y) - ( standard-unordered-pair y x) - ( equiv-succ-Fin 2) - ( λ { (inl (inr star)) → refl ; (inr star) → refl}) +module _ + {l1 : Level} {A : UU l1} (x y : A) + where + + swap-standard-unordered-pair : + Eq-unordered-pair + ( standard-unordered-pair x y) + ( standard-unordered-pair y x) + pr1 swap-standard-unordered-pair = equiv-succ-Fin 2 + pr2 swap-standard-unordered-pair (inl (inr star)) = refl + pr2 swap-standard-unordered-pair (inr star) = refl + + is-commutative-standard-unordered-pair : + standard-unordered-pair x y ＝ standard-unordered-pair y x + is-commutative-standard-unordered-pair = + eq-Eq-unordered-pair' + ( standard-unordered-pair x y) + ( standard-unordered-pair y x) + ( swap-standard-unordered-pair) ``` ### Functoriality of unordered pairs @@ -346,5 +447,74 @@ id-equiv-standard-unordered-pair x y = unordered-distinct-pair : {l : Level} (A : UU l) → UU (lsuc lzero ⊔ l) -unordered-distinct-pair A = Σ (UU-Fin lzero 2) (λ X → pr1 X ↪ A) +unordered-distinct-pair A = + Σ (UU-Fin lzero 2) (λ X → pr1 X ↪ A) +``` + +### Every unordered pair is merely equal to a standard unordered pair + +```agda +is-surjective-standard-unordered-pair : + {l : Level} {A : UU l} (p : unordered-pair A) → + type-trunc-Prop + ( Σ A (λ x → Σ A (λ y → standard-unordered-pair x y ＝ p))) +is-surjective-standard-unordered-pair (I , a) = + apply-universal-property-trunc-Prop + ( has-two-elements-type-2-Element-Type I) + ( trunc-Prop + ( Σ _ (λ x → Σ _ (λ y → standard-unordered-pair x y ＝ (I , a))))) + ( λ e → + unit-trunc-Prop + ( a (map-equiv e (zero-Fin 1)) , + a (map-equiv e (one-Fin 1)) , + eq-Eq-unordered-pair + ( standard-unordered-pair _ _) + ( I , a) + ( e) + ( λ { (inl (inr star)) → refl ; (inr star) → refl}))) +``` + +### For every unordered pair `p` and every element `i` in its underlying type, `p` is equal to a standard unordered pair + +```agda +module _ + {l : Level} {A : UU l} (p : unordered-pair A) (i : type-unordered-pair p) + where + + compute-standard-unordered-pair-element-unordered-pair : + Eq-unordered-pair + ( standard-unordered-pair + ( element-unordered-pair p i) + ( other-element-unordered-pair p i)) + ( p) + pr1 compute-standard-unordered-pair-element-unordered-pair = + equiv-point-2-Element-Type + ( 2-element-type-unordered-pair p) + ( i) + pr2 compute-standard-unordered-pair-element-unordered-pair (inl (inr star)) = + ap + ( element-unordered-pair p) + ( inv + ( compute-map-equiv-point-2-Element-Type + ( 2-element-type-unordered-pair p) + ( i))) + pr2 compute-standard-unordered-pair-element-unordered-pair (inr star) = + ap + ( element-unordered-pair p) + ( inv + ( compute-map-equiv-point-2-Element-Type' + ( 2-element-type-unordered-pair p) + ( i))) + + eq-compute-standard-unordered-pair-element-unordered-pair : + standard-unordered-pair + ( element-unordered-pair p i) + ( other-element-unordered-pair p i) ＝ p + eq-compute-standard-unordered-pair-element-unordered-pair = + eq-Eq-unordered-pair' + ( standard-unordered-pair + ( element-unordered-pair p i) + ( other-element-unordered-pair p i)) + ( p) + ( compute-standard-unordered-pair-element-unordered-pair) ``` diff --git a/src/group-theory/commuting-elements-groups.lagda.md b/src/group-theory/commuting-elements-groups.lagda.md index 5b20cee33a..9e76af7d68 100644 --- a/src/group-theory/commuting-elements-groups.lagda.md +++ b/src/group-theory/commuting-elements-groups.lagda.md @@ -7,10 +7,8 @@ module group-theory.commuting-elements-groups where
Imports ```agda -open import foundation.action-on-identifications-functions open import foundation.identity-types open import foundation.propositions -open import foundation.sets open import foundation.universe-levels open import group-theory.commuting-elements-monoids diff --git a/src/group-theory/endomorphism-rings-abelian-groups.lagda.md b/src/group-theory/endomorphism-rings-abelian-groups.lagda.md index 8ae3888a1a..d3dfb679a9 100644 --- a/src/group-theory/endomorphism-rings-abelian-groups.lagda.md +++ b/src/group-theory/endomorphism-rings-abelian-groups.lagda.md @@ -8,8 +8,6 @@ module group-theory.endomorphism-rings-abelian-groups where ```agda open import foundation.dependent-pair-types -open import foundation.propositional-truncations -open import foundation.surjective-maps open import foundation.universe-levels open import group-theory.abelian-groups diff --git a/src/group-theory/free-groups-with-one-generator.lagda.md b/src/group-theory/free-groups-with-one-generator.lagda.md index 82e51078e9..c500185cbc 100644 --- a/src/group-theory/free-groups-with-one-generator.lagda.md +++ b/src/group-theory/free-groups-with-one-generator.lagda.md @@ -10,16 +10,13 @@ module group-theory.free-groups-with-one-generator where open import elementary-number-theory.addition-integers open import elementary-number-theory.group-of-integers open import elementary-number-theory.integers -open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions open import foundation.contractible-maps open import foundation.contractible-types -open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types -open import foundation.iterating-automorphisms open import foundation.sets open import foundation.subtypes open import foundation.universe-levels diff --git a/src/group-theory/images-of-group-homomorphisms.lagda.md b/src/group-theory/images-of-group-homomorphisms.lagda.md index 420c28599e..c8bde8b2fa 100644 --- a/src/group-theory/images-of-group-homomorphisms.lagda.md +++ b/src/group-theory/images-of-group-homomorphisms.lagda.md @@ -7,13 +7,11 @@ module group-theory.images-of-group-homomorphisms where
Imports ```agda -open import foundation.commuting-triangles-of-maps open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.images open import foundation.logical-equivalences open import foundation.propositional-truncations -open import foundation.surjective-maps open import foundation.universal-property-image open import foundation.universe-levels diff --git a/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md b/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md index 3251509447..8520bd3ff2 100644 --- a/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md @@ -13,19 +13,14 @@ open import elementary-number-theory.multiplication-integers open import elementary-number-theory.natural-numbers 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.iterating-automorphisms open import foundation.universe-levels open import group-theory.abelian-groups open import group-theory.homomorphisms-abelian-groups open import group-theory.integer-powers-of-elements-groups open import group-theory.multiples-of-elements-abelian-groups - -open import structured-types.initial-pointed-type-equipped-with-automorphism -open import structured-types.pointed-types-equipped-with-automorphisms ```
diff --git a/src/group-theory/integer-powers-of-elements-groups.lagda.md b/src/group-theory/integer-powers-of-elements-groups.lagda.md index c82108f187..5315782812 100644 --- a/src/group-theory/integer-powers-of-elements-groups.lagda.md +++ b/src/group-theory/integer-powers-of-elements-groups.lagda.md @@ -16,7 +16,6 @@ open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.identity-types open import foundation.iterating-automorphisms -open import foundation.unit-type open import foundation.universe-levels open import group-theory.commuting-elements-groups diff --git a/src/group-theory/multiples-of-elements-abelian-groups.lagda.md b/src/group-theory/multiples-of-elements-abelian-groups.lagda.md index 7423a3fc0c..e2f024ab58 100644 --- a/src/group-theory/multiples-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/multiples-of-elements-abelian-groups.lagda.md @@ -7,25 +7,15 @@ module group-theory.multiples-of-elements-abelian-groups where
Imports ```agda -open import elementary-number-theory.addition-integers open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.integers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers -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.iterating-automorphisms open import foundation.universe-levels open import group-theory.abelian-groups -open import group-theory.groups -open import group-theory.homomorphisms-abelian-groups open import group-theory.powers-of-elements-groups - -open import structured-types.initial-pointed-type-equipped-with-automorphism ```
diff --git a/src/group-theory/powers-of-elements-groups.lagda.md b/src/group-theory/powers-of-elements-groups.lagda.md index 2b55097976..e0583295d3 100644 --- a/src/group-theory/powers-of-elements-groups.lagda.md +++ b/src/group-theory/powers-of-elements-groups.lagda.md @@ -7,26 +7,17 @@ module group-theory.powers-of-elements-groups where
Imports ```agda -open import elementary-number-theory.addition-integers open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.integers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers -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.iterating-automorphisms -open import foundation.unit-type open import foundation.universe-levels open import group-theory.commuting-elements-groups open import group-theory.groups open import group-theory.homomorphisms-groups open import group-theory.powers-of-elements-monoids - -open import structured-types.initial-pointed-type-equipped-with-automorphism ```
diff --git a/src/group-theory/subgroups-generated-by-elements-groups.lagda.md b/src/group-theory/subgroups-generated-by-elements-groups.lagda.md index 71fbafefa0..e03f34a3a7 100644 --- a/src/group-theory/subgroups-generated-by-elements-groups.lagda.md +++ b/src/group-theory/subgroups-generated-by-elements-groups.lagda.md @@ -9,15 +9,12 @@ module group-theory.subgroups-generated-by-elements-groups where ```agda open import elementary-number-theory.group-of-integers open import elementary-number-theory.integers -open import elementary-number-theory.natural-numbers -open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.singleton-subtypes open import foundation.subtypes -open import foundation.unit-type open import foundation.universe-levels open import group-theory.free-groups-with-one-generator diff --git a/src/higher-group-theory/cyclic-higher-groups.lagda.md b/src/higher-group-theory/cyclic-higher-groups.lagda.md index fe27880197..8870924523 100644 --- a/src/higher-group-theory/cyclic-higher-groups.lagda.md +++ b/src/higher-group-theory/cyclic-higher-groups.lagda.md @@ -14,9 +14,6 @@ open import foundation.universe-levels open import higher-group-theory.higher-groups open import higher-group-theory.homomorphisms-higher-groups - -open import synthetic-homotopy-theory.functoriality-loop-spaces -open import synthetic-homotopy-theory.loop-spaces ```
diff --git a/src/orthogonal-factorization-systems/local-families.lagda.md b/src/orthogonal-factorization-systems/local-families.lagda.md index fa92bac793..7fcf5faa64 100644 --- a/src/orthogonal-factorization-systems/local-families.lagda.md +++ b/src/orthogonal-factorization-systems/local-families.lagda.md @@ -7,27 +7,10 @@ module orthogonal-factorization-systems.local-families where
Imports ```agda -open import foundation.action-on-identifications-functions -open import foundation.contractible-maps -open import foundation.contractible-types open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.equivalences -open import foundation.fibers-of-maps -open import foundation.function-extensionality open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.functoriality-function-types -open import foundation.identity-types open import foundation.propositions -open import foundation.retractions -open import foundation.sections -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 -open import foundation.universal-property-empty-type open import foundation.universe-levels open import orthogonal-factorization-systems.local-types diff --git a/src/orthogonal-factorization-systems/local-maps.lagda.md b/src/orthogonal-factorization-systems/local-maps.lagda.md index 14a6b71b46..414018dfb5 100644 --- a/src/orthogonal-factorization-systems/local-maps.lagda.md +++ b/src/orthogonal-factorization-systems/local-maps.lagda.md @@ -7,31 +7,11 @@ module orthogonal-factorization-systems.local-maps where
Imports ```agda -open import foundation.action-on-identifications-functions -open import foundation.contractible-maps -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.empty-types -open import foundation.equivalences open import foundation.fibers-of-maps -open import foundation.function-extensionality -open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.functoriality-function-types -open import foundation.identity-types open import foundation.propositions -open import foundation.retractions -open import foundation.sections -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 -open import foundation.universal-property-empty-type open import foundation.universe-levels open import orthogonal-factorization-systems.local-families -open import orthogonal-factorization-systems.local-types ```
diff --git a/src/ring-theory/category-of-rings.lagda.md b/src/ring-theory/category-of-rings.lagda.md index b947694e21..864f8110f8 100644 --- a/src/ring-theory/category-of-rings.lagda.md +++ b/src/ring-theory/category-of-rings.lagda.md @@ -10,7 +10,6 @@ module ring-theory.category-of-rings where open import category-theory.categories open import category-theory.large-categories -open import foundation.fundamental-theorem-of-identity-types open import foundation.universe-levels open import ring-theory.isomorphisms-rings 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 5f2d652de3..aefe4acb6d 100644 --- a/src/ring-theory/integer-multiples-of-elements-rings.lagda.md +++ b/src/ring-theory/integer-multiples-of-elements-rings.lagda.md @@ -16,7 +16,6 @@ open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.identity-types open import foundation.transport-along-identifications -open import foundation.unit-type open import foundation.universe-levels open import group-theory.homomorphisms-abelian-groups diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md index f36a5fb094..aeff4276e6 100644 --- a/src/ring-theory/isomorphisms-rings.lagda.md +++ b/src/ring-theory/isomorphisms-rings.lagda.md @@ -10,7 +10,6 @@ module ring-theory.isomorphisms-rings where open import category-theory.isomorphisms-large-precategories open import foundation.action-on-identifications-functions -open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types @@ -21,7 +20,6 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions -open import foundation.sets open import foundation.structure-identity-principle open import foundation.subtype-identity-principle open import foundation.subtypes diff --git a/src/ring-theory/powers-of-elements-semirings.lagda.md b/src/ring-theory/powers-of-elements-semirings.lagda.md index d85e2984a0..ca2f29b47c 100644 --- a/src/ring-theory/powers-of-elements-semirings.lagda.md +++ b/src/ring-theory/powers-of-elements-semirings.lagda.md @@ -11,7 +11,6 @@ open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers -open import foundation.action-on-identifications-functions open import foundation.identity-types open import foundation.universe-levels diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md index a2096ced2b..e113b5a80e 100644 --- a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md @@ -7,12 +7,9 @@ module synthetic-homotopy-theory.dependent-suspension-structures where
Imports ```agda -open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps open import foundation.constant-maps -open import foundation.contractible-types open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences @@ -20,25 +17,16 @@ open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies -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-along-identifications -open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type open import foundation.universe-levels -open import synthetic-homotopy-theory.cocones-under-spans -open import synthetic-homotopy-theory.conjugation-loops open import synthetic-homotopy-theory.dependent-cocones-under-spans -open import synthetic-homotopy-theory.dependent-universal-property-pushouts -open import synthetic-homotopy-theory.functoriality-loop-spaces -open import synthetic-homotopy-theory.loop-spaces -open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.suspension-structures -open import synthetic-homotopy-theory.universal-property-pushouts ```
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 fd85921d9e..e4b40dc9c1 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md @@ -8,39 +8,17 @@ module synthetic-homotopy-theory.dependent-universal-property-suspensions where ```agda open import foundation.action-on-identifications-dependent-functions -open import foundation.action-on-identifications-functions -open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps open import foundation.constant-maps -open import foundation.contractible-types -open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-extensionality open import foundation.function-types -open import foundation.functoriality-dependent-pair-types open import foundation.homotopies -open import foundation.identity-systems -open import foundation.identity-types -open import foundation.structure-identity-principle -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 open import foundation.universe-levels -open import structured-types.pointed-equivalences -open import structured-types.pointed-maps -open import structured-types.pointed-types - -open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-suspension-structures -open import synthetic-homotopy-theory.dependent-universal-property-pushouts -open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.suspension-structures -open import synthetic-homotopy-theory.universal-property-pushouts -open import synthetic-homotopy-theory.universal-property-suspensions ```
diff --git a/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md b/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md index e0cc330f78..412d79e16b 100644 --- a/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md @@ -9,7 +9,6 @@ module synthetic-homotopy-theory.descent-circle-dependent-pair-types where ```agda open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types -open import foundation.equivalences open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.universe-levels 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 26b8f2b799..885cc7d9e8 100644 --- a/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md @@ -149,12 +149,13 @@ module _ ( equiv-inv-htpy ( map-aut-family-with-descent-data-circle B ∘ h) ( h ∘ map-aut-family-with-descent-data-circle A)) ∘e - ( ( inv-equiv - ( equiv-coherence-triangle-maps-inv-top - ( map-aut-family-with-descent-data-circle B ∘ h) - ( h) - ( aut-family-with-descent-data-circle A))) ∘e - ( equiv-funext))) + ( inv-equiv + ( equiv-coherence-triangle-maps-inv-top + ( map-aut-family-with-descent-data-circle B ∘ h) + ( h) + ( aut-family-with-descent-data-circle A))) ∘e + ( equiv-inv-htpy _ _) ∘e + ( equiv-funext)) equiv-ev-descent-data-circle-function-type-hom : dependent-universal-property-circle (l2 ⊔ l3) l → diff --git a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md index 41ccd22018..7b328268d2 100644 --- a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md @@ -11,7 +11,6 @@ open import foundation.commuting-squares-of-maps open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.function-types -open import foundation.functoriality-function-types open import foundation.pullbacks open import foundation.universe-levels diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md index 51084e96be..3e73a38685 100644 --- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md @@ -7,15 +7,10 @@ module synthetic-homotopy-theory.suspension-structures where
Imports ```agda -open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions -open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps open import foundation.constant-maps open import foundation.contractible-types -open import foundation.dependent-identifications open import foundation.dependent-pair-types -open import foundation.embeddings open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types @@ -25,22 +20,11 @@ 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-along-identifications -open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-unit-type open import foundation.universe-levels -open import structured-types.pointed-equivalences -open import structured-types.pointed-maps -open import structured-types.pointed-types - open import synthetic-homotopy-theory.cocones-under-spans -open import synthetic-homotopy-theory.dependent-cocones-under-spans -open import synthetic-homotopy-theory.dependent-universal-property-pushouts -open import synthetic-homotopy-theory.loop-spaces -open import synthetic-homotopy-theory.pushouts -open import synthetic-homotopy-theory.universal-property-pushouts ```
@@ -259,7 +243,7 @@ module _ P c' H) ind-htpy-suspension-structure P = pr1 - ( Ind-identity-system + ( is-identity-system-is-torsorial ( c) ( refl-htpy-suspension-structure) ( is-contr-equiv 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 66d7735858..b6959c312d 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-pointed-types.lagda.md @@ -7,43 +7,16 @@ module synthetic-homotopy-theory.suspensions-of-pointed-types where
Imports ```agda -open import foundation.action-on-identifications-dependent-functions -open import foundation.action-on-identifications-functions -open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps open import foundation.constant-maps -open import foundation.contractible-types -open import foundation.dependent-identifications open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.function-extensionality -open import foundation.function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.homotopies -open import foundation.identity-systems open import foundation.identity-types -open import foundation.structure-identity-principle -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 open import foundation.universe-levels -open import structured-types.pointed-equivalences -open import structured-types.pointed-maps open import structured-types.pointed-types -open import synthetic-homotopy-theory.cocones-under-spans -open import synthetic-homotopy-theory.dependent-cocones-under-spans -open import synthetic-homotopy-theory.dependent-suspension-structures -open import synthetic-homotopy-theory.dependent-universal-property-pushouts -open import synthetic-homotopy-theory.dependent-universal-property-suspensions open import synthetic-homotopy-theory.loop-spaces -open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.suspensions-of-types -open import synthetic-homotopy-theory.universal-property-pushouts -open import synthetic-homotopy-theory.universal-property-suspensions ```
diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 517d08df40..1c37e70746 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -10,29 +10,21 @@ module synthetic-homotopy-theory.suspensions-of-types where open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps open import foundation.constant-maps open import foundation.contractible-types -open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies -open import foundation.identity-systems open import foundation.identity-types -open import foundation.structure-identity-principle 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 open import foundation.universe-levels open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-suspension-structures -open import synthetic-homotopy-theory.dependent-universal-property-pushouts open import synthetic-homotopy-theory.dependent-universal-property-suspensions open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.suspension-structures diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 940f31faf7..9c3de244af 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -12,7 +12,6 @@ open import elementary-number-theory.universal-property-integers open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions -open import foundation.cartesian-product-types open import foundation.commuting-squares-of-maps open import foundation.contractible-types open import foundation.dependent-identifications @@ -28,7 +27,6 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.raising-universe-levels open import foundation.sets -open import foundation.structure-identity-principle open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels 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 aa892fc08a..38ab886c89 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 @@ -7,46 +7,23 @@ module synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types
Imports ```agda -open import foundation.action-on-identifications-dependent-functions -open import foundation.action-on-identifications-functions -open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps -open import foundation.constant-maps open import foundation.contractible-types -open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types -open import foundation.homotopies -open import foundation.identity-systems open import foundation.identity-types -open import foundation.structure-identity-principle -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 open import foundation.universe-levels open import structured-types.pointed-equivalences open import structured-types.pointed-maps open import structured-types.pointed-types -open import synthetic-homotopy-theory.cocones-under-spans -open import synthetic-homotopy-theory.conjugation-loops -open import synthetic-homotopy-theory.dependent-cocones-under-spans -open import synthetic-homotopy-theory.dependent-suspension-structures -open import synthetic-homotopy-theory.dependent-universal-property-pushouts -open import synthetic-homotopy-theory.dependent-universal-property-suspensions open import synthetic-homotopy-theory.functoriality-loop-spaces open import synthetic-homotopy-theory.loop-spaces -open import synthetic-homotopy-theory.pushouts -open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.suspensions-of-pointed-types open import synthetic-homotopy-theory.suspensions-of-types -open import synthetic-homotopy-theory.universal-property-pushouts -open import synthetic-homotopy-theory.universal-property-suspensions ```
diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md index a8a1066c3b..af2d5a2e74 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md @@ -7,34 +7,17 @@ module synthetic-homotopy-theory.universal-property-suspensions where
Imports ```agda -open import foundation.action-on-identifications-dependent-functions -open import foundation.action-on-identifications-functions -open import foundation.commuting-squares-of-identifications -open import foundation.commuting-squares-of-maps open import foundation.constant-maps -open import foundation.contractible-types -open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-extensionality open import foundation.function-types -open import foundation.functoriality-dependent-pair-types open import foundation.homotopies -open import foundation.identity-systems open import foundation.identity-types -open import foundation.structure-identity-principle -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 open import foundation.universe-levels open import foundation.whiskering-homotopies open import synthetic-homotopy-theory.cocones-under-spans -open import synthetic-homotopy-theory.dependent-cocones-under-spans -open import synthetic-homotopy-theory.dependent-suspension-structures -open import synthetic-homotopy-theory.dependent-universal-property-pushouts -open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.universal-property-pushouts ``` diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md index 4324e51af9..0e822632fb 100644 --- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md +++ b/src/univalent-combinatorics/pigeonhole-principle.lagda.md @@ -17,7 +17,6 @@ open import foundation.embeddings open import foundation.empty-types open import foundation.equivalences open import foundation.function-types -open import foundation.homotopies open import foundation.identity-types open import foundation.injective-maps open import foundation.negation