Add variant of first? to Data.List.Relation.Unary.First.Properties (#1475)

Author: damhiya

CHANGELOG.md

@@ -448,6 +448,11 @@ Other minor additions
   all-upTo           : All (_< n) (upTo n)
   ```
 
+* Added new proof in `Data.List.Relation.Unary.First.Properties`:
+  ```agda
+  cofirst? : Decidable P → Decidable (First (∁ P) P)
+  ```
+
 * Added new operations in `Data.List.Relation.Unary.Linked`:
   ```agda
   head′ : Linked R (x ∷ xs) → Connected R (just x) (head xs)

src/Data/List/Relation/Unary/First/Properties.agda

@@ -85,6 +85,11 @@ module _ {a p} {A : Set a} {P : Pred A p} where
                $ Sum.map₂ (All⇒¬First contradiction)
                $ first (Sum.fromDec ∘ P?) xs
 
+  cofirst? : Decidable P → Decidable (First (∁ P) P)
+  cofirst? P? xs = Sum.toDec
+                 $ Sum.map₂ (All⇒¬First id)
+                 $ first (Sum.swap ∘ Sum.fromDec ∘ P?) xs
+
 ------------------------------------------------------------------------
 -- Conversion to Any