Refactor coproduct equivalences

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

@@ -194,36 +194,48 @@ module _
   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
+    is-section-map-inv-equiv-coproduct :
+      (f : A ≃ A') (g : B ≃ B') →
+      ( map-coproduct (map-equiv f) (map-equiv g)) ∘
+      ( map-coproduct (map-inv-equiv f) (map-inv-equiv g)) ~ id
+    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')
-    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
+
+  abstract
+    is-retraction-map-inv-equiv-coproduct :
+      (f : A ≃ A') (g : B ≃ B') →
+      ( map-coproduct (map-inv-equiv f) (map-inv-equiv g)) ∘
+      ( map-coproduct (map-equiv f) (map-equiv g)) ~ id
+    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))
+
   map-equiv-coproduct : A ≃ A' → B ≃ B' → A + B → A' + B'
   map-equiv-coproduct e e' = map-coproduct (map-equiv e) (map-equiv e')
 

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
@@ -69,6 +72,29 @@ inr-coproduct-Fin k l = map-coproduct-Fin k l ∘ inr
 compute-inl-coproduct-Fin :
   (k : ℕ) → inl-coproduct-Fin k 0 ~ id
 compute-inl-coproduct-Fin k x = refl
+
+map-Fin-add-ℕ :
+  (k l : ℕ) → Fin (k +ℕ l) → Fin k + Fin l
+map-Fin-add-ℕ k zero-ℕ = inl
+map-Fin-add-ℕ k (succ-ℕ l) =
+  ( map-equiv (associative-coproduct {A = Fin k} {B = Fin l})) ∘
+  ( map-coproduct (map-Fin-add-ℕ k l) id)
+
+compute-map-Fin-add-ℕ :
+  (k l : ℕ) → map-equiv (Fin-add-ℕ k l) ~ map-Fin-add-ℕ k l
+compute-map-Fin-add-ℕ k zero-ℕ x = refl
+compute-map-Fin-add-ℕ k (succ-ℕ l) x =
+  ( htpy-eq
+    ( distributive-map-inv-comp-equiv
+      ( inv-associative-coproduct)
+      ( equiv-coproduct (coproduct-Fin k l) id-equiv))
+    ( x)) ∙
+  ( htpy-eq-equiv
+    ( inv-inv-equiv associative-coproduct)
+    ( map-inv-equiv (equiv-coproduct (coproduct-Fin k l) id-equiv) x)) ∙
+  ( ap
+    ( map-associative-coproduct)
+    ( htpy-map-coproduct (compute-map-Fin-add-ℕ k l) refl-htpy x))
 ```
 
 ### Inclusion of `coproduct-Fin` into the natural numbers