Quasiidempotence is not a proposition (#1127)

Follow-up to #1105.

src/foundation/constant-type-families.lagda.md

@@ -10,13 +10,13 @@ module foundation.constant-type-families where
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.identity-types
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-identifications
 open import foundation-core.dependent-identifications
 open import foundation-core.equivalences
-open import foundation-core.identity-types
 ```
 
 </details>
@@ -76,6 +76,26 @@ tr-constant-type-family :
 tr-constant-type-family refl b = refl
 ```
 
+### Computing dependent identifications in constant type families
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  map-compute-dependent-identification-constant-type-family :
+    {x y : A} (p : x ＝ y) {x' y' : B} →
+    x' ＝ y' → dependent-identification (λ _ → B) p x' y'
+  map-compute-dependent-identification-constant-type-family p {x'} q =
+    tr-constant-type-family p x' ∙ q
+
+  compute-dependent-identification-constant-type-family :
+    {x y : A} (p : x ＝ y) {x' y' : B} →
+    (x' ＝ y') ≃ dependent-identification (λ _ → B) p x' y'
+  compute-dependent-identification-constant-type-family p {x'} {y'} =
+    equiv-concat (tr-constant-type-family p x') y'
+```
+
 ### Dependent action on paths of sections of standard constant type families
 
 ```agda

src/foundation/dependent-identifications.lagda.md

@@ -9,8 +9,10 @@ open import foundation-core.dependent-identifications public
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.strictly-right-unital-concatenation-identifications
 open import foundation.transport-along-higher-identifications
 open import foundation.universe-levels
 
@@ -26,7 +28,7 @@ open import foundation-core.transport-along-identifications
 ## Idea
 
 We characterize dependent paths in the family of depedent paths; define the
-groupoidal operators on dependent paths; define the cohrences paths: prove the
+groupoidal operators on dependent paths; define the coherence paths; prove the
 operators are equivalences.
 
 ## Properites
@@ -120,12 +122,35 @@ module _
     dependent-identification B (p ∙ q) x' z'
   concat-dependent-identification refl q refl q' = q'
 
-  compute-concat-dependent-identification-refl :
+  compute-concat-dependent-identification-left-base-refl :
     { y z : A} (q : y ＝ z) →
     { x' y' : B y} {z' : B z} (p' : x' ＝ y') →
     ( q' : dependent-identification B q y' z') →
-    ( concat-dependent-identification refl q p' q') ＝ ap (tr B q) p' ∙ q'
-  compute-concat-dependent-identification-refl refl refl q' = refl
+    concat-dependent-identification refl q p' q' ＝ ap (tr B q) p' ∙ q'
+  compute-concat-dependent-identification-left-base-refl q refl q' = refl
+```
+
+#### Strictly right unital concatenation of dependent identifications
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2)
+  where
+
+  right-strict-concat-dependent-identification :
+    {x y z : A} (p : x ＝ y) (q : y ＝ z) {x' : B x} {y' : B y} {z' : B z} →
+    dependent-identification B p x' y' →
+    dependent-identification B q y' z' →
+    dependent-identification B (p ∙ᵣ q) x' z'
+  right-strict-concat-dependent-identification p refl p' q' = p' ∙ᵣ q'
+
+  compute-right-strict-concat-dependent-identification-right-base-refl :
+    { x y : A} (p : x ＝ y) →
+    { x' : B x} {y' z' : B y} (p' : dependent-identification B p x' y') →
+    ( q' : y' ＝ z') →
+    right-strict-concat-dependent-identification p refl p' q' ＝ p' ∙ᵣ q'
+  compute-right-strict-concat-dependent-identification-right-base-refl q p' q' =
+    refl
 ```
 
 #### Inverses of dependent identifications

src/foundation/quasicoherently-idempotent-maps.lagda.md

@@ -8,11 +8,15 @@ module foundation.quasicoherently-idempotent-maps where
 
 ```agda
 open import foundation.1-types
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-pair-types
 open import foundation.homotopy-algebra
 open import foundation.idempotent-maps
+open import foundation.identity-types
+open import foundation.negated-equality
 open import foundation.negation
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 open import foundation.whiskering-higher-homotopies-composition
 open import foundation.whiskering-homotopies-composition
@@ -24,6 +28,7 @@ open import foundation-core.retractions
 open import foundation-core.sets
 
 open import synthetic-homotopy-theory.circle
+open import synthetic-homotopy-theory.loop-homotopy-circle
 ```
 
 </details>
@@ -54,13 +59,13 @@ corresponds to the definition of a _quasiidempotent map_ in {{#cite Shu17}} and
 ### The structure of quasicoherent idempotence on maps
 
 ```agda
-coherence-is-quasicoherently-idempotent :
+quasicoherence-is-idempotent :
   {l : Level} {A : UU l} (f : A → A) → f ∘ f ~ f → UU l
-coherence-is-quasicoherently-idempotent f I = f ·l I ~ I ·r f
+quasicoherence-is-idempotent f I = f ·l I ~ I ·r f
 
 is-quasicoherently-idempotent : {l : Level} {A : UU l} → (A → A) → UU l
 is-quasicoherently-idempotent f =
-  Σ (f ∘ f ~ f) (coherence-is-quasicoherently-idempotent f)
+  Σ (f ∘ f ~ f) (quasicoherence-is-idempotent f)
 
 module _
   {l : Level} {A : UU l} {f : A → A} (H : is-quasicoherently-idempotent f)
@@ -70,7 +75,7 @@ module _
   is-idempotent-is-quasicoherently-idempotent = pr1 H
 
   coh-is-quasicoherently-idempotent :
-    coherence-is-quasicoherently-idempotent f
+    quasicoherence-is-idempotent f
       ( is-idempotent-is-quasicoherently-idempotent)
   coh-is-quasicoherently-idempotent = pr2 H
 ```
@@ -99,7 +104,7 @@ module _
       ( is-quasicoherently-idempotent-quasicoherently-idempotent-map)
 
   coh-quasicoherently-idempotent-map :
-    coherence-is-quasicoherently-idempotent
+    quasicoherence-is-idempotent
       ( map-quasicoherently-idempotent-map)
       ( is-idempotent-quasicoherently-idempotent-map)
   coh-quasicoherently-idempotent-map =
@@ -114,16 +119,44 @@ module _
 
 ## Properties
 
+### The identity function is quasicoherently idempotent
+
+In fact, any idempotence witness of the identity function is quasicoherent.
+
+```agda
+module _
+  {l : Level} {A : UU l} (H : is-idempotent (id {A = A}))
+  where
+
+  quasicoherence-is-idempotent-id :
+    quasicoherence-is-idempotent id H
+  quasicoherence-is-idempotent-id = left-unit-law-left-whisker-comp H
+
+  is-quasicoherently-idempotent-is-idempotent-id :
+    is-quasicoherently-idempotent (id {A = A})
+  is-quasicoherently-idempotent-is-idempotent-id =
+    ( H , quasicoherence-is-idempotent-id)
+
+module _
+  {l : Level} {A : UU l}
+  where
+
+  is-quasicoherently-idempotent-id :
+    is-quasicoherently-idempotent (id {A = A})
+  is-quasicoherently-idempotent-id =
+    is-quasicoherently-idempotent-is-idempotent-id refl-htpy
+```
+
 ### Being quasicoherently idempotent on a set is a property
 
 ```agda
 module _
   {l : Level} {A : UU l} (is-set-A : is-set A) (f : A → A)
   where
 
-  is-prop-coherence-is-quasicoherently-idempotent-is-set :
-    (I : f ∘ f ~ f) → is-prop (coherence-is-quasicoherently-idempotent f I)
-  is-prop-coherence-is-quasicoherently-idempotent-is-set I =
+  is-prop-quasicoherence-is-idempotent-is-set :
+    (I : f ∘ f ~ f) → is-prop (quasicoherence-is-idempotent f I)
+  is-prop-quasicoherence-is-idempotent-is-set I =
     is-prop-Π
       ( λ x →
         is-set-is-prop
@@ -136,7 +169,7 @@ module _
   is-prop-is-quasicoherently-idempotent-is-set =
     is-prop-Σ
       ( is-prop-is-idempotent-is-set is-set-A f)
-      ( is-prop-coherence-is-quasicoherently-idempotent-is-set)
+      ( is-prop-quasicoherence-is-idempotent-is-set)
 
   is-quasicoherently-idempotent-is-set-Prop : Prop l
   is-quasicoherently-idempotent-is-set-Prop =
@@ -171,16 +204,22 @@ Two distinct witnesses that it is idempotent are given by `t ↦ refl` and
 `t ↦ loop`. Both of these are quasicoherent, because
 
 ```text
-  coherence-is-quasicoherently-idempotent id I ≐ (id ·l I ~ I ·r id) ≃ (I ~ I).
+  quasicoherence-is-idempotent id I ≐ (id ·l I ~ I ·r id) ≃ (I ~ I).
 ```
 
-To formalize this result, we first need that the loop of the circle is
-nontrivial.
-
-```text
-is-not-prop-is-quasicoherently-idempotent-id-circle :
+```agda
+is-not-prop-is-quasicoherently-idempotent-id-𝕊¹ :
   ¬ (is-prop (is-quasicoherently-idempotent (id {A = 𝕊¹})))
-is-not-prop-is-quasicoherently-idempotent-id-circle = ?
+is-not-prop-is-quasicoherently-idempotent-id-𝕊¹ H =
+  nonequal-Π
+    ( loop-htpy-𝕊¹)
+    ( refl-htpy)
+    ( base-𝕊¹)
+    ( is-not-refl-ev-base-loop-htpy-𝕊¹)
+    ( ap pr1
+      ( eq-is-prop H
+        { is-quasicoherently-idempotent-is-idempotent-id loop-htpy-𝕊¹}
+        { is-quasicoherently-idempotent-is-idempotent-id refl-htpy}))
 ```
 
 ### Idempotent maps on sets are quasicoherently idempotent
@@ -208,11 +247,11 @@ module _
   (i : B → A) (r : A → B) (H : is-retraction i r)
   where
 
-  coherence-is-quasicoherently-idempotent-inclusion-retraction :
-    coherence-is-quasicoherently-idempotent
+  quasicoherence-is-idempotent-inclusion-retraction :
+    quasicoherence-is-idempotent
       ( i ∘ r)
       ( is-idempotent-inclusion-retraction i r H)
-  coherence-is-quasicoherently-idempotent-inclusion-retraction =
+  quasicoherence-is-idempotent-inclusion-retraction =
     ( inv-preserves-comp-left-whisker-comp i r (i ·l H ·r r)) ∙h
     ( double-whisker-comp²
       ( i)
@@ -223,7 +262,7 @@ module _
     is-quasicoherently-idempotent (i ∘ r)
   is-quasicoherently-idempotent-inclusion-retraction =
     ( is-idempotent-inclusion-retraction i r H ,
-      coherence-is-quasicoherently-idempotent-inclusion-retraction)
+      quasicoherence-is-idempotent-inclusion-retraction)
 ```
 
 ### Quasicoherent idempotence is preserved by homotopies
@@ -237,13 +276,13 @@ module _
   where
 
   abstract
-    coherence-is-quasicoherently-idempotent-htpy :
+    quasicoherence-is-idempotent-htpy :
       (H : g ~ f) →
-      coherence-is-quasicoherently-idempotent g
+      quasicoherence-is-idempotent g
         ( is-idempotent-htpy
           ( is-idempotent-is-quasicoherently-idempotent F)
           ( H))
-    coherence-is-quasicoherently-idempotent-htpy H =
+    quasicoherence-is-idempotent-htpy H =
       homotopy-reasoning
       ( g ·l is-idempotent-htpy I H)
       ~ ( H ·r (g ∘ g)) ∙h
@@ -317,7 +356,7 @@ module _
       ( is-idempotent-is-quasicoherently-idempotent F)
       ( H)
   pr2 (is-quasicoherently-idempotent-htpy H) =
-    coherence-is-quasicoherently-idempotent-htpy H
+    quasicoherence-is-idempotent-htpy H
 
   is-quasicoherently-idempotent-inv-htpy :
     f ~ g → is-quasicoherently-idempotent g
@@ -326,7 +365,7 @@ module _
       ( is-idempotent-is-quasicoherently-idempotent F)
       ( inv-htpy H)
   pr2 (is-quasicoherently-idempotent-inv-htpy H) =
-    coherence-is-quasicoherently-idempotent-htpy (inv-htpy H)
+    quasicoherence-is-idempotent-htpy (inv-htpy H)
 ```
 
 ### Realigning the coherence of a quasicoherent idempotence proof
@@ -341,18 +380,18 @@ module _
   (I : f ∘ f ~ f)
   where
 
-  coherence-is-quasicoherently-idempotent-is-idempotent-htpy :
+  quasicoherence-is-idempotent-is-idempotent-htpy :
     is-idempotent-is-quasicoherently-idempotent F ~ I →
-    coherence-is-quasicoherently-idempotent f I
-  coherence-is-quasicoherently-idempotent-is-idempotent-htpy α =
+    quasicoherence-is-idempotent f I
+  quasicoherence-is-idempotent-is-idempotent-htpy α =
     ( left-whisker-comp² f (inv-htpy α)) ∙h
     ( coh-is-quasicoherently-idempotent F) ∙h
     ( right-whisker-comp² α f)
 
-  coherence-is-quasicoherently-idempotent-is-idempotent-inv-htpy :
+  quasicoherence-is-idempotent-is-idempotent-inv-htpy :
     I ~ is-idempotent-is-quasicoherently-idempotent F →
-    coherence-is-quasicoherently-idempotent f I
-  coherence-is-quasicoherently-idempotent-is-idempotent-inv-htpy α =
+    quasicoherence-is-idempotent f I
+  quasicoherence-is-idempotent-is-idempotent-inv-htpy α =
     ( left-whisker-comp² f α) ∙h
     ( coh-is-quasicoherently-idempotent F) ∙h
     ( right-whisker-comp² (inv-htpy α) f)
@@ -361,13 +400,13 @@ module _
     is-idempotent-is-quasicoherently-idempotent F ~ I →
     is-quasicoherently-idempotent f
   is-quasicoherently-idempotent-is-idempotent-htpy α =
-    ( I , coherence-is-quasicoherently-idempotent-is-idempotent-htpy α)
+    ( I , quasicoherence-is-idempotent-is-idempotent-htpy α)
 
   is-quasicoherently-idempotent-is-idempotent-inv-htpy :
     I ~ is-idempotent-is-quasicoherently-idempotent F →
     is-quasicoherently-idempotent f
   is-quasicoherently-idempotent-is-idempotent-inv-htpy α =
-    ( I , coherence-is-quasicoherently-idempotent-is-idempotent-inv-htpy α)
+    ( I , quasicoherence-is-idempotent-is-idempotent-inv-htpy α)
 ```
 
 ### Not every idempotent map is quasicoherently idempotent

src/foundation/split-idempotent-maps.lagda.md

@@ -525,11 +525,11 @@ module _
   where
 
   abstract
-    coherence-is-quasicoherently-idempotent-is-split-idempotent :
-      coherence-is-quasicoherently-idempotent f
+    quasicoherence-is-idempotent-is-split-idempotent :
+      quasicoherence-is-idempotent f
         ( is-idempotent-is-split-idempotent H)
-    coherence-is-quasicoherently-idempotent-is-split-idempotent =
-      coherence-is-quasicoherently-idempotent-is-idempotent-htpy
+    quasicoherence-is-idempotent-is-split-idempotent =
+      quasicoherence-is-idempotent-is-idempotent-htpy
         ( is-quasicoherently-idempotent-inv-htpy
           ( is-quasicoherently-idempotent-inclusion-retraction
             ( inclusion-is-split-idempotent H)
@@ -543,7 +543,7 @@ module _
     is-quasicoherently-idempotent f
   is-quasicoherently-idempotent-is-split-idempotent =
     ( is-idempotent-is-split-idempotent H ,
-      coherence-is-quasicoherently-idempotent-is-split-idempotent)
+      quasicoherence-is-idempotent-is-split-idempotent)
 
 module _
   {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A)

src/synthetic-homotopy-theory.lagda.md

@@ -79,6 +79,7 @@ open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types publ
 open import synthetic-homotopy-theory.join-powers-of-types public
 open import synthetic-homotopy-theory.joins-of-maps public
 open import synthetic-homotopy-theory.joins-of-types public
+open import synthetic-homotopy-theory.loop-homotopy-circle public
 open import synthetic-homotopy-theory.loop-spaces public
 open import synthetic-homotopy-theory.maps-of-prespectra public
 open import synthetic-homotopy-theory.mere-spheres public