Add flip′ to Function.Base (#1812)

Author: XiaohuWang0921

CHANGELOG.md

@@ -1949,6 +1949,12 @@ Other minor changes
   from-Σ     : (I : Set i) (C : I → Container s p) → ⟦ Σ I C ⟧ A → ∃ λ i → ⟦ C i ⟧ A
   ```
 
+* Added a non-dependent version of `Function.Base.flip` due to an issue noted in
+  Pull Request #1812:
+  ```agda
+  flip′ : (A → B → C) → (B → A → C)
+  ```
+
 NonZero/Positive/Negative changes
 ---------------------------------
 

src/Function/Base.agda

@@ -137,6 +137,11 @@ f ∘′ g = _∘_ f g
 _∘₂′_ : (C → D) → (A → B → C) → (A → B → D)
 f ∘₂′ g = _∘₂_ f g
 
+-- Flipping order of arguments
+
+flip′ : (A → B → C) → (B → A → C)
+flip′ = flip
+
 -- Application
 
 _$′_ : (A → B) → (A → B)