Add it utility function (#1104)

Author: jespercockx

CHANGELOG.md

@@ -914,6 +914,11 @@ Other minor additions
   _<+>_ : String → String → String -- space-introducing append
   ```
 
+* Added utility function to `Function.Base`:
+  ```agda
+  it : {A : Set a} → {{A}} → A
+  ```
+
 Version 2.6.1 changes
 =====================
 

src/Function/Base.agda

@@ -175,3 +175,8 @@ A ∋ x = x
 
 typeOf : {A : Set a} → A → Set a
 typeOf {A = A} _ = A
+
+-- Construct an element of the given type by instance search.
+
+it : {A : Set a} → {{A}} → A
+it {{x}} = x