Refactor coproduct equivalences (#1137)

Refactors some equivalences related to coproducs and adds one new
definition.

- removes the abstract block around `is-equiv-coproduct` in
`foundation.functorality-coproduct-types`, thus allowing `map-inv-equiv
(equiv-coproduct e e')` to compute to `map-coproduct (map-inv-equiv e)
(map-inv-equiv e')`. We keep abstract blocks around the proof that the
inverse map is a section and retraction

- computes the underlying map of the equivalence `Fin-add-ℕ` in
`univalent-combinatorics.coproduct-types`

---------

Co-authored-by: Fredrik Bakke <[email protected]>

src/elementary-number-theory/falling-factorials.lagda.md

@@ -79,6 +79,6 @@ Fin-falling-factorial-ℕ (succ-ℕ n) (succ-ℕ m) =
     ( equiv-coproduct
       ( Fin-falling-factorial-ℕ n m)
       ( Fin-falling-factorial-ℕ n (succ-ℕ m)))) ∘e
-  ( Fin-add-ℕ (falling-factorial-ℕ n m) (falling-factorial-ℕ n (succ-ℕ m)))
+  ( inv-compute-coproduct-Fin (falling-factorial-ℕ n m) (falling-factorial-ℕ n (succ-ℕ m)))
 -}
 ```

src/foundation/functoriality-coproduct-types.lagda.md

@@ -40,6 +40,7 @@ open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.negation
 open import foundation-core.propositions
+open import foundation-core.sections
 open import foundation-core.transport-along-identifications
 ```
 
@@ -207,44 +208,60 @@ module _
   {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'}
   where
 
-  abstract
-    is-equiv-map-coproduct :
-      {f : A → A'} {g : B → B'} →
-      is-equiv f → is-equiv g → is-equiv (map-coproduct f g)
-    pr1
-      ( pr1
-        ( is-equiv-map-coproduct
-          ( (sf , Sf) , (rf , Rf))
-          ( (sg , Sg) , (rg , Rg)))) = map-coproduct sf sg
-    pr2
-      ( pr1
-        ( is-equiv-map-coproduct {f} {g}
-          ( (sf , Sf) , (rf , Rf))
-          ( (sg , Sg) , (rg , Rg)))) =
-      ( ( inv-htpy (preserves-comp-map-coproduct sf f sg g)) ∙h
-        ( htpy-map-coproduct Sf Sg)) ∙h
-      ( id-map-coproduct A' B')
-    pr1
-      ( pr2
-        ( is-equiv-map-coproduct
-          ( (sf , Sf) , (rf , Rf))
-          ( (sg , Sg) , (rg , Rg)))) = map-coproduct rf rg
-    pr2
-      ( pr2
-        ( is-equiv-map-coproduct {f} {g}
-          ( (sf , Sf) , (rf , Rf))
-          ( (sg , Sg) , (rg , Rg)))) =
-      ( ( inv-htpy (preserves-comp-map-coproduct f rf g rg)) ∙h
-        ( htpy-map-coproduct Rf Rg)) ∙h
-      ( id-map-coproduct A B)
-
   map-equiv-coproduct : A ≃ A' → B ≃ B' → A + B → A' + B'
-  map-equiv-coproduct e e' = map-coproduct (map-equiv e) (map-equiv e')
+  map-equiv-coproduct f g = map-coproduct (map-equiv f) (map-equiv g)
+
+  map-inv-equiv-coproduct : A ≃ A' → B ≃ B' → A' + B' → A + B
+  map-inv-equiv-coproduct f g =
+    map-coproduct (map-inv-equiv f) (map-inv-equiv g)
+
+  is-section-map-inv-equiv-coproduct :
+    (f : A ≃ A') (g : B ≃ B') →
+    is-section
+      ( map-equiv-coproduct f g)
+      ( map-inv-equiv-coproduct f g)
+  is-section-map-inv-equiv-coproduct f g =
+    ( inv-htpy
+      ( preserves-comp-map-coproduct
+        ( map-inv-equiv f)
+        ( map-equiv f)
+        ( map-inv-equiv g)
+        ( map-equiv g))) ∙h
+    ( htpy-map-coproduct
+      ( is-section-map-inv-equiv f)
+      ( is-section-map-inv-equiv g)) ∙h
+    ( id-map-coproduct A' B')
+
+  is-retraction-map-inv-equiv-coproduct :
+    (f : A ≃ A') (g : B ≃ B') →
+    is-retraction
+      ( map-equiv-coproduct f g)
+      ( map-inv-equiv-coproduct f g)
+  is-retraction-map-inv-equiv-coproduct f g =
+    ( inv-htpy
+      ( preserves-comp-map-coproduct
+        ( map-equiv f)
+        ( map-inv-equiv f)
+        ( map-equiv g)
+        ( map-inv-equiv g))) ∙h
+    ( htpy-map-coproduct
+      ( is-retraction-map-inv-equiv f)
+      ( is-retraction-map-inv-equiv g)) ∙h
+    ( id-map-coproduct A B)
+
+  is-equiv-map-coproduct :
+    {f : A → A'} {g : B → B'} →
+    is-equiv f → is-equiv g → is-equiv (map-coproduct f g)
+  is-equiv-map-coproduct {f} {g} H K =
+    is-equiv-is-invertible
+      ( map-coproduct (map-inv-is-equiv H) (map-inv-is-equiv K))
+      ( is-section-map-inv-equiv-coproduct (f , H) (g , K))
+      ( is-retraction-map-inv-equiv-coproduct (f , H) (g , K))
 
   equiv-coproduct : A ≃ A' → B ≃ B' → (A + B) ≃ (A' + B')
-  pr1 (equiv-coproduct e e') = map-equiv-coproduct e e'
-  pr2 (equiv-coproduct e e') =
-    is-equiv-map-coproduct (is-equiv-map-equiv e) (is-equiv-map-equiv e')
+  equiv-coproduct e e' =
+    ( map-equiv-coproduct e e' ,
+      is-equiv-map-coproduct (is-equiv-map-equiv e) (is-equiv-map-equiv e'))
 ```
 
 ### The functorial action of coproducts preserves retractions

src/univalent-combinatorics/binomial-types.lagda.md

@@ -402,7 +402,7 @@ binomial-type-Fin (succ-ℕ n) zero-ℕ =
   equiv-is-contr binomial-type-over-empty is-contr-Fin-one-ℕ
 binomial-type-Fin (succ-ℕ n) (succ-ℕ m) =
   ( ( inv-equiv
-      ( Fin-add-ℕ
+      ( inv-compute-coproduct-Fin
         ( binomial-coefficient-ℕ n m)
         ( binomial-coefficient-ℕ n (succ-ℕ m)))) ∘e
     ( equiv-coproduct

src/univalent-combinatorics/cartesian-product-types.lagda.md

@@ -54,7 +54,7 @@ operation on finite types.
 product-Fin : (k l : ℕ) → ((Fin k) × (Fin l)) ≃ Fin (k *ℕ l)
 product-Fin zero-ℕ l = left-absorption-product (Fin l)
 product-Fin (succ-ℕ k) l =
-  ( ( coproduct-Fin (k *ℕ l) l) ∘e
+  ( ( 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))
 

src/univalent-combinatorics/coproduct-types.lagda.md

@@ -13,12 +13,15 @@ open import elementary-number-theory.natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.equivalence-extensionality
 open import foundation.equivalences
+open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-propositional-truncation
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.injective-maps
 open import foundation.mere-equivalences
 open import foundation.propositional-truncations
 open import foundation.type-arithmetic-coproduct-types
@@ -44,54 +47,84 @@ Coproducts of finite types are finite, giving a coproduct operation on the type
 ### The standard finite types are closed under coproducts
 
 ```agda
-coproduct-Fin :
-  (k l : ℕ) → (Fin k + Fin l) ≃ Fin (k +ℕ l)
-coproduct-Fin k zero-ℕ = right-unit-law-coproduct (Fin k)
-coproduct-Fin k (succ-ℕ l) =
-  (equiv-coproduct (coproduct-Fin k l) id-equiv) ∘e inv-associative-coproduct
-
-map-coproduct-Fin :
-  (k l : ℕ) → (Fin k + Fin l) → Fin (k +ℕ l)
-map-coproduct-Fin k l = map-equiv (coproduct-Fin k l)
-
-Fin-add-ℕ :
-  (k l : ℕ) → Fin (k +ℕ l) ≃ (Fin k + Fin l)
-Fin-add-ℕ k l = inv-equiv (coproduct-Fin k l)
-
-inl-coproduct-Fin :
-  (k l : ℕ) → Fin k → Fin (k +ℕ l)
-inl-coproduct-Fin k l = map-coproduct-Fin k l ∘ inl
-
-inr-coproduct-Fin :
-  (k l : ℕ) → Fin l → Fin (k +ℕ l)
-inr-coproduct-Fin k l = map-coproduct-Fin k l ∘ inr
-
-compute-inl-coproduct-Fin :
-  (k : ℕ) → inl-coproduct-Fin k 0 ~ id
+compute-coproduct-Fin : (k l : ℕ) → (Fin k + Fin l) ≃ Fin (k +ℕ l)
+compute-coproduct-Fin k zero-ℕ = right-unit-law-coproduct (Fin k)
+compute-coproduct-Fin k (succ-ℕ l) =
+  ( equiv-coproduct (compute-coproduct-Fin k l) id-equiv) ∘e
+  ( inv-associative-coproduct)
+
+map-compute-coproduct-Fin : (k l : ℕ) → (Fin k + Fin l) → Fin (k +ℕ l)
+map-compute-coproduct-Fin k l = map-equiv (compute-coproduct-Fin k l)
+
+inv-compute-coproduct-Fin : (k l : ℕ) → Fin (k +ℕ l) ≃ (Fin k + Fin l)
+inv-compute-coproduct-Fin k l = inv-equiv (compute-coproduct-Fin k l)
+
+map-inv-compute-coproduct-Fin : (k l : ℕ) → Fin (k +ℕ l) → Fin k + Fin l
+map-inv-compute-coproduct-Fin k l = map-equiv (inv-compute-coproduct-Fin k l)
+
+inl-coproduct-Fin : (k l : ℕ) → Fin k → Fin (k +ℕ l)
+inl-coproduct-Fin k l = map-compute-coproduct-Fin k l ∘ inl
+
+inr-coproduct-Fin : (k l : ℕ) → Fin l → Fin (k +ℕ l)
+inr-coproduct-Fin k l = map-compute-coproduct-Fin k l ∘ inr
+
+compute-inl-coproduct-Fin : (k : ℕ) → inl-coproduct-Fin k 0 ~ id
 compute-inl-coproduct-Fin k x = refl
+
+map-compute-map-inv-compute-coproduct-Fin :
+  (k l : ℕ) → Fin (k +ℕ l) → Fin k + Fin l
+map-compute-map-inv-compute-coproduct-Fin k zero-ℕ = inl
+map-compute-map-inv-compute-coproduct-Fin k (succ-ℕ l) =
+  ( map-equiv (associative-coproduct {A = Fin k} {B = Fin l})) ∘
+  ( map-coproduct (map-compute-map-inv-compute-coproduct-Fin k l) id)
+
+abstract
+  compute-map-inv-compute-coproduct-Fin :
+    (k l : ℕ) →
+    map-inv-compute-coproduct-Fin k l ~
+    map-compute-map-inv-compute-coproduct-Fin k l
+  compute-map-inv-compute-coproduct-Fin k zero-ℕ x = refl
+  compute-map-inv-compute-coproduct-Fin k (succ-ℕ l) x =
+    ( htpy-eq
+      ( distributive-map-inv-comp-equiv
+        ( inv-associative-coproduct)
+        ( equiv-coproduct (compute-coproduct-Fin k l) id-equiv))
+      ( x)) ∙
+    ( htpy-eq-equiv
+      ( inv-inv-equiv associative-coproduct)
+      ( map-inv-equiv-coproduct (compute-coproduct-Fin k l) id-equiv x)) ∙
+    ( ap
+      ( map-associative-coproduct)
+      ( htpy-map-coproduct
+        ( compute-map-inv-compute-coproduct-Fin k l)
+        ( refl-htpy)
+        ( x)))
 ```
 
-### Inclusion of `coproduct-Fin` into the natural numbers
+### Computing the inclusion of a coproduct of standard finite types into the natural numbers
 
 ```agda
-nat-coproduct-Fin :
-  (n m : ℕ) → (x : Fin n + Fin m) →
-  nat-Fin (n +ℕ m) (map-coproduct-Fin n m x) ＝
-  ind-coproduct _ (nat-Fin n) (λ i → n +ℕ (nat-Fin m i)) x
-nat-coproduct-Fin n zero-ℕ (inl x) = refl
-nat-coproduct-Fin n (succ-ℕ m) (inl x) = nat-coproduct-Fin n m (inl x)
-nat-coproduct-Fin n (succ-ℕ m) (inr (inl x)) = nat-coproduct-Fin n m (inr x)
-nat-coproduct-Fin n (succ-ℕ m) (inr (inr _)) = refl
-
-nat-inl-coproduct-Fin :
-  (n m : ℕ) (i : Fin n) →
-  nat-Fin (n +ℕ m) (inl-coproduct-Fin n m i) ＝ nat-Fin n i
-nat-inl-coproduct-Fin n m i = nat-coproduct-Fin n m (inl i)
-
-nat-inr-coproduct-Fin :
-  (n m : ℕ) (i : Fin m) →
-  nat-Fin (n +ℕ m) (inr-coproduct-Fin n m i) ＝ n +ℕ (nat-Fin m i)
-nat-inr-coproduct-Fin n m i = nat-coproduct-Fin n m (inr i)
+abstract
+  nat-coproduct-Fin :
+    (n m : ℕ) (x : Fin n + Fin m) →
+    nat-Fin (n +ℕ m) (map-compute-coproduct-Fin n m x) ＝
+    ind-coproduct _ (nat-Fin n) (λ i → n +ℕ (nat-Fin m i)) x
+  nat-coproduct-Fin n zero-ℕ (inl x) = refl
+  nat-coproduct-Fin n (succ-ℕ m) (inl x) = nat-coproduct-Fin n m (inl x)
+  nat-coproduct-Fin n (succ-ℕ m) (inr (inl x)) = nat-coproduct-Fin n m (inr x)
+  nat-coproduct-Fin n (succ-ℕ m) (inr (inr _)) = refl
+
+abstract
+  nat-inl-coproduct-Fin :
+    (n m : ℕ) (i : Fin n) →
+    nat-Fin (n +ℕ m) (inl-coproduct-Fin n m i) ＝ nat-Fin n i
+  nat-inl-coproduct-Fin n m i = nat-coproduct-Fin n m (inl i)
+
+abstract
+  nat-inr-coproduct-Fin :
+    (n m : ℕ) (i : Fin m) →
+    nat-Fin (n +ℕ m) (inr-coproduct-Fin n m i) ＝ n +ℕ (nat-Fin m i)
+  nat-inr-coproduct-Fin n m i = nat-coproduct-Fin n m (inr i)
 ```
 
 ### Types equipped with a count are closed under coproducts
@@ -102,13 +135,13 @@ count-coproduct :
   count X → count Y → count (X + Y)
 pr1 (count-coproduct (pair k e) (pair l f)) = k +ℕ l
 pr2 (count-coproduct (pair k e) (pair l f)) =
-  (equiv-coproduct e f) ∘e (inv-equiv (coproduct-Fin k l))
+  (equiv-coproduct e f) ∘e (inv-equiv (compute-coproduct-Fin k l))
 
 abstract
   number-of-elements-count-coproduct :
     {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : count X) (f : count Y) →
-    Id ( number-of-elements-count (count-coproduct e f))
-      ( (number-of-elements-count e) +ℕ (number-of-elements-count f))
+    number-of-elements-count (count-coproduct e f) ＝
+    (number-of-elements-count e) +ℕ (number-of-elements-count f)
   number-of-elements-count-coproduct (pair k e) (pair l f) = refl
 ```
 
@@ -225,7 +258,7 @@ pr2 (coproduct-UU-Fin {l1} {l2} k l (pair X H) (pair Y K)) =
         ( mere-equiv-Prop (Fin (k +ℕ l)) (X + Y))
         ( λ e2 →
           unit-trunc-Prop
-            ( equiv-coproduct e1 e2 ∘e inv-equiv (coproduct-Fin k l))))
+            ( equiv-coproduct e1 e2 ∘e inv-equiv (compute-coproduct-Fin k l))))
 
 coproduct-eq-is-finite :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} (P : is-finite X) (Q : is-finite Y) →