Miscellaneous edits from #1547 (#1667)

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-core/commuting-squares-of-maps.lagda.md

@@ -82,6 +82,14 @@ module _
   pasting-horizontal-coherence-square-maps sq-left sq-right =
     (bottom-right ·l sq-left) ∙h (sq-right ·r top-left)
 
+  pasting-horizontal-coherence-square-maps' :
+    coherence-square-maps' top-left left mid bottom-left →
+    coherence-square-maps' top-right mid right bottom-right →
+    coherence-square-maps'
+      (top-right ∘ top-left) left right (bottom-right ∘ bottom-left)
+  pasting-horizontal-coherence-square-maps' sq-left sq-right =
+    (sq-right ·r top-left) ∙h (bottom-right ·l sq-left)
+
   pasting-horizontal-up-to-htpy-coherence-square-maps :
     {top : A → C} (H : coherence-triangle-maps top top-right top-left)
     {bottom : X → Z}

src/foundation-core/contractible-types.lagda.md

@@ -27,8 +27,8 @@ open import foundation-core.transport-along-identifications
 
 ## Idea
 
-Contractible types are types that have, up to identification, exactly one
-element.
+{{#concept "Contractible types" Agda=is-contr}} are types that have, up to
+[identification](foundation-core.identity-types.md), exactly one element.
 
 ## Definition
 
@@ -93,8 +93,7 @@ module _
 
   abstract
     is-contr-equiv : A ≃ B → is-contr B → is-contr A
-    is-contr-equiv (e , is-equiv-e) is-contr-B =
-      is-contr-is-equiv e is-equiv-e is-contr-B
+    is-contr-equiv (e , is-equiv-e) = is-contr-is-equiv e is-equiv-e
 
 module _
   {l1 l2 : Level} (A : UU l1) {B : UU l2}
@@ -103,16 +102,14 @@ module _
   abstract
     is-contr-is-equiv' :
       (f : A → B) → is-equiv f → is-contr A → is-contr B
-    is-contr-is-equiv' f is-equiv-f is-contr-A =
+    is-contr-is-equiv' f is-equiv-f =
       is-contr-is-equiv A
         ( map-inv-is-equiv is-equiv-f)
         ( is-equiv-map-inv-is-equiv is-equiv-f)
-        ( is-contr-A)
 
   abstract
     is-contr-equiv' : (e : A ≃ B) → is-contr A → is-contr B
-    is-contr-equiv' (pair e is-equiv-e) is-contr-A =
-      is-contr-is-equiv' e is-equiv-e is-contr-A
+    is-contr-equiv' (e , is-equiv-e) = is-contr-is-equiv' e is-equiv-e
 
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
@@ -128,7 +125,8 @@ module _
         ( contraction is-contr-A)
 
   equiv-is-contr : is-contr A → is-contr B → A ≃ B
-  pr1 (equiv-is-contr is-contr-A is-contr-B) a = center is-contr-B
+  pr1 (equiv-is-contr is-contr-A is-contr-B) a =
+    center is-contr-B
   pr2 (equiv-is-contr is-contr-A is-contr-B) =
     is-equiv-is-contr _ is-contr-A is-contr-B
 ```

src/foundation-core/dependent-identifications.lagda.md

@@ -47,6 +47,16 @@ refl-dependent-identification :
   {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x : A} {y : B x} →
   dependent-identification B refl y y
 refl-dependent-identification B = refl
+
+dependent-identification' :
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x x' : A} (p : x ＝ x') →
+  B x → B x' → UU l2
+dependent-identification' B p u v = (u ＝ inv-tr B p v)
+
+refl-dependent-identification' :
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x : A} {y : B x} →
+  dependent-identification' B refl y y
+refl-dependent-identification' B = refl
 ```
 
 ### Iterated dependent identifications

src/foundation-core/embeddings.lagda.md

@@ -113,7 +113,7 @@ module _
   where
 
   is-emb-id : is-emb (id {A = A})
-  is-emb-id x y = is-equiv-htpy id ap-id is-equiv-id
+  is-emb-id x y = is-equiv-htpy-id ap-id
 
   id-emb : A ↪ A
   pr1 id-emb = id

src/foundation-core/equivalences.lagda.md

@@ -500,6 +500,12 @@ module _
     htpy-map-inv-is-invertible H
       ( is-invertible-is-equiv F)
       ( is-invertible-is-equiv G)
+
+is-equiv-htpy-id : {l : Level} {A : UU l} {f : A → A} → f ~ id → is-equiv f
+is-equiv-htpy-id H = is-equiv-htpy id H is-equiv-id
+
+is-equiv-htpy-id' : {l : Level} {A : UU l} {f : A → A} → id ~ f → is-equiv f
+is-equiv-htpy-id' H = is-equiv-htpy' id H is-equiv-id
 ```
 
 ### Any retraction of an equivalence is an equivalence

src/foundation-core/fibers-of-maps.lagda.md

@@ -455,7 +455,19 @@ module _
       is-retraction-map-inv-equiv-fiber-htpy
 
   equiv-fiber-htpy : fiber f y ≃ fiber g y
-  equiv-fiber-htpy = map-equiv-fiber-htpy , is-equiv-map-equiv-fiber-htpy
+  equiv-fiber-htpy =
+    ( map-equiv-fiber-htpy , is-equiv-map-equiv-fiber-htpy)
+
+  is-equiv-map-inv-equiv-fiber-htpy : is-equiv map-inv-equiv-fiber-htpy
+  is-equiv-map-inv-equiv-fiber-htpy =
+    is-equiv-is-invertible
+      ( map-equiv-fiber-htpy)
+      ( is-retraction-map-inv-equiv-fiber-htpy)
+      ( is-section-map-inv-equiv-fiber-htpy)
+
+  inv-equiv-fiber-htpy : fiber g y ≃ fiber f y
+  inv-equiv-fiber-htpy =
+    ( map-inv-equiv-fiber-htpy , is-equiv-map-inv-equiv-fiber-htpy)
 ```
 
 We repeat the construction for `fiber'`.

src/foundation-core/functoriality-dependent-function-types.lagda.md

@@ -96,15 +96,20 @@ module _
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
   where
 
+  abstract
+    is-contr-map-map-Π-is-fiberwise-contr-map :
+      {f : (i : I) → A i → B i} →
+      ((i : I) → is-contr-map (f i)) → is-contr-map (map-Π f)
+    is-contr-map-map-Π-is-fiberwise-contr-map H g =
+      is-contr-equiv' _ (compute-fiber-map-Π _ g) (is-contr-Π (λ i → H i (g i)))
+
   abstract
     is-equiv-map-Π-is-fiberwise-equiv :
       {f : (i : I) → A i → B i} → is-fiberwise-equiv f → is-equiv (map-Π f)
     is-equiv-map-Π-is-fiberwise-equiv is-equiv-f =
       is-equiv-is-contr-map
-        ( λ g →
-          is-contr-equiv' _
-            ( compute-fiber-map-Π _ g)
-            ( is-contr-Π (λ i → is-contr-map-is-equiv (is-equiv-f i) (g i))))
+        ( is-contr-map-map-Π-is-fiberwise-contr-map
+          ( is-contr-map-is-equiv ∘ is-equiv-f))
 
   equiv-Π-equiv-family :
     (e : (i : I) → A i ≃ B i) → ((i : I) → A i) ≃ ((i : I) → B i)

src/foundation-core/precomposition-dependent-functions.lagda.md

@@ -50,7 +50,11 @@ module _
   {f g : A → B} (H : f ~ g) (C : B → UU l3) (h : (y : B) → C y)
   where
 
-  htpy-precomp-Π :
+  htpy-htpy-precomp-Π :
     dependent-homotopy (λ _ → C) H (precomp-Π f C h) (precomp-Π g C h)
-  htpy-precomp-Π x = apd h (H x)
+  htpy-htpy-precomp-Π x = apd h (H x)
+
+  htpy-htpy-precomp-Π' :
+    dependent-homotopy' (λ _ → C) H (precomp-Π f C h) (precomp-Π g C h)
+  htpy-htpy-precomp-Π' x = apd' h (H x)
 ```

src/foundation-core/transport-along-identifications.lagda.md

@@ -32,9 +32,15 @@ recorded in
 ### Transport
 
 ```agda
-tr :
-  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x y : A} (p : x ＝ y) → B x → B y
-tr B refl b = b
+module _
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x y : A}
+  where
+
+  tr : x ＝ y → B x → B y
+  tr refl b = b
+
+  inv-tr : y ＝ x → B x → B y
+  inv-tr p = tr (inv p)
 ```
 
 ## Properties
@@ -96,6 +102,11 @@ module _
     {x y z : A} (p : x ＝ y) (q : y ＝ z) (b : B x) →
     tr B (p ∙ q) b ＝ tr B q (tr B p b)
   tr-concat refl q b = refl
+
+  comp-tr :
+    {x y z : A} (p : x ＝ y) (q : y ＝ z) (b : B x) →
+    tr B q (tr B p b) ＝ tr B (p ∙ q) b
+  comp-tr p q b = inv (tr-concat p q b)
 ```
 
 ### Transposing transport along the inverse of an identification