Use point x instead of const unit X x (#994)

Also adds the fact `is-injective-point`, and fixes misnamings in
`foundation.constant-maps`.

src/foundation/booleans.lagda.md

@@ -124,9 +124,11 @@ eq-Eq-bool :
 eq-Eq-bool {true} {true} star = refl
 eq-Eq-bool {false} {false} star = refl
 
-neq-false-true-bool :
-  false ≠ true
+neq-false-true-bool : false ≠ true
 neq-false-true-bool ()
+
+neq-true-false-bool : true ≠ false
+neq-true-false-bool ()
 ```
 
 ## Structure
@@ -195,12 +197,12 @@ Fin-two-ℕ-bool true = inl (inr star)
 Fin-two-ℕ-bool false = inr star
 
 abstract
-  is-retraction-Fin-two-ℕ-bool : (Fin-two-ℕ-bool ∘ bool-Fin-two-ℕ) ~ id
+  is-retraction-Fin-two-ℕ-bool : Fin-two-ℕ-bool ∘ bool-Fin-two-ℕ ~ id
   is-retraction-Fin-two-ℕ-bool (inl (inr star)) = refl
   is-retraction-Fin-two-ℕ-bool (inr star) = refl
 
 abstract
-  is-section-Fin-two-ℕ-bool : (bool-Fin-two-ℕ ∘ Fin-two-ℕ-bool) ~ id
+  is-section-Fin-two-ℕ-bool : bool-Fin-two-ℕ ∘ Fin-two-ℕ-bool ~ id
   is-section-Fin-two-ℕ-bool true = refl
   is-section-Fin-two-ℕ-bool false = refl
 
@@ -261,20 +263,6 @@ pr2 equiv-neg-bool = is-equiv-neg-bool
 abstract
   not-equiv-const :
     (b : bool) → ¬ (is-equiv (const bool bool b))
-  not-equiv-const true (pair (pair g G) (pair h H)) =
-    neq-false-true-bool (inv (G false))
-  not-equiv-const false (pair (pair g G) (pair h H)) =
-    neq-false-true-bool (G true)
-```
-
-### The constant function `const bool bool b` is injective
-
-```agda
-abstract
-  is-injective-const-true : is-injective (const unit bool true)
-  is-injective-const-true {star} {star} p = refl
-
-abstract
-  is-injective-const-false : is-injective (const unit bool false)
-  is-injective-const-false {star} {star} p = refl
+  not-equiv-const true ((g , G) , _) = neq-true-false-bool (G false)
+  not-equiv-const false ((g , G) , _) = neq-false-true-bool (G true)
 ```

src/foundation/constant-maps.lagda.md

@@ -55,115 +55,115 @@ module _
   compute-action-htpy-function-const c H = ap-const c (eq-htpy H)
 ```
 
-### A type is `k+1`-truncated if and only if all constant maps into it are `k`-truncated
+### A type is `k+1`-truncated if and only if all point inclusions are `k`-truncated maps
 
 ```agda
 module _
   {l : Level} {A : UU l}
   where
 
-  fiber-const : (x y : A) → fiber (const unit A x) y ≃ (x ＝ y)
-  fiber-const x y = left-unit-law-prod
+  compute-fiber-point : (x y : A) → fiber (point x) y ≃ (x ＝ y)
+  compute-fiber-point x y = left-unit-law-prod
 
   abstract
-    is-trunc-map-const-is-trunc :
+    is-trunc-map-point-is-trunc :
       (k : 𝕋) → is-trunc (succ-𝕋 k) A →
-      (x : A) → is-trunc-map k (const unit A x)
-    is-trunc-map-const-is-trunc k is-trunc-A x y =
+      (x : A) → is-trunc-map k (point x)
+    is-trunc-map-point-is-trunc k is-trunc-A x y =
       is-trunc-equiv k
         ( x ＝ y)
-        ( fiber-const x y)
+        ( compute-fiber-point x y)
         ( is-trunc-A x y)
 
   abstract
-    is-trunc-is-trunc-map-const :
-      (k : 𝕋) → ((x : A) → is-trunc-map k (const unit A x)) →
+    is-trunc-is-trunc-map-point :
+      (k : 𝕋) → ((x : A) → is-trunc-map k (point x)) →
       is-trunc (succ-𝕋 k) A
-    is-trunc-is-trunc-map-const k is-trunc-const x y =
+    is-trunc-is-trunc-map-point k is-trunc-point x y =
       is-trunc-equiv' k
         ( Σ unit (λ _ → x ＝ y))
         ( left-unit-law-Σ (λ _ → x ＝ y))
-        ( is-trunc-const x y)
+        ( is-trunc-point x y)
 
   abstract
-    is-contr-map-const-is-prop :
-      is-prop A → (x : A) → is-contr-map (const unit A x)
-    is-contr-map-const-is-prop = is-trunc-map-const-is-trunc neg-two-𝕋
+    is-contr-map-point-is-prop :
+      is-prop A → (x : A) → is-contr-map (point x)
+    is-contr-map-point-is-prop = is-trunc-map-point-is-trunc neg-two-𝕋
 
   abstract
-    is-equiv-const-is-prop :
-      is-prop A → (x : A) → is-equiv (const unit A x)
-    is-equiv-const-is-prop H x =
-      is-equiv-is-contr-map (is-contr-map-const-is-prop H x)
+    is-equiv-point-is-prop :
+      is-prop A → (x : A) → is-equiv (point x)
+    is-equiv-point-is-prop H x =
+      is-equiv-is-contr-map (is-contr-map-point-is-prop H x)
 
   abstract
-    is-prop-map-const-is-set :
-      is-set A → (x : A) → is-prop-map (const unit A x)
-    is-prop-map-const-is-set = is-trunc-map-const-is-trunc neg-one-𝕋
+    is-prop-map-point-is-set :
+      is-set A → (x : A) → is-prop-map (point x)
+    is-prop-map-point-is-set = is-trunc-map-point-is-trunc neg-one-𝕋
 
   abstract
-    is-emb-const-is-set : is-set A → (x : A) → is-emb (const unit A x)
-    is-emb-const-is-set H x = is-emb-is-prop-map (is-prop-map-const-is-set H x)
+    is-emb-point-is-set : is-set A → (x : A) → is-emb (point x)
+    is-emb-point-is-set H x = is-emb-is-prop-map (is-prop-map-point-is-set H x)
 
   abstract
-    is-0-map-const-is-1-type : is-1-type A → (x : A) → is-0-map (const unit A x)
-    is-0-map-const-is-1-type = is-trunc-map-const-is-trunc zero-𝕋
+    is-0-map-point-is-1-type : is-1-type A → (x : A) → is-0-map (point x)
+    is-0-map-point-is-1-type = is-trunc-map-point-is-trunc zero-𝕋
 
   abstract
-    is-faithful-const-is-1-type :
-      is-1-type A → (x : A) → is-faithful (const unit A x)
-    is-faithful-const-is-1-type H x =
-      is-faithful-is-0-map (is-0-map-const-is-1-type H x)
+    is-faithful-point-is-1-type :
+      is-1-type A → (x : A) → is-faithful (point x)
+    is-faithful-point-is-1-type H x =
+      is-faithful-is-0-map (is-0-map-point-is-1-type H x)
 
   abstract
-    is-prop-is-contr-map-const :
-      ((x : A) → is-contr-map (const unit A x)) → is-prop A
-    is-prop-is-contr-map-const = is-trunc-is-trunc-map-const neg-two-𝕋
+    is-prop-is-contr-map-point :
+      ((x : A) → is-contr-map (point x)) → is-prop A
+    is-prop-is-contr-map-point = is-trunc-is-trunc-map-point neg-two-𝕋
 
   abstract
-    is-prop-is-equiv-const :
-      ((x : A) → is-equiv (const unit A x)) → is-prop A
-    is-prop-is-equiv-const H =
-      is-prop-is-contr-map-const (is-contr-map-is-equiv ∘ H)
+    is-prop-is-equiv-point :
+      ((x : A) → is-equiv (point x)) → is-prop A
+    is-prop-is-equiv-point H =
+      is-prop-is-contr-map-point (is-contr-map-is-equiv ∘ H)
 
   abstract
-    is-set-is-prop-map-const :
-      ((x : A) → is-prop-map (const unit A x)) → is-set A
-    is-set-is-prop-map-const = is-trunc-is-trunc-map-const neg-one-𝕋
+    is-set-is-prop-map-point :
+      ((x : A) → is-prop-map (point x)) → is-set A
+    is-set-is-prop-map-point = is-trunc-is-trunc-map-point neg-one-𝕋
 
   abstract
-    is-set-is-emb-const :
-      ((x : A) → is-emb (const unit A x)) → is-set A
-    is-set-is-emb-const H =
-      is-set-is-prop-map-const (is-prop-map-is-emb ∘ H)
+    is-set-is-emb-point :
+      ((x : A) → is-emb (point x)) → is-set A
+    is-set-is-emb-point H =
+      is-set-is-prop-map-point (is-prop-map-is-emb ∘ H)
 
   abstract
-    is-1-type-is-0-map-const :
-      ((x : A) → is-0-map (const unit A x)) → is-1-type A
-    is-1-type-is-0-map-const = is-trunc-is-trunc-map-const zero-𝕋
+    is-1-type-is-0-map-point :
+      ((x : A) → is-0-map (point x)) → is-1-type A
+    is-1-type-is-0-map-point = is-trunc-is-trunc-map-point zero-𝕋
 
   abstract
-    is-1-type-is-faithful-const :
-      ((x : A) → is-faithful (const unit A x)) → is-1-type A
-    is-1-type-is-faithful-const H =
-      is-1-type-is-0-map-const (is-0-map-is-faithful ∘ H)
+    is-1-type-is-faithful-point :
+      ((x : A) → is-faithful (point x)) → is-1-type A
+    is-1-type-is-faithful-point H =
+      is-1-type-is-0-map-point (is-0-map-is-faithful ∘ H)
 
-const-equiv :
+point-equiv :
   {l : Level} (A : Prop l) (x : type-Prop A) → unit ≃ type-Prop A
-pr1 (const-equiv A x) = const unit (type-Prop A) x
-pr2 (const-equiv A x) = is-equiv-const-is-prop (is-prop-type-Prop A) x
+pr1 (point-equiv A x) = point x
+pr2 (point-equiv A x) = is-equiv-point-is-prop (is-prop-type-Prop A) x
 
-const-emb :
+point-emb :
   {l : Level} (A : Set l) (x : type-Set A) → unit ↪ type-Set A
-pr1 (const-emb A x) = const unit (type-Set A) x
-pr2 (const-emb A x) = is-emb-const-is-set (is-set-type-Set A) x
+pr1 (point-emb A x) = point x
+pr2 (point-emb A x) = is-emb-point-is-set (is-set-type-Set A) x
 
-const-faithful-map :
+point-faithful-map :
   {l : Level} (A : 1-Type l) (x : type-1-Type A) →
   faithful-map unit (type-1-Type A)
-pr1 (const-faithful-map A x) = const unit (type-1-Type A) x
-pr2 (const-faithful-map A x) =
-  is-faithful-const-is-1-type (is-1-type-type-1-Type A) x
+pr1 (point-faithful-map A x) = point x
+pr2 (point-faithful-map A x) =
+  is-faithful-point-is-1-type (is-1-type-type-1-Type A) x
 ```
 
 ### Given a term of `A`, the constant map is injective viewed as a function `B → (A → B)`
@@ -184,12 +184,12 @@ pr2 (const-injection A B a) = is-injective-const A B a
 ```agda
 htpy-diagonal-Id-ap-diagonal-htpy-eq :
   {l1 l2 : Level} (A : UU l1) {B : UU l2} (x y : B) →
-  htpy-eq ∘ ap (const A B) {x} {y} ~ const A (x ＝ y)
+  htpy-eq ∘ ap (const A B) ~ const A (x ＝ y)
 htpy-diagonal-Id-ap-diagonal-htpy-eq A x y refl = refl
 
 htpy-ap-diagonal-htpy-eq-diagonal-Id :
   {l1 l2 : Level} (A : UU l1) {B : UU l2} (x y : B) →
-  const A (x ＝ y) ~ htpy-eq ∘ ap (const A B) {x} {y}
+  const A (x ＝ y) ~ htpy-eq ∘ ap (const A B)
 htpy-ap-diagonal-htpy-eq-diagonal-Id A x y =
   inv-htpy (htpy-diagonal-Id-ap-diagonal-htpy-eq A x y)
 ```

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

@@ -39,26 +39,26 @@ module _
   where
 
   square-fiber :
-    f ∘ pr1 ~ const unit B b ∘ const (fiber f b) unit star
+    f ∘ pr1 ~ point b ∘ terminal-map (fiber f b)
   square-fiber = pr2
 
-  cone-fiber : cone f (const unit B b) (fiber f b)
+  cone-fiber : cone f (point b) (fiber f b)
   pr1 cone-fiber = pr1
-  pr1 (pr2 cone-fiber) = const (fiber f b) unit star
+  pr1 (pr2 cone-fiber) = terminal-map (fiber f b)
   pr2 (pr2 cone-fiber) = square-fiber
 
   abstract
-    is-pullback-cone-fiber : is-pullback f (const unit B b) cone-fiber
+    is-pullback-cone-fiber : is-pullback f (point b) cone-fiber
     is-pullback-cone-fiber =
       is-equiv-tot-is-fiberwise-equiv
         ( λ a → is-equiv-map-inv-left-unit-law-prod)
 
   abstract
     universal-property-pullback-cone-fiber :
-      universal-property-pullback f (const unit B b) cone-fiber
+      universal-property-pullback f (point b) cone-fiber
     universal-property-pullback-cone-fiber =
       universal-property-pullback-is-pullback f
-        ( const unit B b)
+        ( point b)
         ( cone-fiber)
         ( is-pullback-cone-fiber)
 ```

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

@@ -191,15 +191,15 @@ is-trunc-map-is-trunc-map-map-Π' :
   (i : I) → is-trunc-map k (f i)
 is-trunc-map-is-trunc-map-map-Π' k {A = A} {B} f H i b =
   is-trunc-equiv' k
-    ( fiber (map-Π (λ (x : unit) → f i)) (const unit (B i) b))
+    ( fiber (map-Π (λ _ → f i)) (point b))
     ( equiv-Σ
       ( λ a → f i a ＝ b)
       ( equiv-universal-property-unit (A i))
       ( λ h → equiv-ap
         ( equiv-universal-property-unit (B i))
-        ( map-Π (λ x → f i) h)
-        ( const unit (B i) b)))
-    ( H (λ x → i) (const unit (B i) b))
+        ( map-Π (λ _ → f i) h)
+        ( point b)))
+    ( H (λ _ → i) (point b))
 
 is-emb-map-Π-is-emb' :
   {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3} →

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

@@ -76,15 +76,15 @@ module _
   is-trunc-map-postcomp-is-trunc-map is-trunc-f A =
     is-trunc-map-map-Π-is-trunc-map' k
       ( terminal-map A)
-      ( const unit (X → Y) f)
-      ( const unit (is-trunc-map k f) is-trunc-f)
+      ( point f)
+      ( point is-trunc-f)
 
   is-trunc-map-is-trunc-map-postcomp :
     ({l3 : Level} (A : UU l3) → is-trunc-map k (postcomp A f)) →
     is-trunc-map k f
   is-trunc-map-is-trunc-map-postcomp is-trunc-postcomp-f =
     is-trunc-map-is-trunc-map-map-Π' k
-      ( const unit (X → Y) f)
+      ( point f)
       ( λ {l} {J} α → is-trunc-postcomp-f {l} J)
       ( star)
 

src/foundation/isolated-elements.lagda.md

@@ -92,12 +92,12 @@ module _
   is-decidable-point-is-isolated :
     is-isolated a → is-decidable-map (point a)
   is-decidable-point-is-isolated d x =
-    is-decidable-equiv (fiber-const a x) (d x)
+    is-decidable-equiv (compute-fiber-point a x) (d x)
 
   is-isolated-is-decidable-point :
     is-decidable-map (point a) → is-isolated a
   is-isolated-is-decidable-point d x =
-    is-decidable-equiv' (fiber-const a x) (d x)
+    is-decidable-equiv' (compute-fiber-point a x) (d x)
 
   cases-Eq-isolated-element :
     is-isolated a → (x : A) → is-decidable (a ＝ x) → UU lzero
@@ -253,7 +253,7 @@ module _
   is-emb-point-isolated-element =
     is-emb-comp
       ( inclusion-isolated-element A)
-      ( const unit (isolated-element A) a)
+      ( point a)
       ( is-emb-inclusion-isolated-element A)
       ( is-emb-is-injective
         ( is-set-isolated-element A)