Miscellaneous edits from UniMath#1547

Author: fredrik-bakke

references.bib

@@ -626,6 +626,20 @@ @misc{Lavenir23
   primaryclass  = {math.AT},
 }
 
+@article{Ljungström24,
+  title         = {Symmetric monoidal smash products in homotopy type theory},
+  author        = {Ljungström, Axel},
+  year          = 2024,
+  month         = oct,
+  journal       = {Mathematical Structures in Computer Science},
+  publisher     = {Cambridge University Press (CUP)},
+  volume        = 34,
+  number        = 9,
+  pages         = {985–1007},
+  doi           = {10.1017/s0960129524000318},
+  issn          = {1469-8072},
+}
+
 @book{Lurie09,
   title         = {Higher Topos Theory},
   author        = {Jacob Lurie},

src/foundation/projective-types.lagda.md

@@ -26,17 +26,17 @@ open import foundation-core.truncated-types
 
 A type `X` is said to be {{#concept "set-projective" Agda=is-set-projective}} if
 for every [surjective map](foundation.surjective-maps.md) `f : A ↠ B` onto a
-[set](foundation-core.sets.md) `B` the [postcomposition
-function[(foundation-core.postcomposition-functions.md)
+[set](foundation-core.sets.md) `B` the
+[postcomposition function](foundation-core.postcomposition-functions.md)
 
 ```text
   (X → A) → (X → B)
 ```
 
 is surjective. This is [equivalent](foundation.logical-equivalences.md) to the
-condition that for every [equivalence
-relation[(foundation-core.equivalence-relations.md) `R` on a type `A` the
-natural map
+condition that for every
+[equivalence relation](foundation-core.equivalence-relations.md) `R` on a type
+`A` the natural map
 
 ```text
   (X → A)/~ → (X → A/R)

src/logic/double-negation-eliminating-maps.lagda.md

@@ -84,9 +84,9 @@ module _
   map-double-negation-eliminating-map : A → B
   map-double-negation-eliminating-map = pr1 f
 
-  is-double-negation-eliminating-double-negation-eliminating-map :
+  is-double-negation-eliminating-map-double-negation-eliminating-map :
     is-double-negation-eliminating-map map-double-negation-eliminating-map
-  is-double-negation-eliminating-double-negation-eliminating-map = pr2 f
+  is-double-negation-eliminating-map-double-negation-eliminating-map = pr2 f
 ```
 
 ## Properties
@@ -348,7 +348,7 @@ module _
     (f : A →¬¬ B) → ε-operator-map (map-double-negation-eliminating-map f)
   ε-operator-double-negation-eliminating-map f =
     ε-operator-map-is-double-negation-eliminating-map
-      ( is-double-negation-eliminating-double-negation-eliminating-map f)
+      ( is-double-negation-eliminating-map-double-negation-eliminating-map f)
 ```
 
 ## See also

src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md

@@ -782,6 +782,10 @@ module _
         ( tr³-horizontal-concat-right-unit-law-right-whisker-left-unit-law-left-whisker-Ω²))
 ```
 
+## See also
+
+- [Medial magmas](structured-types.medial-magmas.md)
+
 ## External links
 
 - [The Eckmann-Hilton argument](https://1lab.dev/Algebra.Magma.Unital.EckmannHilton.html)

src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md

@@ -15,6 +15,8 @@ open import foundation.faithful-maps
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.truncated-maps
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import structured-types.faithful-pointed-maps
@@ -77,6 +79,30 @@ module _
       ( ap (map-pointed-map f) x))
 ```
 
+### (𝑛+1)-truncated pointed maps induce 𝑛-truncated maps on loop spaces
+
+```agda
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : Pointed-Type l1} {B : Pointed-Type l2}
+  where
+
+  is-trunc-map-map-Ω :
+    (f : A →∗ B) →
+    is-trunc-map (succ-𝕋 k) (map-pointed-map f) →
+    is-trunc-map k (map-Ω f)
+  is-trunc-map-map-Ω f H =
+    is-trunc-map-comp k
+      ( tr-type-Ω (preserves-point-pointed-map f))
+      ( ap (map-pointed-map f))
+      ( is-trunc-map-is-equiv k
+        ( is-equiv-tr-type-Ω (preserves-point-pointed-map f)))
+      ( is-trunc-map-ap-is-trunc-map k
+        ( map-pointed-map f)
+        ( H)
+        ( point-Pointed-Type A)
+        ( point-Pointed-Type A))
+```
+
 ### Faithful pointed maps induce embeddings on loop spaces
 
 ```agda

src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md

@@ -9,7 +9,11 @@ module synthetic-homotopy-theory.iterated-loop-spaces where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.function-types
+open import foundation.iterated-successors-truncation-levels
 open import foundation.iterating-functions
+open import foundation.truncated-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import structured-types.h-spaces
@@ -61,6 +65,20 @@ module _
     Ω-H-Space (iterated-loop-space n (pointed-type-H-Space X))
 ```
 
+### If A is (𝑛+𝑘)-truncated then ΩⁿA is 𝑘-truncated
+
+```agda
+is-trunc-iterated-loop-space :
+  {l : Level} (n : ℕ) (k : 𝕋) (A : Pointed-Type l) →
+  is-trunc (iterate-succ-𝕋 n k) (type-Pointed-Type A) →
+  is-trunc k (type-iterated-loop-space n A)
+is-trunc-iterated-loop-space zero-ℕ k A H = H
+is-trunc-iterated-loop-space (succ-ℕ n) k A H =
+  is-trunc-Ω k
+    ( iterated-loop-space n A)
+    ( is-trunc-iterated-loop-space n (succ-𝕋 k) A H)
+```
+
 ## See also
 
 - [Double loop spaces](synthetic-homotopy-theory.double-loop-spaces.md)

src/synthetic-homotopy-theory/loop-spaces.lagda.md

@@ -10,6 +10,8 @@ module synthetic-homotopy-theory.loop-spaces where
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.truncated-types
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import structured-types.h-spaces
@@ -23,10 +25,12 @@ open import structured-types.wild-quasigroups
 
 ## Idea
 
-The **loop space** of a [pointed type](structured-types.pointed-types.md) `A` is
-the pointed type of self-[identifications](foundation-core.identity-types.md) of
-the base point of `A`. The loop space comes equipped with a group-like structure
-induced by the groupoidal-like structure on identifications.
+The
+{{#concept "loop space" Disambiguation="of a pointed type" Agda=Ω WD="loop space" WDID=Q2066070}}
+of a [pointed type](structured-types.pointed-types.md) `A` is the pointed type
+of self-[identifications](foundation-core.identity-types.md) of the base point
+of `A`. The loop space comes equipped with a group-like structure induced by the
+groupoidal-like structure on identifications.
 
 ## Table of files directly related to loop spaces
 
@@ -48,7 +52,7 @@ module _
   refl-Ω = refl
 
   Ω : Pointed-Type l
-  Ω = pair type-Ω refl-Ω
+  Ω = (type-Ω , refl-Ω)
 ```
 
 ### The magma of loops on a pointed space
@@ -84,11 +88,12 @@ module _
   coherence-unit-laws-mul-Ω = refl
 
   Ω-H-Space : H-Space l
-  pr1 Ω-H-Space = Ω A
-  pr1 (pr2 Ω-H-Space) = mul-Ω A
-  pr1 (pr2 (pr2 Ω-H-Space)) = left-unit-law-mul-Ω
-  pr1 (pr2 (pr2 (pr2 Ω-H-Space))) = right-unit-law-mul-Ω
-  pr2 (pr2 (pr2 (pr2 Ω-H-Space))) = coherence-unit-laws-mul-Ω
+  Ω-H-Space =
+    ( Ω A ,
+      mul-Ω A ,
+      left-unit-law-mul-Ω ,
+      right-unit-law-mul-Ω ,
+      coherence-unit-laws-mul-Ω)
 ```
 
 ### The wild quasigroup of loops on a pointed space
@@ -134,14 +139,14 @@ module _
   {l1 : Level} {A : UU l1} {x y : A}
   where
 
-  equiv-tr-Ω : x ＝ y → Ω (pair A x) ≃∗ Ω (pair A y)
-  equiv-tr-Ω refl = pair id-equiv refl
+  equiv-tr-Ω : x ＝ y → Ω (A , x) ≃∗ Ω (A , y)
+  equiv-tr-Ω refl = (id-equiv , refl)
 
-  equiv-tr-type-Ω : x ＝ y → type-Ω (pair A x) ≃ type-Ω (pair A y)
+  equiv-tr-type-Ω : x ＝ y → type-Ω (A , x) ≃ type-Ω (A , y)
   equiv-tr-type-Ω p =
     equiv-pointed-equiv (equiv-tr-Ω p)
 
-  tr-type-Ω : x ＝ y → type-Ω (pair A x) → type-Ω (pair A y)
+  tr-type-Ω : x ＝ y → type-Ω (A , x) → type-Ω (A , y)
   tr-type-Ω p = map-equiv (equiv-tr-type-Ω p)
 
   is-equiv-tr-type-Ω : (p : x ＝ y) → is-equiv (tr-type-Ω p)
@@ -151,21 +156,18 @@ module _
   preserves-refl-tr-Ω refl = refl
 
   preserves-mul-tr-Ω :
-    (p : x ＝ y) (u v : type-Ω (pair A x)) →
-    Id
-      ( tr-type-Ω p (mul-Ω (pair A x) u v))
-      ( mul-Ω (pair A y) (tr-type-Ω p u) (tr-type-Ω p v))
+    (p : x ＝ y) (u v : type-Ω (A , x)) →
+    tr-type-Ω p (mul-Ω (A , x) u v) ＝
+    mul-Ω (A , y) (tr-type-Ω p u) (tr-type-Ω p v)
   preserves-mul-tr-Ω refl u v = refl
 
   preserves-inv-tr-Ω :
-    (p : x ＝ y) (u : type-Ω (pair A x)) →
-    Id
-      ( tr-type-Ω p (inv-Ω (pair A x) u))
-      ( inv-Ω (pair A y) (tr-type-Ω p u))
+    (p : x ＝ y) (u : type-Ω (A , x)) →
+    tr-type-Ω p (inv-Ω (A , x) u) ＝ inv-Ω (A , y) (tr-type-Ω p u)
   preserves-inv-tr-Ω refl u = refl
 
   eq-tr-type-Ω :
-    (p : x ＝ y) (q : type-Ω (pair A x)) →
+    (p : x ＝ y) (q : type-Ω (A , x)) →
     tr-type-Ω p q ＝ inv p ∙ (q ∙ p)
   eq-tr-type-Ω refl q = inv right-unit
 ```
@@ -181,9 +183,18 @@ module _
   where
 
   pointed-equiv-loop-pointed-identity :
-    ( pair (point-Pointed-Type A ＝ x) p) ≃∗ Ω A
-  pr1 pointed-equiv-loop-pointed-identity =
-    equiv-concat' (point-Pointed-Type A) (inv p)
-  pr2 pointed-equiv-loop-pointed-identity =
-    right-inv p
+    ( (point-Pointed-Type A ＝ x) , p) ≃∗ Ω A
+  pointed-equiv-loop-pointed-identity =
+    ( equiv-concat' (point-Pointed-Type A) (inv p) , right-inv p)
+```
+
+### The loop space of a (𝑘+1)-truncated type is 𝑘-truncated
+
+```agda
+module _
+  {l : Level} (k : 𝕋) (A : Pointed-Type l)
+  where
+
+  is-trunc-Ω : is-trunc (succ-𝕋 k) (type-Pointed-Type A) → is-trunc k (type-Ω A)
+  is-trunc-Ω H = H (point-Pointed-Type A) (point-Pointed-Type A)
 ```

src/synthetic-homotopy-theory/pushouts.lagda.md

@@ -30,6 +30,7 @@ open import reflection.erasing-equality
 
 open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.dependent-cocones-under-spans
+open import synthetic-homotopy-theory.dependent-pullback-property-pushouts
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.flattening-lemma-pushouts
 open import synthetic-homotopy-theory.induction-principle-pushouts
@@ -473,7 +474,7 @@ module _
       ( up-pushout f g)
 ```
 
-### Pushout cocones satisfy the pullback property of the pushout
+### Cocones satisfy the pullback property of the pushout if and only if they are pushouts
 
 ```agda
 module _
@@ -496,6 +497,29 @@ module _
         ( universal-property-pushout-pullback-property-pushout f g c pb)
 ```
 
+### Cocones satisfy the dependent pullback property of the pushout if and only if they are pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
+  where
+
+  abstract
+    dependent-pullback-property-pushout-is-pushout :
+      is-pushout f g c → dependent-pullback-property-pushout f g c
+    dependent-pullback-property-pushout-is-pushout po =
+      dependent-pullback-property-pullback-property-pushout f g c
+        ( pullback-property-pushout-is-pushout f g c po)
+
+  abstract
+    is-pushout-dependent-pullback-property-pushout :
+      dependent-pullback-property-pushout f g c → is-pushout f g c
+    is-pushout-dependent-pullback-property-pushout pb =
+      is-pushout-pullback-property-pushout f g c
+        ( pullback-property-dependent-pullback-property-pushout f g c pb)
+```
+
 ### Fibers of the cogap map
 
 We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map

src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md

@@ -475,6 +475,21 @@ the canonical maps `X → X ⋊∗ Y` and `Y → X ⋉∗ Y`, i.e., we have push
 
 > This remains to be formalized.
 
+### The smash product as a bipointed pushout
+
+Given two pointed types `X` and `Y`, the smash product is the pushout
+{{#cite Ljungström24}}
+
+```text
+  X + Y ------> X × Y
+    |             |
+    |             |
+    ∨           ⌜ ∨
+  1 + 1 ------> X ∧ Y.
+```
+
+> This remains to be formalized.
+
 ## References
 
 {{#bibliography}}

src/univalent-combinatorics/subcounting.lagda.md

@@ -149,7 +149,7 @@ abstract
 propositional truncations, we have an embedding `║X║₋₁ ↪ ║Fin k║₋₁`. By
 induction, if `k ≐ 0` then `║Fin k║₋₁ ≃ 0 ≃ Fin 0` and so `║X║₋₁ ↪ Fin 0` is a
 subcounting. Otherwise, if `k ≐ j + 1`, then `║Fin k║₋₁ ≃ 1 ≃ Fin 1` and again
-`║X║₋₁ ↪ Fin 1` is a subcounting.
+`║X║₋₁ ↪ Fin 1` is a subcounting. ∎
 
 ```agda
 module _
@@ -173,8 +173,8 @@ We reproduce a proof given by
 [Gro-Tsen](https://mathoverflow.net/users/17064/gro-tsen) in this MathOverflow
 answer: <https://mathoverflow.net/a/433318>.
 
-**Proof.** Let $X$ be a type with a subcounting $ι : X ↪ Fin n$, and let
-$f : X ↪ X$ be an arbitrary self-embedding. It suffices to prove $f$ is
+**Proof.** Let $X$ be a type with a subcounting $ι : X ↪ \operatorname{Fin}n$,
+and let $f : X ↪ X$ be an arbitrary self-embedding. It suffices to prove $f$ is
 surjective, so assume given an $x : X$ where we want to show there exists
 $z : X$ such that $f(z) ＝ x$. The mapping $i ↦ fⁱ(x)$ defines an $ℕ$-indexed
 sequence of elements of $X$. Since the