diff --git a/.vscode/tasks.json b/.vscode/tasks.json index 293173d868..bc9d85e2c9 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -9,11 +9,11 @@ "kind": "test", "isDefault": true }, - "dependsOn": ["pre-commit", "link-check", "typecheck"], + "dependsOn": ["pre-commit", "link-check", "typecheck_"], "dependsOrder": "parallel" }, { - "label": "typecheck", + "label": "typecheck_", "detail": "Typecheck the library", "type": "shell", "command": "make", @@ -21,6 +21,20 @@ "problemMatcher": [], "group": { "kind": "build" }, "dependsOn": "pre-commit", + "hide": true, + "presentation": { + "panel": "dedicated", + "clear": true + } + }, + { + "label": "typecheck", + "detail": "Typecheck the library", + "type": "shell", + "command": "make", + "args": ["check"], + "problemMatcher": [], + "group": { "kind": "build" }, "presentation": { "panel": "dedicated", "clear": true diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md index 0a9c7a225e..5c3f902d6a 100644 --- a/src/category-theory/functors-precategories.lagda.md +++ b/src/category-theory/functors-precategories.lagda.md @@ -278,14 +278,7 @@ module _ equiv-ap-emb ( comp-emb ( emb-subtype (is-functor-prop-map-Precategory C D)) - ( emb-equiv - ( inv-associative-Σ - ( obj-Precategory C → obj-Precategory D) - ( λ F₀ → - { x y : obj-Precategory C} → - hom-Precategory C x y → - hom-Precategory D (F₀ x) (F₀ y)) - ( pr1 ∘ is-functor-prop-map-Precategory C D)))) + ( emb-equiv inv-associative-Σ)) eq-map-eq-functor-Precategory : (F ＝ G) → (map-functor-Precategory C D F ＝ map-functor-Precategory C D G) diff --git a/src/category-theory/functors-set-magmoids.lagda.md b/src/category-theory/functors-set-magmoids.lagda.md index 63fbec6ca4..5007025482 100644 --- a/src/category-theory/functors-set-magmoids.lagda.md +++ b/src/category-theory/functors-set-magmoids.lagda.md @@ -231,16 +231,8 @@ module _ equiv-eq-map-eq-functor-Set-Magmoid = equiv-ap-emb ( comp-emb - ( emb-subtype - ( preserves-comp-hom-prop-map-Set-Magmoid A B)) - ( emb-equiv - ( inv-associative-Σ - ( obj-Set-Magmoid A → obj-Set-Magmoid B) - ( λ F₀ → - { x y : obj-Set-Magmoid A} → - hom-Set-Magmoid A x y → - hom-Set-Magmoid B (F₀ x) (F₀ y)) - ( preserves-comp-hom-map-Set-Magmoid A B)))) + ( emb-subtype (preserves-comp-hom-prop-map-Set-Magmoid A B)) + ( emb-equiv inv-associative-Σ)) eq-map-eq-functor-Set-Magmoid : F ＝ G → map-functor-Set-Magmoid A B F ＝ map-functor-Set-Magmoid A B G diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md index 2fb548ee06..57d4f11e78 100644 --- a/src/category-theory/groupoids.lagda.md +++ b/src/category-theory/groupoids.lagda.md @@ -151,20 +151,7 @@ module _ ( λ (y , p) → Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl)) ( λ (q , l) → p ∙ q ＝ refl))) - ( ( equiv-tot - ( λ y → - equiv-tot - ( λ p → - associative-Σ - ( y ＝ x) - ( λ q → q ∙ p ＝ refl) - ( λ (q , r) → p ∙ q ＝ refl)))) ∘e - ( associative-Σ - ( type-1-Type X) - ( λ y → x ＝ y) - ( λ (y , p) → - Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl)) - ( λ (q , l) → p ∙ q ＝ refl)))) + ( equiv-tot (λ y → equiv-tot (λ p → associative-Σ)) ∘e associative-Σ) ( is-contr-iterated-Σ 2 ( is-torsorial-Id x , ( x , refl) , diff --git a/src/category-theory/replete-subprecategories.lagda.md b/src/category-theory/replete-subprecategories.lagda.md index 3de9094024..c98a58ff9f 100644 --- a/src/category-theory/replete-subprecategories.lagda.md +++ b/src/category-theory/replete-subprecategories.lagda.md @@ -247,7 +247,7 @@ module _ ( equiv-tot ( equiv-is-iso-is-iso-base-is-replete-Subprecategory C P is-replete-P {x} {y})) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot ( λ f → ( commutative-product) ∘e diff --git a/src/category-theory/structure-equivalences-set-magmoids.lagda.md b/src/category-theory/structure-equivalences-set-magmoids.lagda.md index 97006c2dcd..57c77791f0 100644 --- a/src/category-theory/structure-equivalences-set-magmoids.lagda.md +++ b/src/category-theory/structure-equivalences-set-magmoids.lagda.md @@ -122,15 +122,15 @@ module _ compute-structure-equiv-Set-Magmoid : componentwise-structure-equiv-Set-Magmoid ≃ structure-equiv-Set-Magmoid A B compute-structure-equiv-Set-Magmoid = - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot ( λ F₀ → - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e equiv-tot (λ _ → equiv-left-swap-Σ) ∘e ( equiv-left-swap-Σ) ∘e ( equiv-tot ( λ is-equiv-F₀ → - ( associative-Σ _ _ _) ∘e + ( associative-Σ) ∘e ( equiv-right-swap-Σ) ∘e ( equiv-Σ-equiv-base ( λ E₁' → @@ -138,7 +138,7 @@ module _ ( ( distributive-implicit-Π-Σ) ∘e ( equiv-implicit-Π-equiv-family ( λ _ → distributive-implicit-Π-Σ)))))))) ∘e - ( associative-Σ _ _ _) + ( associative-Σ) ``` ### Structure equivalences of set-magmoids characterize their equality diff --git a/src/commutative-algebra/polynomials-commutative-semirings.lagda.md b/src/commutative-algebra/polynomials-commutative-semirings.lagda.md index 6e21dadfa9..04df6a5232 100644 --- a/src/commutative-algebra/polynomials-commutative-semirings.lagda.md +++ b/src/commutative-algebra/polynomials-commutative-semirings.lagda.md @@ -874,7 +874,7 @@ module _ sum-equiv-finite-Commutative-Semiring R ( _) ( _) - ( associative-Σ _ _ _) + ( associative-Σ) ( _)) ( refl)) ＝ diff --git a/src/elementary-number-theory/falling-factorials.lagda.md b/src/elementary-number-theory/falling-factorials.lagda.md index a799101a48..f5ac9bfd58 100644 --- a/src/elementary-number-theory/falling-factorials.lagda.md +++ b/src/elementary-number-theory/falling-factorials.lagda.md @@ -70,11 +70,7 @@ Fin-falling-factorial-ℕ (succ-ℕ n) (succ-ℕ m) = ( is-decidable-Σ-Fin ( λ x → has-decidable-equality-Fin (map-emb f x) (inr star))))) ∘e - ( ( inv-equiv - ( left-distributive-Σ-coproduct - ( Fin (succ-ℕ m) ↪ Fin (succ-ℕ n)) - ( λ f → fiber (map-emb f) (inr star)) - ( λ f → ¬ (fiber (map-emb f) (inr star))))) ∘e + ( ( inv-left-distributive-Σ-coproduct) ∘e {!!})) ∘e ( equiv-coproduct ( Fin-falling-factorial-ℕ n m) diff --git a/src/elementary-number-theory/type-arithmetic-natural-numbers.lagda.md b/src/elementary-number-theory/type-arithmetic-natural-numbers.lagda.md index 9d3fa6833f..cc48c40cab 100644 --- a/src/elementary-number-theory/type-arithmetic-natural-numbers.lagda.md +++ b/src/elementary-number-theory/type-arithmetic-natural-numbers.lagda.md @@ -206,12 +206,12 @@ equiv-coproduct-Fin-ℕ (succ-ℕ n) = equiv-product-Fin-ℕ : (n : ℕ) → ((Fin (succ-ℕ n)) × ℕ) ≃ ℕ equiv-product-Fin-ℕ zero-ℕ = ( left-unit-law-coproduct ℕ) ∘e - ( ( equiv-coproduct (left-absorption-product ℕ) left-unit-law-product) ∘e - ( right-distributive-product-coproduct empty unit ℕ)) + ( ( equiv-coproduct (left-absorption-product ℕ) left-unit-law-product) ∘e + ( right-distributive-product-coproduct)) equiv-product-Fin-ℕ (succ-ℕ n) = ( ℕ+ℕ≃ℕ) ∘e - ( ( equiv-coproduct (equiv-product-Fin-ℕ n) left-unit-law-product) ∘e - ( right-distributive-product-coproduct (Fin (succ-ℕ n)) unit ℕ)) + ( ( equiv-coproduct (equiv-product-Fin-ℕ n) left-unit-law-product) ∘e + ( right-distributive-product-coproduct)) ``` ### The integers `ℤ` is equivalent to `ℕ` diff --git a/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md b/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md index f3b417e9ae..1f0ea1cd99 100644 --- a/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md @@ -245,6 +245,6 @@ abstract ( Σ (Fin k) (B ∘ inl)) ( B (inr star)) f) ∘e ( equiv-coproduct id-equiv (left-unit-law-Σ (B ∘ inr)))) ∘e - ( right-distributive-Σ-coproduct (Fin k) unit B)) + ( right-distributive-Σ-coproduct B)) ( y))) ``` diff --git a/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md b/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md index c29be5ba4a..5790b0d216 100644 --- a/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md +++ b/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md @@ -138,7 +138,7 @@ module _ ( ( equiv-tot ( λ Y → equiv-postcomp-equiv - ( right-distributive-Σ-coproduct A B Y) + ( right-distributive-Σ-coproduct Y) ( X))) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (A + B)) diff --git a/src/foundation/choice-of-representatives-equivalence-relation.lagda.md b/src/foundation/choice-of-representatives-equivalence-relation.lagda.md index 6ba3e69b75..0cf976d904 100644 --- a/src/foundation/choice-of-representatives-equivalence-relation.lagda.md +++ b/src/foundation/choice-of-representatives-equivalence-relation.lagda.md @@ -83,10 +83,8 @@ module _ fundamental-theorem-id ( is-contr-equiv ( Σ A (λ x → P x × sim-equivalence-relation R a x)) - ( ( associative-Σ A P (λ z → sim-equivalence-relation R a (pr1 z))) ∘e - ( equiv-tot - ( λ t → - is-effective-class R a (pr1 t)))) + ( ( associative-Σ) ∘e + ( equiv-tot (λ t → is-effective-class R a (pr1 t)))) ( H a)) ( λ y → ap (class-representatives H) {pair a p} {y}) diff --git a/src/foundation/coherently-invertible-maps.lagda.md b/src/foundation/coherently-invertible-maps.lagda.md index 03f1ed4655..5bdd4981a1 100644 --- a/src/foundation/coherently-invertible-maps.lagda.md +++ b/src/foundation/coherently-invertible-maps.lagda.md @@ -78,7 +78,7 @@ module _ is-proof-irrelevant-is-coherently-invertible H = is-contr-equiv' ( _) - ( associative-Σ _ _ _) + ( associative-Σ) ( is-contr-Σ ( is-contr-section-is-coherently-invertible H) ( section-is-coherently-invertible H) diff --git a/src/foundation/coproduct-decompositions-subuniverse.lagda.md b/src/foundation/coproduct-decompositions-subuniverse.lagda.md index 3d8495b9a1..494082f580 100644 --- a/src/foundation/coproduct-decompositions-subuniverse.lagda.md +++ b/src/foundation/coproduct-decompositions-subuniverse.lagda.md @@ -294,23 +294,15 @@ module _ binary-coproduct-Decomposition-subuniverse P X ≃ binary-coproduct-Decomposition-subuniverse P X equiv-commutative-binary-coproduct-Decomposition-subuniverse = - ( associative-Σ - ( type-subuniverse P) - ( λ _ → type-subuniverse P) - ( _)) ∘e + ( associative-Σ) ∘e ( ( equiv-Σ ( _) ( commutative-product) ( λ x → equiv-postcomp-equiv - ( commutative-coproduct - ( inclusion-subuniverse P (pr1 x)) - ( inclusion-subuniverse P (pr2 x))) - (inclusion-subuniverse P X))) ∘e - ( ( inv-associative-Σ - ( type-subuniverse P) - ( λ _ → type-subuniverse P) - ( _)))) + ( commutative-coproduct) + ( inclusion-subuniverse P X))) ∘e + ( inv-associative-Σ)) ``` ### Equivalence between iterated coproduct and ternary coproduct decomposition @@ -384,7 +376,7 @@ module _ ( equiv-tot ( λ x → ( ( equiv-postcomp-equiv - ( commutative-coproduct _ _) + ( commutative-coproduct) ( inclusion-subuniverse P X)) ∘e ( ( left-unit-law-Σ-is-contr ( is-torsorial-equiv-subuniverse' P @@ -506,8 +498,7 @@ module _ ( eq-type-Prop (P _))) ( eq-is-prop is-property-is-empty))) ( ( raise-empty l1 , C1) , is-empty-raise-empty)) ∘e - ( ( inv-associative-Σ _ _ _) ∘e - ( ( equiv-tot (λ _ → commutative-product)) ∘e - ( ( associative-Σ _ _ _))))))) ∘e - ( ( associative-Σ _ _ _)) + ( ( inv-associative-Σ) ∘e + ( equiv-tot (λ _ → commutative-product) ∘e associative-Σ))))) ∘e + ( associative-Σ) ``` diff --git a/src/foundation/coproduct-decompositions.lagda.md b/src/foundation/coproduct-decompositions.lagda.md index 4f8dfd14be..081d474d3f 100644 --- a/src/foundation/coproduct-decompositions.lagda.md +++ b/src/foundation/coproduct-decompositions.lagda.md @@ -246,7 +246,7 @@ module _ ( ( equiv-coproduct ( left-unit-law-Σ-is-contr ( is-contr-Fin-1) ( inr star)) ( left-unit-law-Σ-is-contr is-contr-unit star)) ∘e - ( ( right-distributive-Σ-coproduct ( Fin 1) unit (λ x → fiber f x) ∘e + ( ( right-distributive-Σ-coproduct (λ x → fiber f x) ∘e ( inv-equiv-total-fiber f)))) compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : @@ -272,8 +272,6 @@ module _ ( inr star)) ( map-left-unit-law-Σ-is-contr is-contr-unit star)) ( map-right-distributive-Σ-coproduct - ( Fin 1) - ( unit) ( λ x → fiber f x) ( pr1 a , x , pr2 a)))) ( λ z → pr1 (pr1 z) ＝ x)) @@ -335,8 +333,6 @@ module _ ( inr star)) ( map-left-unit-law-Σ-is-contr is-contr-unit star)) ( map-right-distributive-Σ-coproduct - ( Fin 1) - ( unit) ( λ x → fiber f x) ( pr1 a , x , pr2 a)))) ( λ z → pr1 (pr1 z) ＝ x)) @@ -519,8 +515,6 @@ module _ ( map-left-unit-law-Σ-is-contr is-contr-Fin-1 ( inr star)) ( map-left-unit-law-Σ-is-contr is-contr-unit star) ( map-right-distributive-Σ-coproduct - ( Fin 1) - ( unit) ( λ y → y ＝ f x) ( f x , refl)))) @@ -543,8 +537,6 @@ module _ equiv-tot ( λ _ → extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e ( ( right-distributive-Σ-coproduct - ( left-summand-binary-coproduct-Decomposition d) - ( right-summand-binary-coproduct-Decomposition d) ( λ y → map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper d y ＝ inl (inr star))) ∘e @@ -573,8 +565,6 @@ module _ equiv-tot ( λ _ → extensionality-Fin 2 (inr star) (inr star)))) ∘e ( ( right-distributive-Σ-coproduct - ( left-summand-binary-coproduct-Decomposition d) - ( right-summand-binary-coproduct-Decomposition d) ( λ y → map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper d y ＝ inr star)) ∘e @@ -612,8 +602,6 @@ module _ ( λ _ → extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e ( ( right-distributive-Σ-coproduct - ( left-summand-binary-coproduct-Decomposition d) - ( right-summand-binary-coproduct-Decomposition d) ( λ y → map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper d y ＝ @@ -667,8 +655,6 @@ module _ equiv-tot ( λ _ → extensionality-Fin 2 (inr star) (inr star)))) ∘e ( ( right-distributive-Σ-coproduct - ( left-summand-binary-coproduct-Decomposition d) - ( right-summand-binary-coproduct-Decomposition d) ( λ y → map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper d y ＝ inr star))))) diff --git a/src/foundation/decidable-dependent-pair-types.lagda.md b/src/foundation/decidable-dependent-pair-types.lagda.md index 401e13a607..01a42bb150 100644 --- a/src/foundation/decidable-dependent-pair-types.lagda.md +++ b/src/foundation/decidable-dependent-pair-types.lagda.md @@ -78,7 +78,7 @@ is-decidable-Σ-coproduct : is-decidable (Σ (A + B) C) is-decidable-Σ-coproduct {A = A} {B} C dA dB = is-decidable-equiv - ( right-distributive-Σ-coproduct A B C) + ( right-distributive-Σ-coproduct C) ( is-decidable-coproduct dA dB) ``` diff --git a/src/foundation/decidable-equivalence-relations.lagda.md b/src/foundation/decidable-equivalence-relations.lagda.md index 7616e35b46..809ae075f3 100644 --- a/src/foundation/decidable-equivalence-relations.lagda.md +++ b/src/foundation/decidable-equivalence-relations.lagda.md @@ -513,8 +513,8 @@ equiv-Surjection-Into-Set-Decidable-Equivalence-Relation {l1} A = ( is-set-has-decidable-equality)) ∘e ( commutative-product)) ∘e ( equiv-left-swap-Σ)))) ∘e - ( associative-Σ _ _ _) ∘e - ( associative-Σ _ _ _) ∘e + ( associative-Σ) ∘e + ( associative-Σ) ∘e ( equiv-type-subtype ( λ surj → is-prop-Π diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md index 8215e2af78..24c1b8f0c4 100644 --- a/src/foundation/decidable-propositions.lagda.md +++ b/src/foundation/decidable-propositions.lagda.md @@ -76,8 +76,7 @@ split-Decidable-Prop : Decidable-Prop l ≃ ((Σ (Prop l) type-Prop) + (Σ (Prop l) (λ Q → ¬ (type-Prop Q)))) split-Decidable-Prop {l} = - ( left-distributive-Σ-coproduct (Prop l) (λ Q → pr1 Q) (λ Q → ¬ (pr1 Q))) ∘e - ( inv-associative-Σ (UU l) is-prop (λ X → is-decidable (pr1 X))) + left-distributive-Σ-coproduct ∘e inv-associative-Σ ``` ### The type of decidable propositions in universe level `l` is equivalent to the type of booleans diff --git a/src/foundation/decidable-subtypes.lagda.md b/src/foundation/decidable-subtypes.lagda.md index b2c8b2f18f..d54451386b 100644 --- a/src/foundation/decidable-subtypes.lagda.md +++ b/src/foundation/decidable-subtypes.lagda.md @@ -500,10 +500,9 @@ module _ equiv-Σ-decide-is-in-decidable-subtype : X ≃ Σ X (is-decidable ∘ is-in-decidable-subtype S) equiv-Σ-decide-is-in-decidable-subtype = - inv-equiv - ( equiv-inclusion-is-full-subtype - ( λ x → is-decidable-Prop (subtype-decidable-subtype S x)) - ( is-decidable-decidable-subtype S)) + inv-equiv-inclusion-is-full-subtype + ( λ x → is-decidable-Prop (subtype-decidable-subtype S x)) + ( is-decidable-decidable-subtype S) ``` ### Given a decidable subtype `S ⊆ X`, there is a surjective map from `Maybe X` to `Maybe S` diff --git a/src/foundation/disjunction.lagda.md b/src/foundation/disjunction.lagda.md index f2ad3c4942..03be3850de 100644 --- a/src/foundation/disjunction.lagda.md +++ b/src/foundation/disjunction.lagda.md @@ -346,7 +346,7 @@ module _ where swap-disjunction : disjunction-type A B → disjunction-type B A - swap-disjunction = map-trunc-Prop (map-commutative-coproduct A B) + swap-disjunction = map-trunc-Prop map-commutative-coproduct ``` ### Associativity of the disjunction diff --git a/src/foundation/exclusive-disjunction.lagda.md b/src/foundation/exclusive-disjunction.lagda.md index 92407933be..f64452e516 100644 --- a/src/foundation/exclusive-disjunction.lagda.md +++ b/src/foundation/exclusive-disjunction.lagda.md @@ -162,8 +162,6 @@ module _ ( is-prop-type-Prop Q q q'))))) ∘e ( equiv-dependent-universal-property-coproduct (inr q ＝_))))) ∘e ( right-distributive-Σ-coproduct - ( type-Prop P) - ( type-Prop Q) ( λ x → (y : type-Prop P + type-Prop Q) → x ＝ y)) ``` diff --git a/src/foundation/exclusive-sum.lagda.md b/src/foundation/exclusive-sum.lagda.md index 7282c9e05d..5683503a4f 100644 --- a/src/foundation/exclusive-sum.lagda.md +++ b/src/foundation/exclusive-sum.lagda.md @@ -250,8 +250,6 @@ module _ ( pr1 (standard-unordered-pair P Q)) ( inl (inr y))))))))))) ∘e ( ( right-distributive-Σ-coproduct - ( Fin 0) - ( unit) ( λ x → ( type-Prop (pr2 (standard-unordered-pair P Q) (inl x))) × ( ¬ ( type-Prop @@ -278,8 +276,6 @@ module _ ( pr1 (standard-unordered-pair P Q)) ( inr y)))))))))) ∘e ( right-distributive-Σ-coproduct - ( Fin 1) - ( unit) ( λ x → ( type-Prop (pr2 (standard-unordered-pair P Q) x)) × ( ¬ ( type-Prop diff --git a/src/foundation/full-subtypes.lagda.md b/src/foundation/full-subtypes.lagda.md index eb9c39abfe..814204107c 100644 --- a/src/foundation/full-subtypes.lagda.md +++ b/src/foundation/full-subtypes.lagda.md @@ -88,6 +88,11 @@ module _ pr1 (equiv-inclusion-is-full-subtype H) = inclusion-subtype P pr2 (equiv-inclusion-is-full-subtype H) = is-equiv-inclusion-is-full-subtype H + inv-equiv-inclusion-is-full-subtype : + is-full-subtype P → A ≃ type-subtype P + inv-equiv-inclusion-is-full-subtype H = + inv-equiv (equiv-inclusion-is-full-subtype H) + is-full-is-equiv-inclusion-subtype : is-equiv (inclusion-subtype P) → is-full-subtype P is-full-is-equiv-inclusion-subtype H x = diff --git a/src/foundation/fundamental-theorem-of-equivalence-relations.lagda.md b/src/foundation/fundamental-theorem-of-equivalence-relations.lagda.md index 8bd7600e74..c86dc7bae8 100644 --- a/src/foundation/fundamental-theorem-of-equivalence-relations.lagda.md +++ b/src/foundation/fundamental-theorem-of-equivalence-relations.lagda.md @@ -93,10 +93,9 @@ module _ equiv-block-equivalence-class = ( compute-block-partition partition-equivalence-relation) ∘e ( ( equiv-right-swap-Σ) ∘e - ( inv-equiv - ( equiv-inclusion-is-full-subtype - ( is-inhabited-subtype-Prop ∘ subtype-equivalence-class R) - ( is-inhabited-subtype-equivalence-class R)))) + ( inv-equiv-inclusion-is-full-subtype + ( is-inhabited-subtype-Prop ∘ subtype-equivalence-class R) + ( is-inhabited-subtype-equivalence-class R))) ``` #### The equivalence relation obtained from a partition @@ -118,10 +117,7 @@ module _ ( Σ ( Σ ( block-partition P) ( λ B → is-in-block-partition P B x)) ( λ B → is-in-block-partition P (pr1 B) y)) - ( associative-Σ - ( block-partition P) - ( λ U → is-in-block-partition P U x) - ( λ U → is-in-block-partition P (pr1 U) y)) + ( associative-Σ) ( is-contr-Σ ( is-contr-block-containing-element-partition P x) ( Q , p) @@ -291,10 +287,7 @@ module _ ( ( left-unit-law-Σ-is-contr ( is-contr-block-containing-element-partition P a) ( center-block-containing-element-partition P a)) ∘e - ( inv-associative-Σ - ( block-partition P) - ( λ B → is-in-block-partition P B a) - ( λ B → is-in-block-partition P (pr1 B) x)))) ∘iff + ( inv-associative-Σ))) ∘iff ( K x)))) ( is-block-class-partition P a)) @@ -322,10 +315,7 @@ module _ ( is-contr-block-containing-element-partition P a) ( ( make-block-partition P Q H) , ( make-is-in-block-partition P Q H a q))) ∘e - ( inv-associative-Σ - ( block-partition P) - ( λ B → is-in-block-partition P B a) - ( λ B → is-in-block-partition P (pr1 B) x)))) ∘e + ( inv-associative-Σ))) ∘e ( compute-is-in-block-partition P Q H x))))) has-same-elements-partition-equivalence-relation-partition : diff --git a/src/foundation/intersections-subtypes.lagda.md b/src/foundation/intersections-subtypes.lagda.md index 9c7cbbe1ea..c4707736f9 100644 --- a/src/foundation/intersections-subtypes.lagda.md +++ b/src/foundation/intersections-subtypes.lagda.md @@ -137,7 +137,7 @@ abstract intersection-subtype P (intersection-subtype Q R) associative-intersection-subtype P Q R = eq-has-same-elements-subtype _ _ - ( λ _ → iff-equiv (associative-product _ _ _)) + ( λ _ → iff-equiv associative-product) ``` ### The intersection operation is idempotent diff --git a/src/foundation/invertible-maps.lagda.md b/src/foundation/invertible-maps.lagda.md index 47fb7cca31..fbd683270d 100644 --- a/src/foundation/invertible-maps.lagda.md +++ b/src/foundation/invertible-maps.lagda.md @@ -255,10 +255,7 @@ pr2 (pr2 (is-invertible-id-htpy-id-id A H)) = H triangle-is-invertible-id-htpy-id-id : {l : Level} (A : UU l) → ( is-invertible-id-htpy-id-id A) ~ - ( ( map-associative-Σ - ( A → A) - ( λ g → (id ∘ g) ~ id) - ( λ s → (pr1 s ∘ id) ~ id)) ∘ + ( ( map-associative-Σ) ∘ ( map-inv-left-unit-law-Σ-is-contr { B = λ s → (pr1 s ∘ id) ~ id} ( is-contr-section-is-equiv (is-equiv-id {_} {A})) @@ -271,10 +268,7 @@ abstract is-equiv-is-invertible-id-htpy-id-id A = is-equiv-left-map-triangle ( is-invertible-id-htpy-id-id A) - ( map-associative-Σ - ( A → A) - ( λ g → (id ∘ g) ~ id) - ( λ s → (pr1 s ∘ id) ~ id)) + ( map-associative-Σ) ( map-inv-left-unit-law-Σ-is-contr ( is-contr-section-is-equiv is-equiv-id) ( pair id refl-htpy)) @@ -282,7 +276,7 @@ abstract ( is-equiv-map-inv-left-unit-law-Σ-is-contr ( is-contr-section-is-equiv is-equiv-id) ( pair id refl-htpy)) - ( is-equiv-map-associative-Σ _ _ _) + ( is-equiv-map-associative-Σ) ``` ### The type of invertible maps is equivalent to the type of free loops on equivalences @@ -336,11 +330,7 @@ module _ equiv-is-retraction-section-is-invertible : (f : A → B) → Σ (section f) (λ g → (map-section f g) ∘ f ~ id) ≃ is-invertible f - equiv-is-retraction-section-is-invertible f = - associative-Σ - ( B → A) - ( λ g → f ∘ g ~ id) - ( λ g → (map-section f g) ∘ f ~ id) + equiv-is-retraction-section-is-invertible f = associative-Σ equiv-free-loop-equivalence-invertible-equivalence : free-loop (A ≃ B) ≃ Σ (A ≃ B) (is-invertible ∘ map-equiv) diff --git a/src/foundation/iterated-cartesian-product-types.lagda.md b/src/foundation/iterated-cartesian-product-types.lagda.md index e51230c990..8dfdd371b9 100644 --- a/src/foundation/iterated-cartesian-product-types.lagda.md +++ b/src/foundation/iterated-cartesian-product-types.lagda.md @@ -131,13 +131,8 @@ equiv-product-iterated-product-lists : equiv-product-iterated-product-lists nil q = left-unit-law-product-is-contr (is-contr-raise-unit) equiv-product-iterated-product-lists (cons x p) q = - ( ( equiv-product - ( id-equiv) - ( equiv-product-iterated-product-lists p q)) ∘e - ( associative-product - ( x) - ( iterated-product-lists p) - ( iterated-product-lists q))) + ( equiv-product-right (equiv-product-iterated-product-lists p q)) ∘e + ( associative-product) ``` ### Iterated cartesian product is closed under permutations diff --git a/src/foundation/logical-equivalences.lagda.md b/src/foundation/logical-equivalences.lagda.md index d806e1ca3d..8be286d75e 100644 --- a/src/foundation/logical-equivalences.lagda.md +++ b/src/foundation/logical-equivalences.lagda.md @@ -234,9 +234,9 @@ compute-fiber-iff-equiv : compute-fiber-iff-equiv {A = A} {B} (f , g) = ( equiv-tot (λ _ → equiv-funext)) ∘e ( left-unit-law-Σ-is-contr (is-torsorial-Id' f) (f , refl)) ∘e - ( inv-associative-Σ (A → B) (_＝ f) _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ _ → equiv-left-swap-Σ)) ∘e - ( associative-Σ (A → B) _ _) ∘e + ( associative-Σ) ∘e ( equiv-tot (λ e → equiv-pair-eq (iff-equiv e) (f , g))) ``` diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md index 11658b834b..a4076473e8 100644 --- a/src/foundation/partitions.lagda.md +++ b/src/foundation/partitions.lagda.md @@ -651,10 +651,7 @@ module _ ( refl)))) ∘e ( equiv-right-swap-Σ)) ∘e ( equiv-tot (λ ie → pr2 ie a)))) ∘e - ( associative-Σ - ( inhabited-subtype l2 A) - ( is-block-partition-Set-Indexed-Σ-Decomposition) - ( λ B → is-in-inhabited-subtype (pr1 B) a))) + ( associative-Σ)) ( is-torsorial-has-same-elements-inhabited-subtype ( pair ( λ x → diff --git a/src/foundation/product-decompositions-subuniverse.lagda.md b/src/foundation/product-decompositions-subuniverse.lagda.md index 8b340ce9dd..fa89797005 100644 --- a/src/foundation/product-decompositions-subuniverse.lagda.md +++ b/src/foundation/product-decompositions-subuniverse.lagda.md @@ -165,21 +165,15 @@ module _ binary-product-Decomposition-Subuniverse P X ≃ binary-product-Decomposition-Subuniverse P X equiv-commutative-binary-product-Decomposition-Subuniverse = - ( ( associative-Σ - ( type-subuniverse P) - ( λ _ → type-subuniverse P) - ( _)) ∘e - ( ( equiv-Σ - ( _) - ( commutative-product) - ( λ x → - equiv-postcomp-equiv - ( commutative-product) - (inclusion-subuniverse P X))) ∘e - ( ( inv-associative-Σ - ( type-subuniverse P) - ( λ _ → type-subuniverse P) - ( _))))) + ( associative-Σ) ∘e + ( ( equiv-Σ + ( _) + ( commutative-product) + ( λ x → + equiv-postcomp-equiv + ( commutative-product) + ( inclusion-subuniverse P X))) ∘e + ( inv-associative-Σ)) ``` ### Equivalence between iterated product and ternary product decomposition @@ -380,8 +374,8 @@ module _ ( eq-is-prop is-property-is-contr))) ( ( raise-unit l1 , C1) , is-contr-raise-unit)) ∘e - ( ( inv-associative-Σ _ _ _) ∘e + ( ( inv-associative-Σ) ∘e ( ( equiv-tot (λ _ → commutative-product)) ∘e - ( ( associative-Σ _ _ _)))))))) ∘e - ( ( associative-Σ _ _ _))) + ( associative-Σ))))))) ∘e + ( associative-Σ)) ``` diff --git a/src/foundation/relaxed-sigma-decompositions.lagda.md b/src/foundation/relaxed-sigma-decompositions.lagda.md index 521c531132..ffe2ba6f9b 100644 --- a/src/foundation/relaxed-sigma-decompositions.lagda.md +++ b/src/foundation/relaxed-sigma-decompositions.lagda.md @@ -612,10 +612,10 @@ module _ matching-correspondence-displayed-fibered-Relaxed-Σ-Decomposition = equivalence-reasoning A ≃ Σ X Y by e - ≃ Σ ( Σ U V) (λ uv → Y ((map-inv-equiv f) uv)) - by inv-equiv ( equiv-Σ-equiv-base Y (inv-equiv f)) - ≃ Σ U ( λ u → Σ (V u) (λ v → Y (map-inv-equiv f (u , v)))) - by associative-Σ U V (λ uv → Y (map-inv-equiv f uv)) + ≃ Σ (Σ U V) (λ uv → Y ((map-inv-equiv f) uv)) + by inv-equiv (equiv-Σ-equiv-base Y (inv-equiv f)) + ≃ Σ U (λ u → Σ (V u) (λ v → Y (map-inv-equiv f (u , v)))) + by associative-Σ map-displayed-fibered-Relaxed-Σ-Decomposition : displayed-Relaxed-Σ-Decomposition l4 (l3 ⊔ l5) l5 l3 A @@ -648,12 +648,10 @@ module _ matching-correspondence-inv-displayed-fibered-Relaxed-Σ-Decomposition = equivalence-reasoning A ≃ Σ M N by s - ≃ Σ M (λ m → Σ (P m) (Q m)) by equiv-Σ (λ m → Σ (P m) (Q m)) id-equiv t + ≃ Σ M (λ m → Σ (P m) (Q m)) + by equiv-tot t ≃ Σ (Σ M P) (λ (m , p) → Q m p) by inv-associative-Σ - ( M) - ( λ z → P z) - ( λ z → Q (pr1 z) (pr2 z)) map-inv-displayed-fibered-Relaxed-Σ-Decomposition : fibered-Relaxed-Σ-Decomposition (l2 ⊔ l4) l5 l2 l4 A @@ -748,14 +746,14 @@ module _ ( ap ( λ f → map-equiv (equiv-tot (inv-equiv ∘ t)) f) ( map-inv-eq-transpose-equiv - ( associative-Σ M P Y) + ( associative-Σ) ( inv ( map-eq-transpose-equiv ( equiv-Σ-equiv-base Y (inv-equiv id-equiv)) ( inv ( map-eq-transpose-equiv - ( associative-Σ M P Y) - ( is-section-map-inv-associative-Σ M P Y + ( associative-Σ) + ( is-section-map-inv-associative-Σ ( map-equiv (equiv-tot t ∘e s) x)))))))) ∙ ( inv ( preserves-comp-tot diff --git a/src/foundation/sigma-decompositions.lagda.md b/src/foundation/sigma-decompositions.lagda.md index 720de58abb..801d549a53 100644 --- a/src/foundation/sigma-decompositions.lagda.md +++ b/src/foundation/sigma-decompositions.lagda.md @@ -785,7 +785,7 @@ module _ ≃ Σ ( Σ U V) (λ uv → Y ((map-inv-equiv f) uv)) by inv-equiv ( equiv-Σ-equiv-base Y (inv-equiv f)) ≃ Σ U ( λ u → Σ (V u) (λ v → Y (map-inv-equiv f (u , v)))) - by associative-Σ U V (λ uv → Y (map-inv-equiv f uv)) + by associative-Σ map-displayed-fibered-Σ-Decomposition : displayed-Σ-Decomposition l4 (l3 ⊔ l5) l5 l3 A @@ -822,12 +822,10 @@ module _ matching-correspondence-inv-displayed-fibered-Σ-Decomposition = equivalence-reasoning A ≃ Σ M N by s - ≃ Σ M (λ m → Σ (P m) (Q m)) by equiv-Σ (λ m → Σ (P m) (Q m)) id-equiv t + ≃ Σ M (λ m → Σ (P m) (Q m)) + by equiv-Σ (λ m → Σ (P m) (Q m)) id-equiv t ≃ Σ (Σ M P) (λ (m , p) → Q m p) by inv-associative-Σ - ( M) - ( λ z → P z) - ( λ z → Q (pr1 z) (pr2 z)) map-inv-displayed-fibered-Σ-Decomposition : fibered-Σ-Decomposition (l2 ⊔ l4) l5 l2 l4 A @@ -929,14 +927,14 @@ module _ ( ap ( λ f → map-equiv (equiv-tot (inv-equiv ∘ t)) f) ( map-inv-eq-transpose-equiv - ( associative-Σ M P Y) + ( associative-Σ) ( inv ( map-eq-transpose-equiv ( equiv-Σ-equiv-base Y (inv-equiv id-equiv)) ( inv ( map-eq-transpose-equiv - ( associative-Σ M P Y) - ( is-section-map-inv-associative-Σ M P Y + ( associative-Σ) + ( is-section-map-inv-associative-Σ ( map-equiv (equiv-tot t ∘e s) x)))))))) ∙ ( inv ( preserves-comp-tot diff --git a/src/foundation/split-idempotent-maps.lagda.md b/src/foundation/split-idempotent-maps.lagda.md index 6935652587..502ec4df31 100644 --- a/src/foundation/split-idempotent-maps.lagda.md +++ b/src/foundation/split-idempotent-maps.lagda.md @@ -344,13 +344,7 @@ module _ Σ ( B retract-of A) ( λ (i , r , R) → i ∘ r ~ f))) ≃ Σ (A → A) (λ f → (Σ (retracts l2 A) (λ (B , i , r , R) → i ∘ r ~ f))) - by - equiv-tot - ( λ f → - inv-associative-Σ - ( UU l2) - ( _retract-of A) - ( λ (B , i , r , R) → i ∘ r ~ f)) + by equiv-tot (λ f → inv-associative-Σ) ≃ Σ (retracts l2 A) (λ (B , i , r , R) → Σ (A → A) (λ f → i ∘ r ~ f)) by equiv-left-swap-Σ ≃ retracts l2 A diff --git a/src/foundation/structured-type-duality.lagda.md b/src/foundation/structured-type-duality.lagda.md index cdbbcfc227..aeed20d718 100644 --- a/src/foundation/structured-type-duality.lagda.md +++ b/src/foundation/structured-type-duality.lagda.md @@ -43,10 +43,7 @@ equiv-Fiber-structure {l1} {l3} l P B = ( λ C → (b : B) → P (C b)) ( equiv-Fiber l B) ( λ f → equiv-Π-equiv-family (λ b → id-equiv)))) ∘e - ( inv-associative-Σ - ( UU (l1 ⊔ l)) - ( λ A → A → B) - ( λ f → structure-map P (pr2 f))) + ( inv-associative-Σ) ``` ```agda diff --git a/src/foundation/type-arithmetic-cartesian-product-types.lagda.md b/src/foundation/type-arithmetic-cartesian-product-types.lagda.md index a4461efe4c..108e57a1cc 100644 --- a/src/foundation/type-arithmetic-cartesian-product-types.lagda.md +++ b/src/foundation/type-arithmetic-cartesian-product-types.lagda.md @@ -69,31 +69,34 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (C : UU l3) + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where map-associative-product : (A × B) × C → A × (B × C) - map-associative-product = map-associative-Σ A (λ _ → B) (λ _ → C) + map-associative-product = map-associative-Σ map-inv-associative-product : A × (B × C) → (A × B) × C - map-inv-associative-product = map-inv-associative-Σ A (λ _ → B) (λ _ → C) + map-inv-associative-product = map-inv-associative-Σ is-section-map-inv-associative-product : (map-associative-product ∘ map-inv-associative-product) ~ id is-section-map-inv-associative-product = - is-section-map-inv-associative-Σ A (λ _ → B) (λ _ → C) + is-section-map-inv-associative-Σ is-retraction-map-inv-associative-product : (map-inv-associative-product ∘ map-associative-product) ~ id is-retraction-map-inv-associative-product = - is-retraction-map-inv-associative-Σ A (λ _ → B) (λ _ → C) + is-retraction-map-inv-associative-Σ is-equiv-map-associative-product : is-equiv map-associative-product is-equiv-map-associative-product = - is-equiv-map-associative-Σ A (λ _ → B) (λ _ → C) + is-equiv-map-associative-Σ associative-product : ((A × B) × C) ≃ (A × (B × C)) - associative-product = associative-Σ A (λ _ → B) (λ _ → C) + associative-product = associative-Σ + + inv-associative-product : (A × (B × C)) ≃ ((A × B) × C) + inv-associative-product = inv-associative-Σ ``` ### The unit laws of cartesian product types with respect to contractible types @@ -119,7 +122,8 @@ module _ left-unit-law-Σ-is-contr is-contr-A (center is-contr-A) inv-left-unit-law-product-is-contr : B ≃ A × B - inv-left-unit-law-product-is-contr = inv-equiv left-unit-law-product-is-contr + inv-left-unit-law-product-is-contr = + inv-left-unit-law-Σ-is-contr is-contr-A (center is-contr-A) is-equiv-pr2-product-is-contr : is-equiv (pr2 {B = λ _ → B}) is-equiv-pr2-product-is-contr = diff --git a/src/foundation/type-arithmetic-coproduct-types.lagda.md b/src/foundation/type-arithmetic-coproduct-types.lagda.md index 4bfa836a20..674b1e9e84 100644 --- a/src/foundation/type-arithmetic-coproduct-types.lagda.md +++ b/src/foundation/type-arithmetic-coproduct-types.lagda.md @@ -34,7 +34,7 @@ themselves, cartesian products, and dependent pair types. ```agda module _ - {l1 l2 : Level} (A : UU l1) (B : UU l2) + {l1 l2 : Level} {A : UU l1} {B : UU l2} where map-commutative-coproduct : A + B → B + A @@ -124,7 +124,7 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (C : A + B → UU l3) + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : A + B → UU l3) where map-right-distributive-Σ-coproduct : @@ -134,10 +134,8 @@ module _ map-inv-right-distributive-Σ-coproduct : (Σ A (λ x → C (inl x))) + (Σ B (λ y → C (inr y))) → Σ (A + B) C - pr1 (map-inv-right-distributive-Σ-coproduct (inl (x , z))) = inl x - pr2 (map-inv-right-distributive-Σ-coproduct (inl (x , z))) = z - pr1 (map-inv-right-distributive-Σ-coproduct (inr (y , z))) = inr y - pr2 (map-inv-right-distributive-Σ-coproduct (inr (y , z))) = z + map-inv-right-distributive-Σ-coproduct (inl (x , z)) = (inl x , z) + map-inv-right-distributive-Σ-coproduct (inr (y , z)) = (inr y , z) is-section-map-inv-right-distributive-Σ-coproduct : ( map-right-distributive-Σ-coproduct ∘ @@ -153,27 +151,40 @@ module _ is-retraction-map-inv-right-distributive-Σ-coproduct (inl x , z) = refl is-retraction-map-inv-right-distributive-Σ-coproduct (inr y , z) = refl - abstract - is-equiv-map-right-distributive-Σ-coproduct : - is-equiv map-right-distributive-Σ-coproduct - is-equiv-map-right-distributive-Σ-coproduct = - is-equiv-is-invertible - map-inv-right-distributive-Σ-coproduct - is-section-map-inv-right-distributive-Σ-coproduct - is-retraction-map-inv-right-distributive-Σ-coproduct + is-equiv-map-right-distributive-Σ-coproduct : + is-equiv map-right-distributive-Σ-coproduct + is-equiv-map-right-distributive-Σ-coproduct = + is-equiv-is-invertible + map-inv-right-distributive-Σ-coproduct + is-section-map-inv-right-distributive-Σ-coproduct + is-retraction-map-inv-right-distributive-Σ-coproduct right-distributive-Σ-coproduct : Σ (A + B) C ≃ ((Σ A (λ x → C (inl x))) + (Σ B (λ y → C (inr y)))) - pr1 right-distributive-Σ-coproduct = map-right-distributive-Σ-coproduct - pr2 right-distributive-Σ-coproduct = - is-equiv-map-right-distributive-Σ-coproduct + right-distributive-Σ-coproduct = + ( map-right-distributive-Σ-coproduct , + is-equiv-map-right-distributive-Σ-coproduct) + + is-equiv-map-inv-right-distributive-Σ-coproduct : + is-equiv map-inv-right-distributive-Σ-coproduct + is-equiv-map-inv-right-distributive-Σ-coproduct = + is-equiv-is-invertible + map-right-distributive-Σ-coproduct + is-retraction-map-inv-right-distributive-Σ-coproduct + is-section-map-inv-right-distributive-Σ-coproduct + + inv-right-distributive-Σ-coproduct : + ((Σ A (λ x → C (inl x))) + (Σ B (λ y → C (inr y)))) ≃ Σ (A + B) C + inv-right-distributive-Σ-coproduct = + ( map-inv-right-distributive-Σ-coproduct , + is-equiv-map-inv-right-distributive-Σ-coproduct) ``` ### Left distributivity of Σ over coproducts ```agda module _ - {l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (C : A → UU l3) + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} where map-left-distributive-Σ-coproduct : @@ -212,85 +223,103 @@ module _ left-distributive-Σ-coproduct : Σ A (λ x → B x + C x) ≃ ((Σ A B) + (Σ A C)) - pr1 left-distributive-Σ-coproduct = map-left-distributive-Σ-coproduct - pr2 left-distributive-Σ-coproduct = is-equiv-map-left-distributive-Σ-coproduct + left-distributive-Σ-coproduct = + ( map-left-distributive-Σ-coproduct , + is-equiv-map-left-distributive-Σ-coproduct) + + is-equiv-map-inv-left-distributive-Σ-coproduct : + is-equiv map-inv-left-distributive-Σ-coproduct + is-equiv-map-inv-left-distributive-Σ-coproduct = + is-equiv-is-invertible + map-left-distributive-Σ-coproduct + is-retraction-map-inv-left-distributive-Σ-coproduct + is-section-map-inv-left-distributive-Σ-coproduct + + inv-left-distributive-Σ-coproduct : + ((Σ A B) + (Σ A C)) ≃ Σ A (λ x → B x + C x) + inv-left-distributive-Σ-coproduct = + ( map-inv-left-distributive-Σ-coproduct , + is-equiv-map-inv-left-distributive-Σ-coproduct) ``` ### Right distributivity of products over coproducts ```agda module _ - {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (C : UU l3) + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where map-right-distributive-product-coproduct : (A + B) × C → (A × C) + (B × C) map-right-distributive-product-coproduct = - map-right-distributive-Σ-coproduct A B (λ _ → C) + map-right-distributive-Σ-coproduct (λ _ → C) map-inv-right-distributive-product-coproduct : (A × C) + (B × C) → (A + B) × C map-inv-right-distributive-product-coproduct = - map-inv-right-distributive-Σ-coproduct A B (λ _ → C) + map-inv-right-distributive-Σ-coproduct (λ _ → C) is-section-map-inv-right-distributive-product-coproduct : map-right-distributive-product-coproduct ∘ map-inv-right-distributive-product-coproduct ~ id is-section-map-inv-right-distributive-product-coproduct = - is-section-map-inv-right-distributive-Σ-coproduct A B (λ _ → C) + is-section-map-inv-right-distributive-Σ-coproduct (λ _ → C) is-retraction-map-inv-right-distributive-product-coproduct : map-inv-right-distributive-product-coproduct ∘ map-right-distributive-product-coproduct ~ id is-retraction-map-inv-right-distributive-product-coproduct = - is-retraction-map-inv-right-distributive-Σ-coproduct A B (λ _ → C) + is-retraction-map-inv-right-distributive-Σ-coproduct (λ _ → C) - abstract - is-equiv-map-right-distributive-product-coproduct : - is-equiv map-right-distributive-product-coproduct - is-equiv-map-right-distributive-product-coproduct = - is-equiv-map-right-distributive-Σ-coproduct A B (λ _ → C) + is-equiv-map-right-distributive-product-coproduct : + is-equiv map-right-distributive-product-coproduct + is-equiv-map-right-distributive-product-coproduct = + is-equiv-map-right-distributive-Σ-coproduct (λ _ → C) right-distributive-product-coproduct : ((A + B) × C) ≃ ((A × C) + (B × C)) right-distributive-product-coproduct = - right-distributive-Σ-coproduct A B (λ _ → C) + right-distributive-Σ-coproduct (λ _ → C) + + inv-right-distributive-product-coproduct : ((A × C) + (B × C)) ≃ ((A + B) × C) + inv-right-distributive-product-coproduct = + inv-right-distributive-Σ-coproduct (λ _ → C) ``` ### Left distributivity of products over coproducts ```agda module _ - {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (C : UU l3) + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where map-left-distributive-product-coproduct : A × (B + C) → (A × B) + (A × C) map-left-distributive-product-coproduct = - map-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C) + map-left-distributive-Σ-coproduct map-inv-left-distributive-product-coproduct : (A × B) + (A × C) → A × (B + C) map-inv-left-distributive-product-coproduct = - map-inv-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C) + map-inv-left-distributive-Σ-coproduct is-section-map-inv-left-distributive-product-coproduct : map-left-distributive-product-coproduct ∘ map-inv-left-distributive-product-coproduct ~ id is-section-map-inv-left-distributive-product-coproduct = - is-section-map-inv-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C) + is-section-map-inv-left-distributive-Σ-coproduct is-retraction-map-inv-left-distributive-product-coproduct : map-inv-left-distributive-product-coproduct ∘ map-left-distributive-product-coproduct ~ id is-retraction-map-inv-left-distributive-product-coproduct = - is-retraction-map-inv-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C) + is-retraction-map-inv-left-distributive-Σ-coproduct is-equiv-map-left-distributive-product-coproduct : is-equiv map-left-distributive-product-coproduct is-equiv-map-left-distributive-product-coproduct = - is-equiv-map-left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C) + is-equiv-map-left-distributive-Σ-coproduct left-distributive-product-coproduct : (A × (B + C)) ≃ ((A × B) + (A × C)) left-distributive-product-coproduct = - left-distributive-Σ-coproduct A (λ _ → B) (λ _ → C) + left-distributive-Σ-coproduct ``` ### If a coproduct is contractible then one summand is contractible and the other is empty diff --git a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md index 022b2dc3a8..d4404bbcdb 100644 --- a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md +++ b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md @@ -168,7 +168,7 @@ formalize both ways. ```agda module _ - {l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (C : Σ A B → UU l3) + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} where map-associative-Σ : Σ (Σ A B) C → Σ A (λ x → Σ (B x) (λ y → C (x , y))) @@ -400,17 +400,25 @@ module _ ### Distributive laws of cartesian products over Σ ```agda -left-distributive-product-Σ : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3} → - (A × (Σ B C)) ≃ Σ B (λ b → A × (C b)) -left-distributive-product-Σ = - equiv-left-swap-Σ - -right-distributive-product-Σ : - {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} → - ((Σ A B) × C) ≃ Σ A (λ a → B a × C) -right-distributive-product-Σ {A} = - associative-Σ _ _ _ +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3} + where + + left-distributive-product-Σ : A × (Σ B C) ≃ Σ B (λ b → A × (C b)) + left-distributive-product-Σ = equiv-left-swap-Σ + + inv-left-distributive-product-Σ : Σ B (λ b → A × (C b)) ≃ A × (Σ B C) + inv-left-distributive-product-Σ = equiv-left-swap-Σ + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} + where + + right-distributive-product-Σ : (Σ A B) × C ≃ Σ A (λ a → B a × C) + right-distributive-product-Σ = associative-Σ + + inv-right-distributive-product-Σ : Σ A (λ a → B a × C) ≃ (Σ A B) × C + inv-right-distributive-product-Σ = inv-associative-Σ ``` ## See also diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md index b73510b8b4..767ae78258 100644 --- a/src/graph-theory/walks-undirected-graphs.lagda.md +++ b/src/graph-theory/walks-undirected-graphs.lagda.md @@ -194,10 +194,7 @@ module _ ( equiv-is-contr ( is-torsorial-Id (other-element-unordered-pair p y)) ( is-contr-unit))) ∘e - ( left-distributive-Σ-coproduct - ( vertex-Undirected-Graph G) - ( is-vertex-on-walk-Undirected-Graph G w) - ( λ z → other-element-unordered-pair p y ＝ z)) + ( left-distributive-Σ-coproduct) ``` ### The type of edges on a constant walk is empty @@ -233,10 +230,7 @@ module _ ( equiv-is-contr ( is-torsorial-Id (pair p e)) ( is-contr-unit))) ∘e - ( left-distributive-Σ-coproduct - ( total-edge-Undirected-Graph G) - ( is-edge-on-walk-Undirected-Graph' G w) - ( λ z → pair p e ＝ z)) + ( left-distributive-Σ-coproduct) ``` ### Right unit law for concatenation of walks diff --git a/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md b/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md index fccff9b2a3..52163be19a 100644 --- a/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md +++ b/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md @@ -55,10 +55,7 @@ module _ ( action-stabilizer-action-Concrete-Group x) is-transitive-action-stabilizer-action-Concrete-Group x = is-0-connected-equiv' - ( associative-Σ - ( classifying-type-Concrete-Group G) - ( type-Set ∘ X) - ( mere-eq (shape-Concrete-Group G , x))) + ( associative-Σ) ( is-0-connected-mere-eq ( ( shape-Concrete-Group G , x) , ( refl-mere-eq (shape-Concrete-Group G , x))) diff --git a/src/group-theory/sums-of-finite-families-of-elements-commutative-monoids.lagda.md b/src/group-theory/sums-of-finite-families-of-elements-commutative-monoids.lagda.md index 2db27e6e13..87f4c78b61 100644 --- a/src/group-theory/sums-of-finite-families-of-elements-commutative-monoids.lagda.md +++ b/src/group-theory/sums-of-finite-families-of-elements-commutative-monoids.lagda.md @@ -585,10 +585,7 @@ module _ map-coproduct ( id) ( map-left-unit-law-Σ (type-Finite-Type ∘ B ∘ inr)) ∘ - map-right-distributive-Σ-coproduct - ( Fin n) - ( unit) - ( type-Finite-Type ∘ B)) + map-right-distributive-Σ-coproduct (type-Finite-Type ∘ B)) by sum-equiv-finite-Commutative-Monoid ( M) @@ -600,10 +597,7 @@ module _ ( equiv-coproduct ( id-equiv) ( left-unit-law-Σ (type-Finite-Type ∘ B ∘ inr)) ∘e - right-distributive-Σ-coproduct - ( Fin n) - ( unit) - ( type-Finite-Type ∘ B))) + right-distributive-Σ-coproduct (type-Finite-Type ∘ B))) _ ＝ sum-finite-Commutative-Monoid diff --git a/src/logic/complements-decidable-subtypes.lagda.md b/src/logic/complements-decidable-subtypes.lagda.md index 44304ffbcd..3af0d7621b 100644 --- a/src/logic/complements-decidable-subtypes.lagda.md +++ b/src/logic/complements-decidable-subtypes.lagda.md @@ -130,8 +130,5 @@ module _ ( is-prop-is-decidable (is-prop-is-in-decidable-subtype P x)) ( is-decidable-decidable-subtype P x)) ≃ type-decidable-subtype P + type-complement-decidable-subtype P - by - left-distributive-Σ-coproduct A - ( is-in-decidable-subtype P) - ( is-in-complement-decidable-subtype P) + by left-distributive-Σ-coproduct ``` diff --git a/src/metric-spaces/equality-of-pseudometric-spaces.lagda.md b/src/metric-spaces/equality-of-pseudometric-spaces.lagda.md index e92824c132..5be6a0ba7f 100644 --- a/src/metric-spaces/equality-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/equality-of-pseudometric-spaces.lagda.md @@ -211,10 +211,7 @@ module _ equiv-tot ( λ e → equiv-eq (ap (is-isometry-Pseudometric-Space A B) refl)))) ∘e - ( associative-Σ - ( type-function-Pseudometric-Space A B) - ( is-equiv) - ( is-isometry-Pseudometric-Space A B ∘ map-equiv)) + ( associative-Σ) ``` ### Isometric equivalences between pseudometric spaces characterize their equality diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md index a57d55d1a2..ba315c5ba8 100644 --- a/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md +++ b/src/metric-spaces/precategory-of-metric-spaces-and-isometries.lagda.md @@ -110,12 +110,9 @@ module _ iso-Precategory precategory-isometry-Metric-Space A B ≃ isometric-equiv-Metric-Space' A B equiv-iso-isometric-equiv-Metric-Space' = - equiv-tot (λ f → commutative-product) ∘e - associative-Σ - ( type-function-Metric-Space A B) - ( is-isometry-Metric-Space A B) - ( is-equiv ∘ map-isometry-Metric-Space A B) ∘e - equiv-tot + ( equiv-tot (λ f → commutative-product)) ∘e + ( associative-Σ) ∘e + ( equiv-tot ( λ f → equiv-iff ( is-iso-prop-Precategory @@ -126,7 +123,7 @@ module _ ( is-equiv-Prop ( map-isometry-Metric-Space A B f)) ( is-equiv-is-iso-isometry-Metric-Space A B f) - ( is-iso-is-equiv-isometry-Metric-Space A B f)) + ( is-iso-is-equiv-isometry-Metric-Space A B f))) ``` ## See also diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md index af0a7e0b14..564a2b9385 100644 --- a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md +++ b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md @@ -236,12 +236,9 @@ module _ iso-Precategory precategory-short-function-Metric-Space A B ≃ isometric-equiv-Metric-Space' A B equiv-isometric-equiv-iso-short-function-Metric-Space' = - equiv-tot - ( equiv-is-isometric-equiv-is-iso-short-function-Metric-Space A B) ∘e - associative-Σ - ( type-function-Metric-Space A B) - ( is-short-function-Metric-Space A B) - ( is-iso-Precategory precategory-short-function-Metric-Space {A} {B}) + ( equiv-tot + ( equiv-is-isometric-equiv-is-iso-short-function-Metric-Space A B)) ∘e + ( associative-Σ) ``` ## See also diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md index 5a982e30d8..31caeafe92 100644 --- a/src/ring-theory/isomorphisms-rings.lagda.md +++ b/src/ring-theory/isomorphisms-rings.lagda.md @@ -446,16 +446,9 @@ module _ equiv-iso-ab-iso-Ring : iso-Ring R S ≃ iso-ab-Ring equiv-iso-ab-iso-Ring = - ( inv-equiv - ( associative-Σ - ( hom-Ab (ab-Ring R) (ab-Ring S)) - ( is-iso-Ab (ab-Ring R) (ab-Ring S)) - ( λ f → is-ring-homomorphism-hom-Ab R S (pr1 f)))) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ f → commutative-product)) ∘e - ( associative-Σ - ( hom-Ab (ab-Ring R) (ab-Ring S)) - ( is-ring-homomorphism-hom-Ab R S) - ( λ f → is-iso-Ab (ab-Ring R) (ab-Ring S) (pr1 f))) ∘e + ( associative-Σ) ∘e ( equiv-type-subtype ( is-prop-is-iso-Ring R S) ( λ f → is-prop-is-iso-Ab (ab-Ring R) (ab-Ring S) (hom-ab-hom-Ring R S f)) diff --git a/src/set-theory/russells-paradox.lagda.md b/src/set-theory/russells-paradox.lagda.md index 9ca07432a8..40800d3405 100644 --- a/src/set-theory/russells-paradox.lagda.md +++ b/src/set-theory/russells-paradox.lagda.md @@ -134,7 +134,7 @@ paradox-Russell {l} H = { B = λ t → (pr1 t) ∉-𝕍 (pr1 t)} ( is-torsorial-Id' R') ( pair R' refl)) ∘e - ( ( inv-associative-Σ (𝕍 l) (_＝ R') (λ t → (pr1 t) ∉-𝕍 (pr1 t))) ∘e + ( ( inv-associative-Σ) ∘e ( ( equiv-tot ( λ t → ( commutative-product) ∘e @@ -146,14 +146,7 @@ paradox-Russell {l} H = ( eq-resize-𝕍 ( is-small-multiset-𝕍 is-small-lsuc t) ( is-small-R'))))))) ∘e - ( associative-Σ - ( 𝕍 l) - ( λ t → t ∉-𝕍 t) - ( λ t → - ( resize-𝕍 - ( pr1 t) - ( is-small-multiset-𝕍 is-small-lsuc (pr1 t))) ＝ - ( R)))))) + ( associative-Σ)))) ``` ### There can be no surjective map `f : A → 𝒰` for any `A : 𝒰` diff --git a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md index 0f5ad3fad1..78ca0ad5d9 100644 --- a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md +++ b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md @@ -144,10 +144,10 @@ module _ ( equiv-tot ( λ D → ( equiv-product-right inv-distributive-Π-Σ) ∘e - ( inv-equiv right-distributive-product-Σ) ∘e - ( equiv-tot (λ _ → inv-equiv left-distributive-product-Σ)) ∘e - ( associative-Σ _ _ _))) ∘e - ( associative-Σ _ _ _) ∘e + ( inv-right-distributive-product-Σ) ∘e + ( equiv-tot (λ _ → inv-left-distributive-product-Σ)) ∘e + ( associative-Σ))) ∘e + ( associative-Σ) ∘e ( equiv-Σ-equiv-base ( _) ( ( equiv-remove-redundant-prop @@ -166,7 +166,7 @@ module _ ( commutative-product) ∘e ( equiv-tot ( λ p → equiv-total-is-in-subuniverse-Σ-Decomposition P (X , p))))) ∘e - ( inv-associative-Σ _ _ _) + ( inv-associative-Σ) ``` ### Unit laws for Cauchy composition of species-subuniverse diff --git a/src/species/cauchy-composition-species-of-types.lagda.md b/src/species/cauchy-composition-species-of-types.lagda.md index 7e66fba693..77c926b381 100644 --- a/src/species/cauchy-composition-species-of-types.lagda.md +++ b/src/species/cauchy-composition-species-of-types.lagda.md @@ -78,7 +78,7 @@ left-unit-law-cauchy-composition-species-types {l1} F A = ( is-contr-type-trivial-Relaxed-Σ-Decomposition) ( trivial-Relaxed-Σ-Decomposition l1 A , is-trivial-trivial-Relaxed-Σ-Decomposition {l1} {l1} {A})) ∘e - ( ( inv-associative-Σ _ _ _) ∘e + ( ( inv-associative-Σ) ∘e ( ( equiv-tot ( λ D → equiv-tot (λ C → left-unit-law-Π-is-contr C (center C)))))) @@ -91,7 +91,7 @@ right-unit-law-cauchy-composition-species-types {l1} F A = ( is-contr-type-discrete-Relaxed-Σ-Decomposition) ( ( discrete-Relaxed-Σ-Decomposition l1 A) , is-discrete-discrete-Relaxed-Σ-Decomposition)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ _ → commutative-product)) ``` @@ -118,10 +118,10 @@ module _ equiv-associative-cauchy-composition-species-types A = ( equiv-tot ( λ D1 → - ( inv-equiv right-distributive-product-Σ) ∘e + ( inv-right-distributive-product-Σ) ∘e ( equiv-tot ( λ D2 → - ( inv-associative-Σ _ _ _))) ∘e + ( inv-associative-Σ))) ∘e ( equiv-tot ( λ D2 → ( equiv-product-right @@ -134,10 +134,10 @@ module _ ( λ x → U (cotype-Relaxed-Σ-Decomposition D1 x)))) ∘e ( equiv-ind-Σ))) ∘e ( distributive-Π-Σ))))))) ∘e - ( associative-Σ _ _ _) ∘e + ( associative-Σ) ∘e ( equiv-Σ-equiv-base _ ( inv-equiv equiv-displayed-fibered-Relaxed-Σ-Decomposition)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot ( λ D → left-distributive-product-Σ ∘e equiv-product-right distributive-Π-Σ)) diff --git a/src/species/cauchy-exponentials-species-of-types.lagda.md b/src/species/cauchy-exponentials-species-of-types.lagda.md index 8ef9626dde..eafbf24565 100644 --- a/src/species/cauchy-exponentials-species-of-types.lagda.md +++ b/src/species/cauchy-exponentials-species-of-types.lagda.md @@ -121,7 +121,7 @@ module _ ( compute-right-equiv-binary-coproduct-Decomposition-Σ-Decomposition ( D) ( b')))))))) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ d → distributive-Π-coproduct-binary-coproduct-Decomposition)) where reassociate : diff --git a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md index 7f48882226..0f01710cdb 100644 --- a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md +++ b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md @@ -165,15 +165,15 @@ module _ P X d)))) ( ( equiv-Σ ( _) - ( associative-product _ _ _ ∘e commutative-product) + ( associative-product ∘e commutative-product) ( λ x → equiv-postcomp-equiv - ( associative-coproduct ∘e commutative-coproduct _ _) + ( associative-coproduct ∘e commutative-coproduct) ( inclusion-subuniverse P X))) ∘e ( equiv-ternary-left-iterated-coproduct-Decomposition-subuniverse P X C2)) - ( λ d → associative-product _ _ _)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( λ d → associative-product)) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ d → right-distributive-product-Σ)) equiv-right-iterated-cauchy-product-species-subuniverse : @@ -200,7 +200,7 @@ module _ ( _) ( equiv-ternary-right-iterated-coproduct-Decomposition-subuniverse P X C2)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ d → left-distributive-product-Σ)) equiv-associative-cauchy-product-species-subuniverse : @@ -324,7 +324,7 @@ module _ P X C2)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ _ → commutative-product)) equiv-left-unit-law-cauchy-product-species-subuniverse : diff --git a/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md index 1e6f11e40a..4617313292 100644 --- a/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md +++ b/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md @@ -63,7 +63,7 @@ module _ cauchy-series-species-subuniverse ≃ cauchy-series-species-types (Σ-extension-species-subuniverse P Q S) X equiv-cauchy-series-Σ-extension-species-subuniverse = - (equiv-tot (λ U → inv-associative-Σ _ _ _)) ∘e (associative-Σ _ _ _) + (equiv-tot (λ U → inv-associative-Σ)) ∘e (associative-Σ) ``` ### Equivalences diff --git a/src/species/composition-cauchy-series-species-of-types.lagda.md b/src/species/composition-cauchy-series-species-of-types.lagda.md index 50802c15ad..f0bca1e821 100644 --- a/src/species/composition-cauchy-series-species-of-types.lagda.md +++ b/src/species/composition-cauchy-series-species-of-types.lagda.md @@ -66,7 +66,7 @@ module _ ( equiv-tot ( λ U → ( equiv-product-right inv-distributive-Π-Σ) ∘e - ( inv-equiv left-distributive-product-Σ) ∘e + ( inv-left-distributive-product-Σ) ∘e ( equiv-tot ( λ V → ( equiv-product-right diff --git a/src/species/dirichlet-exponentials-species-of-types.lagda.md b/src/species/dirichlet-exponentials-species-of-types.lagda.md index 8fdc9897a6..dccfe72288 100644 --- a/src/species/dirichlet-exponentials-species-of-types.lagda.md +++ b/src/species/dirichlet-exponentials-species-of-types.lagda.md @@ -99,7 +99,7 @@ module _ ( compute-right-equiv-binary-product-Decomposition-Π-Decomposition ( D) ( b')))))))) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ d → distributive-Π-coproduct-binary-coproduct-Decomposition)) where reassociate : diff --git a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md index 1a872f00c7..b77419e7b6 100644 --- a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md +++ b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md @@ -183,18 +183,17 @@ module _ d)))) ( equiv-Σ ( _) - ( associative-product _ _ _ ∘e commutative-product) + ( associative-product ∘e commutative-product) ( λ x → equiv-postcomp-equiv - ( ( associative-product _ _ _ ∘e - ( commutative-product))) + ( associative-product ∘e commutative-product) ( inclusion-subuniverse P X)) ∘e equiv-ternary-left-iterated-product-Decomposition-Subuniverse P X C2) - ( λ d → associative-product _ _ _)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( λ d → associative-product)) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ d → right-distributive-product-Σ)) equiv-right-iterated-dirichlet-product-species-subuniverse : @@ -232,7 +231,7 @@ module _ P X C2)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( ( equiv-tot (λ d → left-distributive-product-Σ))) equiv-associative-dirichlet-product-species-subuniverse : @@ -357,7 +356,7 @@ module _ P X C2)) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ _ → commutative-product)) equiv-left-unit-law-dirichlet-product-species-subuniverse : diff --git a/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md index 0988bc7cc7..d3eee985d6 100644 --- a/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md +++ b/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md @@ -116,10 +116,10 @@ module _ ( equiv-tot ( λ D → ( equiv-product-right inv-distributive-Π-Σ) ∘e - ( inv-equiv right-distributive-product-Σ) ∘e - ( equiv-tot (λ _ → inv-equiv left-distributive-product-Σ)) ∘e - ( associative-Σ _ _ _))) ∘e - ( associative-Σ _ _ _) ∘e + ( inv-right-distributive-product-Σ) ∘e + ( equiv-tot (λ _ → inv-left-distributive-product-Σ)) ∘e + ( associative-Σ))) ∘e + ( associative-Σ) ∘e ( equiv-Σ-equiv-base ( _) ( ( equiv-remove-redundant-prop @@ -138,7 +138,7 @@ module _ ( commutative-product) ∘e ( equiv-tot ( λ p → equiv-total-is-in-subuniverse-Σ-Decomposition P (X , p))))) ∘e - ( inv-associative-Σ _ _ _) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ p → inv-equiv (equiv-is-small (C1 S T (X , p))))) ``` diff --git a/src/structured-types/h-spaces.lagda.md b/src/structured-types/h-spaces.lagda.md index be217b8539..156a5f15c5 100644 --- a/src/structured-types/h-spaces.lagda.md +++ b/src/structured-types/h-spaces.lagda.md @@ -194,5 +194,5 @@ module _ ( equiv-funext) ( λ _ → equiv-tot (λ _ → inv-equiv (equiv-right-whisker-concat refl))))) ∘e - ( associative-Σ _ _ _) + ( associative-Σ) ``` diff --git a/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md b/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md index 8b2ed00fc2..b08f68dd4c 100644 --- a/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md @@ -91,20 +91,7 @@ module _ ( B)) ( x , r) ＝ ( x , r))) - by - associative-Σ - ( type-family-with-descent-data-circle A) - ( type-double-family-with-dependent-descent-data-circle A B) - ( λ u → - map-Σ - ( type-double-family-with-dependent-descent-data-circle A B) - ( map-aut-family-with-descent-data-circle A) - ( λ x → - map-dependent-automorphism-double-family-with-dependent-descent-data-circle - ( A) - ( B)) - ( u) ＝ - u) + by associative-Σ ≃ Σ ( type-family-with-descent-data-circle A) ( λ x → ( is-in-subtype subtype-descent-data-circle-subtype x) × @@ -126,11 +113,7 @@ module _ ≃ Σ ( fixpoint-descent-data-circle ( descent-data-family-with-descent-data-circle A)) ( λ x → is-in-subtype subtype-descent-data-circle-subtype (pr1 x)) - by - inv-associative-Σ - ( type-family-with-descent-data-circle A) - ( λ x → map-aut-family-with-descent-data-circle A x ＝ x) - ( λ x → is-in-subtype subtype-descent-data-circle-subtype (pr1 x)) + by inv-associative-Σ equiv-section-descent-data-circle-subtype-fixpoint-in-subtype : dependent-universal-property-circle l → diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md index abddcc385a..a42dcdfe4c 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md @@ -167,8 +167,6 @@ module _ ( horizontal-map-span-cocone-cofork a) ( cocone-codiagonal-cofork a e)) ( right-distributive-Σ-coproduct - ( domain-double-arrow a) - ( domain-double-arrow a) ( ( P) ∘ ( horizontal-map-cocone-cofork a e) ∘ ( vertical-map-span-cocone-cofork a))) diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md index 1e014f974d..f3580c570c 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md @@ -123,14 +123,8 @@ module _ ( cofork-cocone-sequential-diagram c)) pr1 equiv-double-arrow-flattening-lemma-sequential-colimit = inv-associative-Σ - ( ℕ) - ( family-sequential-diagram A) - ( P ∘ ind-Σ (map-cocone-sequential-diagram c)) pr1 (pr2 equiv-double-arrow-flattening-lemma-sequential-colimit) = inv-associative-Σ - ( ℕ) - ( family-sequential-diagram A) - ( P ∘ ind-Σ (map-cocone-sequential-diagram c)) pr1 (pr2 (pr2 equiv-double-arrow-flattening-lemma-sequential-colimit)) = refl-htpy pr2 (pr2 (pr2 equiv-double-arrow-flattening-lemma-sequential-colimit)) = diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md index 10609483e0..4ad46b4c42 100644 --- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md +++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md @@ -219,11 +219,7 @@ module _ ( ( ( left-unit-law-Σ-is-contr ( is-torsorial-Id' (a ∙ a)) ( a ∙ a , refl)) ∘e - ( inv-associative-Σ - ( type-Ω (Ω A)) - ( λ b → b ＝ (a ∙ a)) - ( λ bq → - power-nat-Ω 5 (Ω A) a ＝ power-nat-Ω 3 (Ω A) (pr1 bq)))) ∘e + ( inv-associative-Σ)) ∘e ( equiv-tot ( λ b → ( commutative-product) ∘e diff --git a/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md b/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md index bab47be956..5e81600a0b 100644 --- a/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md @@ -156,12 +156,7 @@ module _ ℤ-Pointed-Type-With-Aut)))) ( is-equiv-id)))) ∘e ( ( equiv-right-swap-Σ) ∘e - ( ( associative-Σ - ( ℤ ≃ ℤ) - ( λ e → Id (map-equiv e zero-ℤ) zero-ℤ) - ( λ e → - ( map-equiv (pr1 e) ∘ succ-ℤ) ~ - ( succ-ℤ ∘ map-equiv (pr1 e)))) ∘e + ( ( associative-Σ) ∘e ( ( equiv-right-swap-Σ) ∘e ( equiv-Σ ( λ e → Id (map-equiv (pr1 e) zero-ℤ) zero-ℤ) 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 a8b0a7025c..a130c79464 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 @@ -146,19 +146,9 @@ module _ ( left-unit-law-Σ-is-contr ( is-torsorial-Id (point-Pointed-Type Y)) ( point-Pointed-Type Y , refl)) ∘e - ( inv-associative-Σ - ( type-Pointed-Type Y) - ( λ z → point-Pointed-Type Y ＝ z) - ( λ t → - Σ ( type-Pointed-Type X → point-Pointed-Type Y ＝ pr1 t) - ( λ f → f (point-Pointed-Type X) ＝ pr2 t))) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot (λ y1 → equiv-left-swap-Σ)) ∘e - ( associative-Σ - ( type-Pointed-Type Y) - ( λ y1 → type-Pointed-Type X → point-Pointed-Type Y ＝ y1) - ( λ z → - Σ ( point-Pointed-Type Y ＝ pr1 z) - ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e + ( associative-Σ) ∘e ( inv-right-unit-law-Σ-is-contr ( λ z → is-torsorial-Id (pr2 z (point-Pointed-Type X)))) ∘e ( left-unit-law-Σ-is-contr diff --git a/src/trees/directed-trees.lagda.md b/src/trees/directed-trees.lagda.md index 5c60f5b264..576a4937af 100644 --- a/src/trees/directed-trees.lagda.md +++ b/src/trees/directed-trees.lagda.md @@ -476,11 +476,7 @@ module _ ( y , e)) ≃ Σ ( Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x)) ( λ p → walk-Directed-Graph G (pr1 p) r) - by - inv-associative-Σ - ( vertex-Directed-Graph G) - ( edge-Directed-Graph G x) - ( λ p → walk-Directed-Graph G (pr1 p) r) + by inv-associative-Σ ≃ walk-Directed-Graph G y r by left-unit-law-Σ-is-contr diff --git a/src/trees/extensional-w-types.lagda.md b/src/trees/extensional-w-types.lagda.md index 257d84375e..87ffe47bce 100644 --- a/src/trees/extensional-w-types.lagda.md +++ b/src/trees/extensional-w-types.lagda.md @@ -135,10 +135,7 @@ module _ ( equiv-tot ( λ g → inv-equiv (equiv-fam-equiv-equiv-slice f g)))))) ∘e - ( associative-Σ - ( A) - ( λ x → B x → 𝕎 A B) - ( λ t → Eq-ext-𝕎 (tree-𝕎 a f) (tree-𝕎 (pr1 t) (pr2 t))))) ∘e + ( associative-Σ)) ∘e ( equiv-Σ ( λ (t : Σ A (λ x → B x → 𝕎 A B)) → Eq-ext-𝕎 (tree-𝕎 a f) (tree-𝕎 (pr1 t) (pr2 t))) diff --git a/src/trees/functoriality-w-types.lagda.md b/src/trees/functoriality-w-types.lagda.md index 6a32e1a93e..e5a123d283 100644 --- a/src/trees/functoriality-w-types.lagda.md +++ b/src/trees/functoriality-w-types.lagda.md @@ -71,10 +71,7 @@ abstract (D : C → UU l4) (f : A → C) (e : (x : A) → B x ≃ D (f x)) → (y : 𝕎 C D) → fiber (map-𝕎 D f e) y ≃ fiber-map-𝕎 D f e y equiv-fiber-map-𝕎 {A = A} {B} {C} D f e (tree-𝕎 c γ) = - ( ( ( inv-equiv - ( associative-Σ A - ( λ a → f a ＝ c) - ( λ t → (d : D c) → fiber (map-𝕎 D f e) (γ d)))) ∘e + ( ( ( inv-associative-Σ) ∘e ( equiv-tot ( λ a → ( ( equiv-tot @@ -110,9 +107,7 @@ abstract ( f a) ( ( map-𝕎 D f e) ∘ ( α ∘ map-inv-equiv (e a)))) (tree-𝕎 c γ)))))) ∘e - ( associative-Σ A - ( λ a → B a → 𝕎 A B) - ( λ t → map-𝕎 D f e (structure-𝕎-Alg t) ＝ tree-𝕎 c γ))) ∘e + ( associative-Σ)) ∘e ( equiv-Σ ( λ t → map-𝕎 D f e (structure-𝕎-Alg t) ＝ tree-𝕎 c γ) ( inv-equiv-structure-𝕎-Alg) diff --git a/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md b/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md index f223fc9b23..fe3efa9178 100644 --- a/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md @@ -221,10 +221,7 @@ module _ ( eq-htpy (λ z → eq-pair-Σ - ( eq-equiv - ( pair - ( map-commutative-coproduct (Id x z) (Id y z)) - ( is-equiv-map-commutative-coproduct (Id x z) (Id y z)))) + ( eq-equiv commutative-coproduct) ( eq-pair-Σ ( eq-is-prop ( is-prop-is-prop diff --git a/src/univalent-combinatorics/2-element-subtypes.lagda.md b/src/univalent-combinatorics/2-element-subtypes.lagda.md index 9c1bd2707d..09ce8a50b9 100644 --- a/src/univalent-combinatorics/2-element-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-subtypes.lagda.md @@ -126,7 +126,7 @@ module _ Fin 2 ≃ type-standard-2-Element-Subtype equiv-type-standard-2-Element-Subtype = ( inv-equiv - ( left-distributive-Σ-coproduct (type-Set X) (Id x) (Id y))) ∘e + ( left-distributive-Σ-coproduct)) ∘e ( equiv-coproduct ( equiv-is-contr ( is-contr-Fin-1) diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index b44650d1ca..94d03c1ac9 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -784,7 +784,7 @@ is-coproduct-Σ-Fin-2 P = ( equiv-coproduct ( left-unit-law-Σ-is-contr is-contr-Fin-1 (zero-Fin 0)) ( left-unit-law-Σ (P ∘ inr))) ∘e - ( right-distributive-Σ-coproduct (Fin 1) unit P) + ( right-distributive-Σ-coproduct P) ``` ### For any equivalence `e : Fin 2 ≃ X`, any element of `X` is either `e 0` or it is `e 1` diff --git a/src/univalent-combinatorics/binomial-types.lagda.md b/src/univalent-combinatorics/binomial-types.lagda.md index f815dbd237..8b2f68067a 100644 --- a/src/univalent-combinatorics/binomial-types.lagda.md +++ b/src/univalent-combinatorics/binomial-types.lagda.md @@ -172,12 +172,9 @@ compute-binomial-type-Level l {l1} {l2} A B = equiv-trunc-Prop ( equiv-postcomp-equiv ( inv-equiv (equiv-total-fiber (pr1 (pr2 e)))) B))) ∘e - ( inv-associative-Σ - ( UU (l1 ⊔ l)) - ( λ X → X ↪ᵈ A) - ( λ X → mere-equiv B (pr1 X)))) ∘e + ( inv-associative-Σ)) ∘e ( equiv-tot (λ X → commutative-product))) ∘e - ( associative-Σ (UU (l1 ⊔ l)) (λ X → mere-equiv B X) (λ X → (pr1 X) ↪ᵈ A)) + ( associative-Σ) compute-binomial-type : {l1 l2 : Level} (A : UU l1) (B : UU l2) → @@ -250,10 +247,7 @@ abstract binomial-type' (Maybe A) (Maybe B) ≃ (binomial-type' A B + binomial-type' A (Maybe B)) recursion-binomial-type' A B = - ( ( ( left-distributive-Σ-coproduct - ( A → Decidable-Prop _) - ( λ P → mere-equiv B (Σ A _)) - ( λ P → mere-equiv (Maybe B) (Σ A _))) ∘e + ( ( ( left-distributive-Σ-coproduct) ∘e ( equiv-tot ( λ P → ( ( equiv-coproduct @@ -283,15 +277,11 @@ abstract ( is-torsorial-false-Prop) ( pair (raise-empty-Prop _) map-inv-raise)))) ∘e ( right-distributive-Σ-coproduct - ( Σ (Prop _) type-Prop) - ( Σ (Prop _) (¬_ ∘ type-Prop)) ( ind-coproduct _ ( λ Q → mere-equiv (Maybe B) ((Σ A _) + (type-Prop (pr1 Q)))) ( λ Q → - mere-equiv - ( Maybe B) - ( (Σ A _) + (type-Prop (pr1 Q))))))) ∘e + mere-equiv (Maybe B) ((Σ A _) + (type-Prop (pr1 Q))))))) ∘e ( equiv-Σ ( ind-coproduct _ ( λ Q → @@ -313,14 +303,7 @@ abstract ( _) ( λ q → id-equiv) ( λ q → id-equiv)))))))) ∘e - ( associative-Σ - ( A → Decidable-Prop _) - ( λ a → Decidable-Prop _) - ( λ t → - mere-equiv - ( Maybe B) - ( ( Σ A (λ a → type-Decidable-Prop (pr1 t a))) + - ( type-Decidable-Prop (pr2 t)))))) ∘e + ( associative-Σ)) ∘e ( equiv-Σ ( λ p → mere-equiv @@ -334,7 +317,7 @@ abstract ( ( equiv-coproduct ( id-equiv) ( left-unit-law-Σ (λ y → type-Decidable-Prop (u (inr y))))) ∘e - ( right-distributive-Σ-coproduct A unit + ( right-distributive-Σ-coproduct ( λ x → type-Decidable-Prop (u x)))) ( Maybe B)))) diff --git a/src/univalent-combinatorics/cartesian-product-types.lagda.md b/src/univalent-combinatorics/cartesian-product-types.lagda.md index 43dee54458..4b60af63a3 100644 --- a/src/univalent-combinatorics/cartesian-product-types.lagda.md +++ b/src/univalent-combinatorics/cartesian-product-types.lagda.md @@ -56,7 +56,7 @@ product-Fin zero-ℕ l = left-absorption-product (Fin l) product-Fin (succ-ℕ k) l = ( ( compute-coproduct-Fin (k *ℕ l) l) ∘e ( equiv-coproduct (product-Fin k l) left-unit-law-product)) ∘e - ( right-distributive-product-coproduct (Fin k) unit (Fin l)) + ( right-distributive-product-coproduct) Fin-mul-ℕ : (k l : ℕ) → (Fin (k *ℕ l)) ≃ ((Fin k) × (Fin l)) Fin-mul-ℕ k l = inv-equiv (product-Fin k l) @@ -84,7 +84,7 @@ equiv-left-factor {l1} {l2} {X} {Y} y = ( ( right-unit-law-product) ∘e ( equiv-tot ( λ x → equiv-is-contr (is-torsorial-Id' y) is-contr-unit))) ∘e - ( associative-Σ X (λ x → Y) (λ t → Id (pr2 t) y)) + ( associative-Σ) count-left-factor : {l1 l2 : Level} {X : UU l1} {Y : UU l2} → count (X × Y) → Y → count X diff --git a/src/univalent-combinatorics/coproduct-types.lagda.md b/src/univalent-combinatorics/coproduct-types.lagda.md index ee2c6015ff..492e28f8b3 100644 --- a/src/univalent-combinatorics/coproduct-types.lagda.md +++ b/src/univalent-combinatorics/coproduct-types.lagda.md @@ -199,7 +199,7 @@ count-Σ-coproduct : count (Σ A P) → count (Σ A Q) → count (Σ A (λ x → (P x) + (Q x))) pr1 (count-Σ-coproduct count-P count-Q) = pr1 (count-coproduct count-P count-Q) pr2 (count-Σ-coproduct count-P count-Q) = - ( inv-equiv (left-distributive-Σ-coproduct _ _ _)) ∘e + ( inv-left-distributive-Σ-coproduct) ∘e ( pr2 (count-coproduct count-P count-Q)) ``` diff --git a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md index 6b06dd1332..b8b4c7ba7c 100644 --- a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md @@ -55,10 +55,7 @@ abstract with is-decidable-decidable-subtype P (inr star) ... | inl p = count-equiv' - ( right-distributive-Σ-coproduct - ( Fin k) - ( unit) - ( is-in-decidable-subtype P)) + ( right-distributive-Σ-coproduct (is-in-decidable-subtype P)) ( pair ( succ-ℕ ( number-of-elements-count (count-decidable-subtype-Fin k (P ∘ inl)))) @@ -70,10 +67,7 @@ abstract ( is-proof-irrelevant-is-in-decidable-subtype P (inr star) p))))) ... | inr f = count-equiv' - ( right-distributive-Σ-coproduct - ( Fin k) - ( unit) - ( is-in-decidable-subtype P)) + ( right-distributive-Σ-coproduct (is-in-decidable-subtype P)) ( count-equiv' ( right-unit-law-coproduct-is-empty ( Σ (Fin k) (is-in-decidable-subtype P ∘ inl)) diff --git a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md index 398a1fe35d..55b38cc930 100644 --- a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md @@ -67,7 +67,7 @@ count-Σ-Fin 0 f = count-is-empty pr1 count-Σ-Fin (succ-ℕ k) {B} f = count-equiv' ( ( equiv-coproduct id-equiv (left-unit-law-Σ (B ∘ inr))) ∘e - ( right-distributive-Σ-coproduct (Fin k) unit B)) + ( right-distributive-Σ-coproduct B)) ( count-coproduct (count-Σ-Fin k (f ∘ inl)) (f (inr star))) count-Σ' : @@ -148,9 +148,7 @@ count-fiber-map-section-family {l1} {l2} {A} {B} b e f (pair y z) = ( ( ( left-unit-law-Σ-is-contr ( is-torsorial-Id' y) ( pair y refl)) ∘e - ( inv-associative-Σ A - ( λ x → Id x y) - ( λ t → Id (tr B (pr2 t) (b (pr1 t))) z))) ∘e + ( inv-associative-Σ)) ∘e ( equiv-tot (λ x → equiv-pair-eq-Σ (pair x (b x)) (pair y z)))) ( count-eq (has-decidable-equality-count (f y)) (b y) z) @@ -196,8 +194,7 @@ count-base-count-Σ' {l1} {l2} {A} {B} e f g = count-base-count-Σ ( section-count-base-count-Σ' e f g) ( count-equiv' - ( left-distributive-Σ-coproduct A B - ( λ x → is-zero-ℕ (number-of-elements-count (f x)))) + ( left-distributive-Σ-coproduct) ( count-coproduct e g)) ( λ x → count-coproduct diff --git a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md index c623cec35a..a792a83eff 100644 --- a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md +++ b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md @@ -187,24 +187,12 @@ equiv-Surjection-Finite-Type-Decidable-Equivalence-Relation-Finite-Type {l1} A = ( λ X → (type-Finite-Type A) ↠ (type-Finite-Type X)) ( equiv-tot ( λ X → inv-equiv is-finite-iff-∃-surjection-has-decidable-equality))) ∘e - ( inv-associative-Σ - ( UU l1) - ( λ X → - has-decidable-equality X × - type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X))) - ( λ X → type-Finite-Type A ↠ pr1 X)) ∘e + ( inv-associative-Σ) ∘e ( equiv-tot ( λ X → - ( ( inv-equiv - ( associative-product - ( has-decidable-equality X) - ( type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X))) - ( type-Finite-Type A ↠ X))) ∘e - ( equiv-product id-equiv commutative-product) ∘e - ( associative-product - ( has-decidable-equality (map-equiv id-equiv X)) - ( type-Finite-Type A ↠ X) - ( type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))) ∘e + ( ( inv-associative-product) ∘e + ( equiv-product-right commutative-product) ∘e + ( associative-product) ∘e ( equiv-product-left commutative-product) ∘e ( equiv-add-redundant-prop ( is-prop-type-trunc-Prop) diff --git a/src/univalent-combinatorics/dependent-pair-types.lagda.md b/src/univalent-combinatorics/dependent-pair-types.lagda.md index bb19fd3a96..4ec8543814 100644 --- a/src/univalent-combinatorics/dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/dependent-pair-types.lagda.md @@ -108,9 +108,7 @@ abstract ( λ t → ( equiv-tot ( λ x → equiv-eq-pair-Σ (map-section-family b x) t)) ∘e - ( ( associative-Σ A - ( λ (x : A) → Id x (pr1 t)) - ( λ s → Id (tr B (pr2 s) (b (pr1 s))) (pr2 t))) ∘e + ( ( associative-Σ) ∘e ( inv-left-unit-law-Σ-is-contr ( is-torsorial-Id' (pr1 t)) ( pair (pr1 t) refl)))))) @@ -162,10 +160,7 @@ abstract is-proof-irrelevant-is-prop ( is-property-is-inhabited-or-empty (B x)) ( is-inhabited-or-empty-is-finite (g x)))) ∘e - ( inv-equiv - ( left-distributive-Σ-coproduct A - ( λ x → type-trunc-Prop (B x)) - ( λ x → is-empty (B x))))) + ( inv-left-distributive-Σ-coproduct)) ( is-finite-coproduct ( is-finite-base-is-finite-Σ-merely-inhabited ( is-set-type-subtype (λ x → trunc-Prop _) K) diff --git a/src/univalent-combinatorics/fibers-of-maps.lagda.md b/src/univalent-combinatorics/fibers-of-maps.lagda.md index 2d9e458ea5..c5c88df7ab 100644 --- a/src/univalent-combinatorics/fibers-of-maps.lagda.md +++ b/src/univalent-combinatorics/fibers-of-maps.lagda.md @@ -121,9 +121,7 @@ abstract ( ( ( left-unit-law-Σ-is-contr ( is-torsorial-Id' y) ( pair y refl)) ∘e - ( inv-associative-Σ A - ( λ x → Id x y) - ( λ t → Id (tr B (pr2 t) (b (pr1 t))) z))) ∘e + ( inv-associative-Σ)) ∘e ( equiv-tot (λ x → equiv-pair-eq-Σ (pair x (b x)) (pair y z)))) ( is-finite-eq (has-decidable-equality-is-finite (g y))) ``` @@ -146,17 +144,25 @@ is-decidable-fiber-Fin {k} {l} f y = ### If `f : A → B` and `B` is finite, then `A` is finite if and only if the fibers of `f` are finite ```agda -equiv-is-finite-domain-is-finite-fiber : - {l1 l2 : Level} {A : UU l1} → - (B : Finite-Type l2) (f : A → (type-Finite-Type B)) → - ((b : type-Finite-Type B) → is-finite (fiber f b)) ≃ is-finite A -equiv-is-finite-domain-is-finite-fiber {A = A} B f = - equiv-iff-is-prop - ( is-prop-Π (λ b → is-prop-is-finite (fiber f b))) - ( is-prop-is-finite A) - ( λ P → - is-finite-equiv - ( equiv-total-fiber f) - ( is-finite-Σ (is-finite-type-Finite-Type B) P)) - ( λ P → is-finite-fiber f P (is-finite-type-Finite-Type B)) +module _ + {l1 l2 : Level} {A : UU l1} + (B : Finite-Type l2) (f : A → (type-Finite-Type B)) + where + + equiv-is-finite-domain-is-finite-fiber : + ((b : type-Finite-Type B) → is-finite (fiber f b)) ≃ is-finite A + equiv-is-finite-domain-is-finite-fiber = + equiv-iff-is-prop + ( is-prop-Π (λ b → is-prop-is-finite (fiber f b))) + ( is-prop-is-finite A) + ( λ P → + is-finite-equiv + ( equiv-total-fiber f) + ( is-finite-Σ (is-finite-type-Finite-Type B) P)) + ( λ P → is-finite-fiber f P (is-finite-type-Finite-Type B)) + + inv-equiv-is-finite-domain-is-finite-fiber : + is-finite A ≃ ((b : type-Finite-Type B) → is-finite (fiber f b)) + inv-equiv-is-finite-domain-is-finite-fiber = + inv-equiv equiv-is-finite-domain-is-finite-fiber ``` diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index a99199ce57..2e092d3685 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -244,7 +244,7 @@ abstract finite-enumeration (X + Y) → finite-enumeration Y finite-enumeration-right-summand eX+Y = finite-enumeration-left-summand - ( finite-enumeration-equiv eX+Y (commutative-coproduct _ _)) + ( finite-enumeration-equiv eX+Y commutative-coproduct) finite-enumeration-coproduct : {l1 l2 : Level} {X : UU l1} {Y : UU l2} → diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index 8fb4593a19..62ad690ee5 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -87,17 +87,17 @@ is-finite-and-inhabited X = compute-Inhabited-Finite-Type' : {l : Level} → Inhabited-Finite-Type l ≃ type-subuniverse is-finite-and-inhabited-Prop -compute-Inhabited-Finite-Type' = associative-Σ _ _ _ +compute-Inhabited-Finite-Type' = associative-Σ map-compute-Inhabited-Finite-Type' : {l : Level} → Inhabited-Finite-Type l → type-subuniverse is-finite-and-inhabited-Prop -map-compute-Inhabited-Finite-Type' = map-associative-Σ _ _ _ +map-compute-Inhabited-Finite-Type' = map-associative-Σ map-inv-compute-Inhabited-Finite-Type' : {l : Level} → type-subuniverse is-finite-and-inhabited-Prop → Inhabited-Finite-Type l -map-inv-compute-Inhabited-Finite-Type' = map-inv-associative-Σ _ _ _ +map-inv-compute-Inhabited-Finite-Type' = map-inv-associative-Σ ``` ### Families of inhabited types diff --git a/src/univalent-combinatorics/sums-of-natural-numbers.lagda.md b/src/univalent-combinatorics/sums-of-natural-numbers.lagda.md index 6fff4532d6..c610429e47 100644 --- a/src/univalent-combinatorics/sums-of-natural-numbers.lagda.md +++ b/src/univalent-combinatorics/sums-of-natural-numbers.lagda.md @@ -51,7 +51,7 @@ abstract ( ( double-counting-equiv ( count-Σ count-A (λ x → count-Σ (count-B x) (λ y → count-Fin (f x y)))) ( count-Σ (count-Σ count-A count-B) (λ x → count-Fin (ind-Σ f x))) - ( inv-associative-Σ A B (λ x → Fin (ind-Σ f x)))) ∙ + ( inv-associative-Σ)) ∙ ( number-of-elements-count-Σ ( count-Σ count-A count-B) ( λ x → (count-Fin (ind-Σ f x))))) diff --git a/src/univalent-combinatorics/type-duality.lagda.md b/src/univalent-combinatorics/type-duality.lagda.md index bdfc816854..0936c63ee0 100644 --- a/src/univalent-combinatorics/type-duality.lagda.md +++ b/src/univalent-combinatorics/type-duality.lagda.md @@ -42,80 +42,57 @@ open import univalent-combinatorics.inhabited-finite-types equiv-surjection-finite-type-family-finite-inhabited-type : {l : Level} (A : Finite-Type l) (B : Finite-Type l) → ( ( type-Finite-Type A ↠ type-Finite-Type B) ≃ - ( Σ ( (type-Finite-Type B) → Inhabited-Finite-Type l) + ( Σ ( type-Finite-Type B → Inhabited-Finite-Type l) ( λ Y → - (type-Finite-Type A) ≃ + type-Finite-Type A ≃ Σ (type-Finite-Type B) (λ b → type-Inhabited-Finite-Type (Y b))))) -equiv-surjection-finite-type-family-finite-inhabited-type {l} A B = - ( ( equiv-Σ - ( λ Y → - type-Finite-Type A ≃ - Σ (type-Finite-Type B) (λ b → type-Inhabited-Finite-Type (Y b))) - ( equiv-postcomp +equiv-surjection-finite-type-family-finite-inhabited-type A B = + ( equiv-Σ-equiv-base + ( λ Y → + type-Finite-Type A ≃ + Σ (type-Finite-Type B) (λ b → type-Inhabited-Finite-Type (Y b))) + ( equiv-postcomp + ( type-Finite-Type B) + ( inv-associative-Σ ∘e equiv-tot (λ _ → commutative-product)))) ∘e + ( equiv-fixed-Slice-structure + ( λ x → (is-inhabited x) × (is-finite x)) + ( type-Finite-Type A) + ( type-Finite-Type B)) ∘e + ( equiv-tot (λ _ → inv-distributive-Π-Σ)) ∘e + ( associative-Σ) ∘e + ( inv-equiv-inclusion-is-full-subtype + ( λ f → + Π-Prop ( type-Finite-Type B) - ( inv-associative-Σ ( UU l) is-finite ( λ X → is-inhabited (pr1 X)) ∘e - equiv-Σ - ( λ z → is-finite z × is-inhabited z) - ( id-equiv) - ( λ _ → commutative-product))) - ( λ b → id-equiv)) ∘e - ( ( equiv-fixed-Slice-structure - ( λ x → (is-inhabited x) × (is-finite x)) - ( type-Finite-Type A) - ( type-Finite-Type B)) ∘e - ( ( equiv-Σ - ( structure-map (λ x → is-inhabited x × is-finite x)) - ( id-equiv) - ( λ _ → inv-equiv distributive-Π-Σ)) ∘e - ( ( associative-Σ - ( type-Finite-Type A → type-Finite-Type B) - ( structure-map is-inhabited) - ( _)) ∘e - ( ( inv-equiv - ( equiv-inclusion-is-full-subtype - ( λ f → - Π-Prop - ( type-Finite-Type B) - ( λ b → is-finite-Prop (fiber (pr1 f) b))) - ( λ f → - is-finite-fiber - ( pr1 f) - ( is-finite-type-Finite-Type A) - ( is-finite-type-Finite-Type B))))))))) + ( λ b → is-finite-Prop (fiber (pr1 f) b))) + ( λ f → + is-finite-fiber + ( pr1 f) + ( is-finite-type-Finite-Type A) + ( is-finite-type-Finite-Type B))) Slice-Surjection-Finite-Type : (l : Level) {l1 : Level} (A : Finite-Type l1) → UU (lsuc l ⊔ l1) Slice-Surjection-Finite-Type l A = - Σ (Finite-Type l) (λ X → (type-Finite-Type X) ↠ type-Finite-Type A) + Σ (Finite-Type l) (λ X → type-Finite-Type X ↠ type-Finite-Type A) equiv-Fiber-trunc-prop-Finite-Type : (l : Level) {l1 : Level} (A : Finite-Type l1) → Slice-Surjection-Finite-Type (l1 ⊔ l) A ≃ (type-Finite-Type A → Inhabited-Finite-Type (l1 ⊔ l)) -equiv-Fiber-trunc-prop-Finite-Type l {l1} A = - ( ( equiv-Π - ( λ _ → Inhabited-Finite-Type _) - ( id-equiv) - ( λ a → inv-associative-Σ _ _ _) ∘e - ( ( equiv-Fiber-structure - ( l) - ( λ X → is-finite X × is-inhabited X) (type-Finite-Type A)))) ∘e - ( ( equiv-Σ - ( _) - ( id-equiv) - ( λ X → - ( equiv-Σ - ( _) - ( id-equiv) - ( λ f → - ( inv-equiv distributive-Π-Σ) ∘e - ( equiv-Σ-equiv-base - ( _) - ( inv-equiv - ( equiv-is-finite-domain-is-finite-fiber A f)))))) ∘e - ( ( equiv-Σ - ( _) - ( id-equiv) - ( λ _ → equiv-left-swap-Σ)) ∘e - ( associative-Σ (UU (l ⊔ l1)) (is-finite) _))))) +equiv-Fiber-trunc-prop-Finite-Type l A = + ( equiv-Π-equiv-family (λ a → inv-associative-Σ)) ∘e + ( equiv-Fiber-structure l + ( λ X → is-finite X × is-inhabited X) + ( type-Finite-Type A)) ∘e + ( equiv-tot + ( λ X → + ( equiv-tot + ( λ f → + ( inv-distributive-Π-Σ) ∘e + ( equiv-Σ-equiv-base + ( λ _ → (x : type-Finite-Type A) → is-inhabited (fiber f x)) + ( inv-equiv-is-finite-domain-is-finite-fiber A f)))) ∘e + ( equiv-left-swap-Σ))) ∘e + ( associative-Σ) ``` diff --git a/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md b/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md index 716344eb21..42e00dddf7 100644 --- a/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md +++ b/src/univalent-combinatorics/untruncated-pi-finite-types.lagda.md @@ -619,11 +619,8 @@ abstract ( unit-trunc-Set ∘ f , Eηf) ( refl-htpy)) ( λ { (inl x) → id-equiv ; (inr x) → id-equiv})) ∘e - ( inv-equiv - ( right-distributive-Σ-coproduct - ( im (f ∘ inl)) - ( im (f ∘ inr)) - ( rec-coproduct (B ∘ pr1) (B ∘ pr1)))) + ( inv-right-distributive-Σ-coproduct + ( rec-coproduct (B ∘ pr1) (B ∘ pr1))) i : Fin k → type-trunc-Set (im (f ∘ inl)) i = unit-trunc-Set ∘ map-unit-im (f ∘ inl) diff --git a/src/universal-algebra/equivalences-of-models-of-signatures.lagda.md b/src/universal-algebra/equivalences-of-models-of-signatures.lagda.md index ecc14d2d33..fe8219a461 100644 --- a/src/universal-algebra/equivalences-of-models-of-signatures.lagda.md +++ b/src/universal-algebra/equivalences-of-models-of-signatures.lagda.md @@ -151,7 +151,7 @@ module _ Eq-Model-Signature X Y ≃ Σ ( hom-Set (set-Model-Signature σ X) (set-Model-Signature σ Y)) ( λ f → is-equiv f × preserves-operations-Model-Signature σ X Y f) - equiv-Eq-Model-Signature' X Y = associative-Σ _ _ _ + equiv-Eq-Model-Signature' X Y = associative-Σ refl-Eq-Model-Signature : {l2 : Level} (X : Model-Signature σ l2) → Eq-Model-Signature X X