Define strictify function at each base type, plus evident property

CHANGELOG.md

@@ -48,6 +48,26 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* New operation in `Data.Bool.Base`:
+  ```agda
+  strictify : Bool → Bool
+  ```
+
+* New lemma in `Data.Bool.Properties`:
+  ```agda
+  strictify≗id : strictify b ≡ b
+  ```
+
+* New operation in `Data.Fin.Base`:
+  ```agda
+  strictify : Fin n → Fin n
+  ```
+
+* New lemma in `Data.Fin.Properties`:
+  ```agda
+  strictify≗id : strictify i ≡ i
+  ```
+
 * In `Data.List.Relation.Unary.All`:
   ```agda
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
@@ -65,10 +85,17 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* New operation in `Data.Nat.Base`:
+  ```agda
+  strictify : ℕ → ℕ
+  ```
+
 * New lemmas in `Data.Nat.Properties`: adjunction between `suc` and `pred`
   ```agda
   suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
   m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
+
+  strictify≗id : strictify n ≡ n
   ```
 
 * New lemma in `Data.Vec.Properties`:

src/Data/Bool/Base.agda

@@ -73,3 +73,7 @@ infix 0 if_then_else_
 if_then_else_ : Bool → A → A → A
 if true  then t else f = t
 if false then t else f = f
+
+strictify : Bool → Bool
+strictify b = if b then true else false
+

src/Data/Bool/Properties.agda

@@ -225,6 +225,13 @@ true  <? _     = no  (λ())
   { isStrictTotalOrder = <-isStrictTotalOrder
   }
 
+------------------------------------------------------------------------
+-- Properties of strictify
+
+strictify≗id : ∀ b → strictify b ≡ b
+strictify≗id true  = refl
+strictify≗id false = refl
+
 ------------------------------------------------------------------------
 -- Properties of _∨_
 

src/Data/Fin/Base.agda

@@ -269,6 +269,13 @@ pinch {suc n} _       zero    = zero
 pinch {suc n} zero    (suc j) = j
 pinch {suc n} (suc i) (suc j) = suc (pinch i j)
 
+------------------------------------------------------------------------
+-- Other operations
+
+strictify : Fin n → Fin n
+strictify zero    = zero
+strictify (suc i) = suc (strictify i)
+
 ------------------------------------------------------------------------
 -- Order relations
 

src/Data/Fin/Properties.agda

@@ -279,6 +279,14 @@ cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ zero = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (suc k) =
   cong suc (cast-trans (ℕ.suc-injective eq₁) (ℕ.suc-injective eq₂) k)
 
+------------------------------------------------------------------------
+-- Properties of strictify
+------------------------------------------------------------------------
+
+strictify≗id : (i : Fin n) → strictify i ≡ i
+strictify≗id zero    = refl
+strictify≗id (suc i) = cong suc (strictify≗id i)
+
 ------------------------------------------------------------------------
 -- Properties of _≤_
 ------------------------------------------------------------------------

src/Data/Nat/Base.agda

@@ -329,6 +329,13 @@ _! : ℕ → ℕ
 zero  ! = 1
 suc n ! = suc n * n !
 
+------------------------------------------------------------------------
+-- Other operations
+
+strictify : ℕ → ℕ
+strictify zero    = zero
+strictify (suc n) = suc (strictify n)
+
 ------------------------------------------------------------------------
 -- Extensionally equivalent alternative definitions of _≤_/_<_ etc.
 

src/Data/Nat/Properties.agda

@@ -523,6 +523,14 @@ module ≤-Reasoning where
 
 open ≤-Reasoning
 
+------------------------------------------------------------------------
+-- Properties of strictify
+------------------------------------------------------------------------
+
+strictify≗id : ∀ n → strictify n ≡ n
+strictify≗id zero    = refl
+strictify≗id (suc n) = cong suc (strictify≗id n)
+
 ------------------------------------------------------------------------
 -- Properties of _+_
 ------------------------------------------------------------------------