code review

martinescardo · Oct 8, 2024 · 932532d · 932532d
1 parent fcf3d45
commit 932532d
Show file tree

Hide file tree

Showing 9 changed files with 146 additions and 88 deletions.
diff --git a/source/Modal/Homotopy.lagda b/source/Modal/Homotopy.lagda
@@ -62,7 +62,7 @@ homotopy-precomp-by-embedding-is-equiv fe0 fe1 fe2 fe3 f g i precomp-i-is-emb =
     aux : (h : f ∼ g) → ap (_∘ i) (inverse _ (fe0 f g) h) ＝ dfunext fe1 (h ∘ i)
     aux h =
      ap (_∘ i) (inverse (happly' f g) (fe0 f g) h)
-      ＝⟨ ap (λ - → ap (_∘ i) (- h)) (inverse-happly-is-dfunext fe0 fe3 f g) ⟩
+      ＝⟨ ap (λ - → ap (_∘ i) (- h)) (inverse-of-happly-is-dfunext fe0 fe3 f g) ⟩
      ap (_∘ i) (dfunext fe0 h)
       ＝⟨ ap-precomp-funext _ _ i h fe0 fe1 ⟩
      dfunext fe1 (h ∘ i) ∎

diff --git a/source/Taboos/LPO.lagda b/source/Taboos/LPO.lagda
@@ -210,7 +210,7 @@ open import UF.DiscreteAndSeparated
 [LPO→ℕ]-discrete-gives-¬LPO-decidable fe =
   discrete-exponential-has-decidable-emptiness-of-exponent
    fe
-   (1 , 0 , positive-not-zero 0)
+   ((1 , 0) , positive-not-zero 0)
 
 \end{code}
 

diff --git a/source/UF/DiscreteAndSeparated.lagda b/source/UF/DiscreteAndSeparated.lagda
@@ -1,8 +1,5 @@
 Martin Escardo 2011.
 
-(Totally separated types moved to the module TotallySeparated January
-2018, and extended.)
-
 \begin{code}
 
 {-# OPTIONS --safe --without-K #-}
@@ -32,6 +29,15 @@ open import UF.Subsingletons-FunExt
 is-isolated : {X : 𝓤 ̇ } → X → 𝓤 ̇
 is-isolated x = ∀ y → is-decidable (x ＝ y)
 
+\end{code}
+
+Notice that there is a different notion of being homotopy isolated
+(abbreviated is-h-isolated) in the module UF.Sets.
+
+A type is perfect if it has no isolated points.
+
+\begin{code}
+
 is-perfect : 𝓤 ̇ → 𝓤 ̇
 is-perfect X = is-empty (Σ x ꞉ X , is-isolated x)
 
@@ -45,10 +51,14 @@ is-decidable-eq-sym x y = cases
                            (λ (p : x ＝ y) → inl (p ⁻¹))
                            (λ (n : ¬ (x ＝ y)) → inr (λ (q : y ＝ x) → n (q ⁻¹)))
 
-is-isolated'-gives-is-isolated : {X : 𝓤 ̇ } (x : X) → is-isolated' x → is-isolated x
+is-isolated'-gives-is-isolated : {X : 𝓤 ̇ } (x : X)
+                               → is-isolated' x
+                               → is-isolated x
 is-isolated'-gives-is-isolated x i' y = is-decidable-eq-sym y x (i' y)
 
-is-isolated-gives-is-isolated' : {X : 𝓤 ̇ } (x : X) → is-isolated x → is-isolated' x
+is-isolated-gives-is-isolated' : {X : 𝓤 ̇ } (x : X)
+                               → is-isolated x
+                               → is-isolated' x
 is-isolated-gives-is-isolated' x i y = is-decidable-eq-sym x y (i y)
 
 is-discrete : 𝓤 ̇ → 𝓤 ̇
@@ -119,8 +129,8 @@ inr-is-isolated {𝓤} {𝓥} {X} {Y} y i = γ
 \end{code}
 
 The closure of discrete types under Σ is proved in the module
-UF.Miscelanea (as this requires to first prove that discrete types
-are sets).
+TypeTopology.SigmaDiscreteAndTotallySeparated (as this requires to
+first prove that discrete types are sets).
 
 General properties:
 
@@ -149,7 +159,9 @@ discrete-types-are-cotransitive' d {x} {y} {z} φ = f (d x z)
   f (inr γ) = inl γ
 
 retract-is-discrete : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
-                    → retract Y of X → is-discrete X → is-discrete Y
+                    → retract Y of X
+                    → is-discrete X
+                    → is-discrete Y
 retract-is-discrete (f , (s , φ)) d y y' = g (d (s y) (s y'))
  where
   g : is-decidable (s y ＝ s y') → is-decidable (y ＝ y')
@@ -167,11 +179,14 @@ retract-is-discrete (f , (s , φ)) d y y' = g (d (s y) (s y'))
  where
   r : X → 𝟚
   r = pr₁ (characteristic-function d)
+
   φ : (x : X) → (r x ＝ ₀ → x₀ ＝ x) × (r x ＝ ₁ → ¬ (x₀ ＝ x))
   φ = pr₂ (characteristic-function d)
+
   s : 𝟚 → X
   s ₀ = x₀
   s ₁ = x₁
+
   rs : (n : 𝟚) → r (s n) ＝ n
   rs ₀ = different-from-₁-equal-₀ (λ p → pr₂ (φ x₀) p refl)
   rs ₁ = different-from-₀-equal-₁ λ p → 𝟘-elim (ne (pr₁ (φ x₁) p))
@@ -307,8 +322,10 @@ binary-product-is-¬¬-separated s t (x , y) (x' , y') φ =
  where
   lemma₀ : ¬¬ ((x , y) ＝ (x' , y')) → x ＝ x'
   lemma₀ = (s x x') ∘ ¬¬-functor (ap pr₁)
+
   lemma₁ : ¬¬ ((x , y) ＝ (x' , y')) → y ＝ y'
   lemma₁ = (t y y') ∘ ¬¬-functor (ap pr₂)
+
   lemma : x ＝ x' → y ＝ y' → (x , y) ＝ (x' , y')
   lemma = ap₂ (_,_)
 
@@ -448,20 +465,26 @@ equality-of-¬¬stable-propositions fe pe p q f g a = γ
 
 \end{code}
 
-21 March 2018
+21 March 2018.
 
 \begin{code}
 
-qinvs-preserve-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → qinv f
-                            → (x : X) → is-isolated x → is-isolated (f x)
+qinvs-preserve-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
+                            → qinv f
+                            → (x : X)
+                            → is-isolated x
+                            → is-isolated (f x)
 qinvs-preserve-isolatedness {𝓤} {𝓥} {X} {Y} f (g , ε , η) x i y = h (i (g y))
  where
   h : is-decidable (x ＝ g y) → is-decidable (f x ＝ y)
   h (inl p) = inl (ap f p ∙ η y)
   h (inr u) = inr (contrapositive (λ (q : f x ＝ y) → (ε x)⁻¹ ∙ ap g q) u)
 
-equivs-preserve-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-equiv f
-                             → (x : X) → is-isolated x → is-isolated (f x)
+equivs-preserve-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
+                             → is-equiv f
+                             → (x : X)
+                             → is-isolated x
+                             → is-isolated (f x)
 equivs-preserve-isolatedness f e = qinvs-preserve-isolatedness f (equivs-are-qinvs f e)
 
 new-point-is-isolated : {X : 𝓤 ̇ } → is-isolated {𝓤 ⊔ 𝓥} {X + 𝟙 {𝓥}} (inr ⋆)
@@ -542,7 +565,8 @@ being-isolated-is-prop {𝓤} fe x = prop-criterion γ
   γ : is-isolated x → is-prop (is-isolated x)
   γ i = Π-is-prop (fe 𝓤 𝓤)
          (λ x → sum-of-contradictory-props
-                 (local-hedberg _ (λ y → decidable-types-are-collapsible (i y)) x)
+                 (local-hedberg _
+                   (λ y → decidable-types-are-collapsible (i y)) x)
                  (negations-are-props (fe 𝓤 𝓤₀))
                  (λ p n → n p))
 
@@ -620,7 +644,8 @@ discrete-inr fe d x = isolated-inr fe x (d x)
 isolated-Id-is-prop : {X : 𝓤 ̇ } (x : X)
                     → is-isolated' x
                     → (y : X) → is-prop (y ＝ x)
-isolated-Id-is-prop x i = local-hedberg' x (λ y → decidable-types-are-collapsible (i y))
+isolated-Id-is-prop x i =
+ local-hedberg' x (λ y → decidable-types-are-collapsible (i y))
 
 lc-maps-reflect-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                              → left-cancellable f
@@ -685,19 +710,18 @@ equiv-to-discrete (f , e) = equivs-preserve-discreteness f e
 
 \end{code}
 
-
 Added 14th Feb 2020:
 
 \begin{code}
 
 discrete-exponential-has-decidable-emptiness-of-exponent
  : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
  → funext 𝓤 𝓥
- → (Σ y₀ ꞉ Y , Σ y₁ ꞉ Y , y₀ ≠ y₁)
+ → has-two-distinct-points Y
  → is-discrete (X → Y)
  → is-decidable (is-empty X)
 discrete-exponential-has-decidable-emptiness-of-exponent
-  {𝓤} {𝓥} {X} {Y} fe (y₀ , y₁ , ne) d = γ
+  {𝓤} {𝓥} {X} {Y} fe ((y₀ , y₁) , ne) d = γ
  where
   a : is-decidable ((λ _ → y₀) ＝ (λ _ → y₁))
   a = d (λ _ → y₀) (λ _ → y₁)
@@ -725,13 +749,11 @@ Added 19th Feb 2020:
 
 \begin{code}
 
-maps-of-props-into-h-isolated-points-are-embeddings :
-
-   {P : 𝓤 ̇ } {X : 𝓥 ̇ } (f : P → X)
+maps-of-props-into-h-isolated-points-are-embeddings
+ : {P : 𝓤 ̇ } {X : 𝓥 ̇ } (f : P → X)
  → is-prop P
  → ((p : P) → is-h-isolated (f p))
  → is-embedding f
-
 maps-of-props-into-h-isolated-points-are-embeddings f i j q (p , s) (p' , s') =
  to-Σ-＝ (i p p' , j p' _ s')
 

diff --git a/source/UF/Embeddings.lagda b/source/UF/Embeddings.lagda
@@ -7,7 +7,6 @@ Martin Escardo
 module UF.Embeddings where
 
 open import MLTT.Spartan
-
 open import MLTT.Plus-Properties
 open import UF.Base
 open import UF.Equiv
@@ -51,7 +50,10 @@ id-is-embedding = singleton-types'-are-props
   T z = Σ (y , _) ꞉ fiber g z , fiber f y
 
   T-is-prop : (z : Z) → is-prop (T z)
-  T-is-prop z = subtypes-of-props-are-props' pr₁ (pr₁-lc (λ {t} → e (pr₁ t))) (d z)
+  T-is-prop z = subtypes-of-props-are-props'
+                 pr₁
+                 (pr₁-lc (λ {t} → e (pr₁ t)))
+                 (d z)
 
   φ : (z : Z) → fiber (g ∘ f) z → T z
   φ z (x , p) = (f x , p) , x , refl
@@ -80,7 +82,6 @@ _∘↪_ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
      → X ↪ Z
 (g , j) ∘↪ (f , i) = g ∘ f , ∘-is-embedding i j
 
-
 ⌊_⌋ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ↪ Y → X → Y
 ⌊ f , _ ⌋     = f
 
@@ -160,7 +161,8 @@ equivs-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ≃ Y → X ↪ Y
 equivs-embedding e = ⌜ e ⌝ , equivs-are-embeddings ⌜ e ⌝ (⌜⌝-is-equiv e)
 
 embeddings-are-lc : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
-                  → is-embedding f → left-cancellable f
+                  → is-embedding f
+                  → left-cancellable f
 embeddings-are-lc f e {x} {x'} p = ap pr₁ (e (f x) (x , refl) (x' , (p ⁻¹)))
 
 subtypes-of-props-are-props : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (e : X → Y)
@@ -202,10 +204,9 @@ embedding-gives-embedding' {𝓤} {𝓥} {X} {Y} f ise = g
 
 \end{code}
 
-Added 27 June 2024.
-It follows that if f is an equivalence, then so is ap f.
-It is added here, rather than in UF.EquivalenceExamples, to avoid cyclic module
-dependencies.
+Added 27 June 2024.  It follows that if f is an equivalence, then so
+is ap f.  It is added here, rather than in UF.EquivalenceExamples, to
+avoid cyclic module dependencies.
 
 \begin{code}
 
@@ -226,7 +227,8 @@ embedding-criterion-converse : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                              → is-embedding f
                              → (x' x : X)
                              → (f x' ＝ f x) ≃ (x' ＝ x)
-embedding-criterion-converse f e x' x = ≃-sym (embedding-criterion-converse' f e x' x)
+embedding-criterion-converse f e x' x =
+ ≃-sym (embedding-criterion-converse' f e x' x)
 
 embedding'-gives-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                              (f : X → Y)
@@ -272,8 +274,11 @@ to-subtype-＝-≃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
                 → {x y : X} {a : A x} {b : A y}
                 → (x ＝ y) ≃ ((x , a) ＝ (y , b))
 to-subtype-＝-≃ A-is-prop-valued {x} {y} {a} {b} =
- embedding-criterion-converse pr₁ (pr₁-is-embedding A-is-prop-valued) (x , a) (y , b)
-
+ embedding-criterion-converse
+  pr₁
+  (pr₁-is-embedding A-is-prop-valued)
+  (x , a)
+  (y , b)
 
 pr₁-lc-bis : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
            → ({x : X} → is-prop (Y x))
@@ -318,7 +323,8 @@ lc-maps-into-sets-are-embeddings : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                                  → left-cancellable f
                                  → is-set Y
                                  → is-embedding f
-lc-maps-into-sets-are-embeddings {𝓤} {𝓥} {X} {Y} f f-lc iss y (x , p) (x' , p') = γ
+lc-maps-into-sets-are-embeddings
+ {𝓤} {𝓥} {X} {Y} f f-lc iss y (x , p) (x' , p') = γ
  where
    r : x ＝ x'
    r = f-lc (p ∙ (p' ⁻¹))
@@ -398,7 +404,10 @@ postcomp-is-embedding {𝓤} {𝓥} {𝓦} fe {X} {Y} {A} f i = γ
   γ : is-embedding (f ∘_)
   γ = embedding-criterion' (f ∘_) k
 
-disjoint-images : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } → (X → A) → (Y → A) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇
+disjoint-images : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ }
+                → (X → A)
+                → (Y → A)
+                → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇
 disjoint-images f g = ∀ x y → f x ≠ g y
 
 disjoint-cases-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ }
@@ -440,7 +449,8 @@ disjoint-cases-embedding {𝓤} {𝓥} {𝓦} {X} {Y} {A} f g ef eg d = γ
 
 TODO.
   (1) f : X → Y is an embedding iff fiber f (f x) is a singleton for every x : X.
-  (2) f : X → Y is an embedding iff its corestriction to its image is an equivalence.
+  (2) f : X → Y is an embedding iff its corestriction to its image is an
+      equivalence.
 
 This can be deduced directly from Yoneda.
 
@@ -588,7 +598,8 @@ Idtofun-is-embedding ua fe {X} {Y} =
   (dfunext fe (idtofun-agreement X Y))
   (idtofun-is-embedding ua)
 
-unique-from-𝟘-is-embedding : {X : 𝓤 ̇ } → is-embedding (unique-from-𝟘 {𝓤} {𝓥} {X})
+unique-from-𝟘-is-embedding : {X : 𝓤 ̇ }
+                           → is-embedding (unique-from-𝟘 {𝓤} {𝓥} {X})
 unique-from-𝟘-is-embedding x (y , p) = 𝟘-elim y
 
 \end{code}
@@ -642,5 +653,4 @@ infix  0 _↪_
 infix  1 _□
 infixr 0 _↪⟨_⟩_
 
-
 \end{code}