rename ≐? to map

Author: mildsunrise

CHANGELOG.md

@@ -834,7 +834,7 @@ Additions to existing modules
 
 * Added new proofs in `Relation.Nullary.Properties`:
   ```agda
-  ≐?     : P ≐ Q → Decidable P → Decidable Q
+  map    : P ≐ Q → Decidable P → Decidable Q
   does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
   does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
   ```

src/Relation/Unary/Properties.agda

@@ -200,9 +200,9 @@ U-Universal = λ _ → _
 ------------------------------------------------------------------------
 -- Decidability properties
 
-≐? : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
-     P ≐ Q → Decidable P → Decidable Q
-≐? (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)
+map : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+      P ≐ Q → Decidable P → Decidable Q
+map (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)
 
 ∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
 ∁? P? x = ¬? (P? x)
@@ -244,7 +244,7 @@ does-≡ P? P?′ x = Dec.does-≡ (P? x) (P?′ x)
 does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
          (P? : Decidable P) → (Q? : Decidable Q) →
          does ∘ P? ≗ does ∘ Q?
-does-≐ P≐Q P? = does-≡ (≐? P≐Q P?)
+does-≐ P≐Q P? = does-≡ (map P≐Q P?)
 
 ------------------------------------------------------------------------
 -- Irrelevant properties