chore: Fix two sections on connected/truncated maps (#1727)

A couple of section headers stated logical equivalences but only
demonstrated one of the two directions.

Author: fredrik-bakke

src/foundation-core/truncated-maps.lagda.md

@@ -329,13 +329,14 @@ module _
   {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
   where
 
-  is-trunc-map-is-trunc-succ-codomain-is-contr-domain :
-    is-contr A →
-    is-trunc (succ-𝕋 k) B →
-    is-trunc-map k f
-  is-trunc-map-is-trunc-succ-codomain-is-contr-domain c tB u =
-    is-trunc-equiv k
-      ( f (center c) ＝ u)
-      ( left-unit-law-Σ-is-contr c (center c))
-      ( tB (f (center c)) u)
+  abstract
+    is-trunc-map-is-trunc-succ-codomain-is-contr-domain :
+      is-contr A →
+      is-trunc (succ-𝕋 k) B →
+      is-trunc-map k f
+    is-trunc-map-is-trunc-succ-codomain-is-contr-domain c tB u =
+      is-trunc-equiv k
+        ( f (center c) ＝ u)
+        ( left-unit-law-Σ-is-contr c (center c))
+        ( tB (f (center c)) u)
 ```

src/foundation/connected-maps.lagda.md

@@ -17,6 +17,7 @@ open import foundation.iterated-successors-truncation-levels
 open import foundation.precomposition-dependent-functions
 open import foundation.structure-identity-principle
 open import foundation.subtype-identity-principle
+open import foundation.transport-along-identifications
 open import foundation.truncated-types
 open import foundation.truncation-levels
 open import foundation.truncations
@@ -497,38 +498,42 @@ module _
       dependent-universal-property-trunc
 ```
 
-### A map `f : A → B` is `k`-connected if and only if precomposing dependent functions into `k+n`-truncated types is an `n-2`-truncated map for all `n : ℕ`
+### Given a `k`-connected map `f` then precomposing dependent functions into `2+k+n`-truncated types by `f` is an `n`-truncated map
 
 ```agda
-abstract
-  is-trunc-map-precomp-Π-is-connected-map :
-    {l1 l2 l3 : Level} (k n : 𝕋) →
-    {A : UU l1} {B : UU l2} {f : A → B} → is-connected-map k f →
-    (P : B → Truncated-Type l3 (add+2-𝕋 n k)) →
-    is-trunc-map
-      ( n)
-      ( precomp-Π f (λ b → type-Truncated-Type (P b)))
-  is-trunc-map-precomp-Π-is-connected-map k neg-two-𝕋 H P =
-    is-contr-map-is-equiv
-      ( dependent-universal-property-is-connected-map k H
-        ( λ b →
-          pair
-            ( type-Truncated-Type (P b))
-            ( is-trunc-eq
-              ( left-unit-law-add+2-𝕋 k)
-              ( is-trunc-type-Truncated-Type (P b)))))
-  is-trunc-map-precomp-Π-is-connected-map k (succ-𝕋 n) H P =
-    is-trunc-map-succ-precomp-Π
-      ( λ g h →
-        is-trunc-map-precomp-Π-is-connected-map k n H
-          ( λ b →
-            pair
-              ( eq-value g h b)
-              ( is-trunc-eq
-                ( left-successor-law-add+2-𝕋 k n)
-                ( is-trunc-type-Truncated-Type (P b))
-                ( g b)
-                ( h b))))
+module _
+  {l1 l2 : Level}
+  {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  abstract
+    is-trunc-map-precomp-Π-is-connected-map :
+      (k n : 𝕋) →
+      is-connected-map k f →
+      {l3 : Level} (P : B → Truncated-Type l3 (add+2-𝕋 k n)) →
+      is-trunc-map n (precomp-Π f (type-Truncated-Type ∘ P))
+    is-trunc-map-precomp-Π-is-connected-map k neg-two-𝕋 H P =
+      is-contr-map-is-equiv
+        ( dependent-universal-property-is-connected-map k H P)
+    is-trunc-map-precomp-Π-is-connected-map k (succ-𝕋 n) H P =
+      is-trunc-map-succ-precomp-Π
+        ( λ g h →
+          is-trunc-map-precomp-Π-is-connected-map k n H
+            ( λ b → Id-Truncated-Type (P b) (g b) (h b)))
+
+  abstract
+    is-trunc-map-precomp-Π-is-connected-map' :
+      (k n : 𝕋) →
+      is-connected-map k f →
+      {l3 : Level} (P : B → Truncated-Type l3 (add+2-𝕋 n k)) →
+      is-trunc-map n (precomp-Π f (type-Truncated-Type ∘ P))
+    is-trunc-map-precomp-Π-is-connected-map' k n H P =
+      is-trunc-map-precomp-Π-is-connected-map k n H
+        ( λ x →
+          ( type-Truncated-Type (P x)) ,
+          ( is-trunc-eq
+            ( commutative-add+2-𝕋 n k)
+            ( is-trunc-type-Truncated-Type (P x))))
 ```
 
 ### Characterization of the identity type of `Connected-Map l2 k A`

src/foundation/epimorphisms-with-respect-to-sets.lagda.md

@@ -80,27 +80,21 @@ abstract
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
     is-epimorphism-Set f → is-surjective f
   is-surjective-is-epimorphism-Set {l1} {l2} {A} {B} {f} H b =
-    map-equiv
-      ( equiv-eq
-        ( ap
-          ( pr1)
-          ( htpy-eq
-            ( is-injective-is-emb
-              ( H (Prop-Set (l1 ⊔ l2)))
-              { g}
-              { h}
-              ( eq-htpy
-                ( λ a →
-                  eq-iff
-                    ( λ _ → unit-trunc-Prop (pair a refl))
-                    ( λ _ → raise-star))))
-            ( b))))
+    map-eq
+      ( ap
+        ( pr1)
+        ( htpy-eq
+          ( is-injective-is-emb
+            ( H (Prop-Set (l1 ⊔ l2)))
+            { λ _ → raise-unit-Prop (l1 ⊔ l2)}
+            { λ y → exists-structure-Prop A (λ x → f x ＝ y)}
+            ( eq-htpy
+              ( λ a →
+                eq-iff
+                  ( λ _ → unit-trunc-Prop (a , refl))
+                  ( λ _ → raise-star))))
+          ( b)))
       ( raise-star)
-    where
-    g : B → Prop (l1 ⊔ l2)
-    g y = raise-unit-Prop (l1 ⊔ l2)
-    h : B → Prop (l1 ⊔ l2)
-    h y = exists-structure-Prop A (λ x → f x ＝ y)
 ```
 
 ### There is at most one extension of a map into a set along a surjection

src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md

@@ -262,13 +262,13 @@ module _
 We consider the commutative diagram for any `k`-type `X`:
 
 ```text
-             horizontal-map-cocone
- (B → X) <---------------------------- cocone f f X
-    |                  ≃                  ∧
- id | ≃                                 ≃ | (universal property)
-    ∨                                     |
- (B → X) ------------------------> (pushout f f → X)
-          precomp (codiagonal f)
+              horizontal-map-cocone
+  (B → X) <---------------------------- cocone f f X
+     |                  ≃                  ∧
+  id | ≃                                 ≃ | (universal property)
+     ∨                                     |
+  (B → X) ------------------------> (pushout f f → X)
+           precomp (codiagonal f)
 ```
 
 Since the top (in case `f` is epic), left and right maps are all equivalences,
@@ -299,10 +299,8 @@ module _
               ( f)
               ( e)
               ( X)))
-          ( is-equiv-htpy
-            ( id)
-            ( λ g → eq-htpy (λ b → ap g (compute-inl-codiagonal-map f b)))
-            ( is-equiv-id)))
+          ( is-equiv-htpy-id
+            ( λ g → eq-htpy (λ b → ap g (compute-inl-codiagonal-map f b)))))
 ```
 
 ### A map is a `k`-epimorphism if its codiagonal is a `k`-equivalence
@@ -323,10 +321,8 @@ module _
       ( horizontal-map-cocone f f)
       ( ( map-equiv (equiv-up-pushout f f (type-Truncated-Type X))) ∘
         ( precomp (codiagonal-map f) (type-Truncated-Type X)))
-      ( is-equiv-htpy
-        ( id)
-        ( λ g → eq-htpy (λ b → ap g (compute-inl-codiagonal-map f b)))
-        ( is-equiv-id))
+      ( is-equiv-htpy-id
+        ( λ g → eq-htpy (λ b → ap g (compute-inl-codiagonal-map f b))))
       ( is-equiv-comp
         ( map-equiv (equiv-up-pushout f f (type-Truncated-Type X)))
         ( precomp (codiagonal-map f) (type-Truncated-Type X))
@@ -336,11 +332,10 @@ module _
   is-epimorphism-is-truncation-equivalence-codiagonal-map-Truncated-Type :
     is-truncation-equivalence k (codiagonal-map f) →
     is-epimorphism-Truncated-Type k f
-  is-epimorphism-is-truncation-equivalence-codiagonal-map-Truncated-Type e X =
+  is-epimorphism-is-truncation-equivalence-codiagonal-map-Truncated-Type e =
     is-epimorphism-is-equiv-horizontal-map-cocone-Truncated-Type k f
       ( is-equiv-horizontal-map-cocone-is-truncation-equivalence-codiagonal-map
         ( e))
-      ( X)
 ```
 
 ### A map is a `k`-epimorphism if and only if its codiagonal is `k`-connected

src/foundation/iterating-functions.lagda.md

@@ -142,48 +142,53 @@ module _
 ```agda
 module _
   {l : Level} {X : UU l} {f : X → X}
-  where abstract
+  where
 
-  is-equiv-iterate : (n : ℕ) → is-equiv f → is-equiv (iterate n f)
-  is-equiv-iterate =
-    is-in-function-class-iterate is-equiv-id (λ h g H G → is-equiv-comp h g G H)
+  abstract
+    is-equiv-iterate : (n : ℕ) → is-equiv f → is-equiv (iterate n f)
+    is-equiv-iterate =
+      is-in-function-class-iterate is-equiv-id
+        ( λ h g H G → is-equiv-comp h g G H)
 ```
 
 ### Iterates of embeddings are embeddings
 
 ```agda
 module _
   {l : Level} {X : UU l} {f : X → X}
-  where abstract
+  where
 
-  is-emb-iterate : (n : ℕ) → is-emb f → is-emb (iterate n f)
-  is-emb-iterate = is-in-function-class-iterate is-emb-id is-emb-comp
+  abstract
+    is-emb-iterate : (n : ℕ) → is-emb f → is-emb (iterate n f)
+    is-emb-iterate = is-in-function-class-iterate is-emb-id is-emb-comp
 ```
 
 ### Iterates of truncated maps are truncated
 
 ```agda
 module _
   {l : Level} (k : 𝕋) {X : UU l} {f : X → X}
-  where abstract
+  where
 
-  is-trunc-map-iterate :
-    (n : ℕ) → is-trunc-map k f → is-trunc-map k (iterate n f)
-  is-trunc-map-iterate =
-    is-in-function-class-iterate (is-trunc-map-id k) (is-trunc-map-comp k)
+  abstract
+    is-trunc-map-iterate :
+      (n : ℕ) → is-trunc-map k f → is-trunc-map k (iterate n f)
+    is-trunc-map-iterate =
+      is-in-function-class-iterate (is-trunc-map-id k) (is-trunc-map-comp k)
 ```
 
 ### Iterates of propositional maps are propositional
 
 ```agda
 module _
   {l : Level} (k : 𝕋) {X : UU l} {f : X → X}
-  where abstract
+  where
 
-  is-prop-map-iterate :
-    (n : ℕ) → is-prop-map f → is-prop-map (iterate n f)
-  is-prop-map-iterate =
-    is-in-function-class-iterate is-prop-map-id is-prop-map-comp
+  abstract
+    is-prop-map-iterate :
+      (n : ℕ) → is-prop-map f → is-prop-map (iterate n f)
+    is-prop-map-iterate =
+      is-in-function-class-iterate is-prop-map-id is-prop-map-comp
 ```
 
 ## External links

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

@@ -226,23 +226,42 @@ module _
 ### Precomposing functions `Π B C` by `f : A → B` is `k+1`-truncated if and only if precomposing homotopies is `k`-truncated
 
 ```agda
-is-trunc-map-succ-precomp-Π :
+module _
   {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B}
-  {C : B → UU l3} →
-  ((g h : (b : B) → C b) → is-trunc-map k (precomp-Π f (eq-value g h))) →
-  is-trunc-map (succ-𝕋 k) (precomp-Π f C)
-is-trunc-map-succ-precomp-Π {k = k} {f = f} {C = C} H =
-  is-trunc-map-succ-is-trunc-map-ap k (precomp-Π f C)
-    ( λ g h →
+  {C : B → UU l3}
+  where
+
+  abstract
+    is-trunc-map-succ-precomp-Π :
+      ((g h : (b : B) → C b) → is-trunc-map k (precomp-Π f (eq-value g h))) →
+      is-trunc-map (succ-𝕋 k) (precomp-Π f C)
+    is-trunc-map-succ-precomp-Π H =
+      is-trunc-map-succ-is-trunc-map-ap k (precomp-Π f C)
+        ( λ g h →
+          is-trunc-map-top-is-trunc-map-bottom-is-equiv k
+            ( ap (precomp-Π f C))
+            ( htpy-eq)
+            ( htpy-eq)
+            ( precomp-Π f (eq-value g h))
+            ( coherence-htpy-eq-ap-precomp-Π f)
+            ( funext g h)
+            ( funext (g ∘ f) (h ∘ f))
+            ( H g h))
+
+  abstract
+    is-trunc-map-precomp-Π-eq-value-is-trunc-map-succ-precomp-Π :
+      is-trunc-map (succ-𝕋 k) (precomp-Π f C) →
+      (g h : (b : B) → C b) → is-trunc-map k (precomp-Π f (eq-value g h))
+    is-trunc-map-precomp-Π-eq-value-is-trunc-map-succ-precomp-Π H g h =
       is-trunc-map-top-is-trunc-map-bottom-is-equiv k
-        ( ap (precomp-Π f C))
-        ( htpy-eq)
-        ( htpy-eq)
         ( precomp-Π f (eq-value g h))
-        ( coherence-htpy-eq-ap-precomp-Π f)
-        ( funext g h)
-        ( funext (g ∘ f) (h ∘ f))
-        ( H g h))
+        ( eq-htpy)
+        ( eq-htpy)
+        ( ap (precomp-Π f C))
+        ( coherence-eq-htpy-ap-precomp-Π f)
+        ( is-equiv-eq-htpy g h)
+        ( is-equiv-eq-htpy (g ∘ f) (h ∘ f))
+        ( is-trunc-map-ap-is-trunc-map-succ k (precomp-Π f C) H g h)
 ```
 
 ### The dependent precomposition map at a dependent pair type

src/foundation/surjective-maps.lagda.md

@@ -631,7 +631,7 @@ is-trunc-map-precomp-Π-is-surjective :
   (P : B → Truncated-Type l3 (succ-𝕋 k)) →
   is-trunc-map k (precomp-Π f (λ b → type-Truncated-Type (P b)))
 is-trunc-map-precomp-Π-is-surjective k H =
-  is-trunc-map-precomp-Π-is-connected-map
+  is-trunc-map-precomp-Π-is-connected-map'
     ( neg-one-𝕋)
     ( k)
     ( is-neg-one-connected-map-is-surjective H)