Implicit type arguments in type-arithmetic

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)

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

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) ,

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

src/category-theory/structure-equivalences-set-magmoids.lagda.md

@@ -122,23 +122,23 @@ 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₁' →
                 preserves-comp-hom-Set-Magmoid A B F₀ (λ f → pr1 E₁' f))
               ( ( distributive-implicit-Π-Σ) ∘e
                 ( equiv-implicit-Π-equiv-family
                   ( λ _ → distributive-implicit-Π-Σ)))))))) ∘e
-    ( associative-Σ _ _ _)
+    ( associative-Σ)
 ```
 
 ### Structure equivalences of set-magmoids characterize their equality

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-equiv left-distributive-Σ-coproduct) ∘e
         {!!})) ∘e
     ( equiv-coproduct
       ( Fin-falling-factorial-ℕ n m)

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 `ℕ`

src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md

@@ -242,6 +242,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)))
 ```

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))

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})

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)

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-Σ)
 ```

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)))))

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)
 ```
 

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-Π

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

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
 ```
 
 ## See also

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))
 ```
 

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

src/foundation/fundamental-theorem-of-equivalence-relations.lagda.md

@@ -118,10 +118,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 +288,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 +316,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 :