Equivalence between the first sphere and the circle (UniMath#776)

Co-authored-by: Egbert Rijke <[email protected]>
fredrik-bakke · Sep 16, 2023 · 1fb5dc5 · 1fb5dc5
1 parent 1fe0803
commit 1fb5dc5
Show file tree

Hide file tree

Showing 6 changed files with 413 additions and 5 deletions.
diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md
@@ -72,6 +72,14 @@ map-compute-dependent-identification-eq-value-id-id :
   dependent-identification (eq-value id id) p q r
 map-compute-dependent-identification-eq-value-id-id refl q r s =
   inv (s ∙ right-unit)
+
+map-compute-dependent-identification-eq-value-comp-id :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : B → A) (f : A → B) {a b : A}
+  (p : a ＝ b) (q : eq-value (g ∘ f) id a) (r : eq-value (g ∘ f) id b) →
+  coherence-square-identifications (ap g (ap f p)) r q p →
+  dependent-identification (eq-value (g ∘ f) id) p q r
+map-compute-dependent-identification-eq-value-comp-id g f refl q r s =
+  inv (s ∙ right-unit)
 ```
 
 ### Homotopies

diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
@@ -620,7 +620,7 @@ interchange-y-z-concat-Id³ refl refl refl refl = inv right-unit
 
 ## Properties of 4-paths
 
-The pattern for concatination of 1, 2, and 3-paths continues. There are four
+The pattern for concatenation of 1, 2, and 3-paths continues. There are four
 ways to concatenate in quadruple identity types. We name the three non-standard
 concatenations in quadruple identity types `i`-, `j`-, and `k`-concatenation,
 after the standard names for the quaternions `i`, `j`, and `k`.