diff --git a/CHANGELOG.md b/CHANGELOG.md
index 70c3357348..d56c3d4af4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -121,6 +121,11 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Function.Base`:
+  ```agda
+  λ∙ : (.(x : A) → B x) → ((x : A) → B x)
+  ```
+
 * In `Relation.Binary.Construct.Intersection`:
   ```agda
   decidable     ↦   _∩?_
@@ -163,6 +168,11 @@ New modules
 
 * `Algebra.Properties.Semiring`.
 
+* A variation on `Fin` seen as a `Nat` refinement, with better runtime representation and performance.
+  ```
+  Data.Nat.Bounded.Base
+  ```
+
 * `Data.List.Fresh.Membership.DecSetoid`.
 
 * Various additions over non-empty lists:
@@ -278,6 +288,12 @@ Additions to existing modules
   ```
   NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`.
 
+
+* In `Data.Bool.Properties`:
+  ```agda
+  ¬T-≡ : (¬ T x) ⇔ x ≡ false
+  ```
+
 * In `Data.Fin.Permutation.Components`:
   ```agda
   transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
@@ -392,6 +408,7 @@ Additions to existing modules
   m⊔n∸[m∸n]≡n : ∀ m n → m ⊔ n ∸ (m ∸ n) ≡ n
   m⊔n≡m∸n+n : ∀ m n → m ⊔ n ≡ m ∸ n + n
   ∣m-n∣≡m⊔n∸m⊓n : ∀ m n → ∣ m - n ∣ ≡ m ⊔ n ∸ m ⊓ n
+  <″⇒< : _<″_ ⇒ _<_
   ```
 
 * In `Data.Product.Properties`:
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 53b4a1f4a7..1ad1b61767 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -41,7 +41,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning; setoid; decSetoid; isEquivalence)
 open import Relation.Nullary.Decidable.Core
   using (True; yes; no; fromWitness ; toWitness)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
@@ -835,6 +835,10 @@ if-cong₂ _ refl refl = refl
 
 open Relation.Nullary.Decidable.Core public using (T?)
 
+¬T-≡ : ∀ {x} → (¬ T x) ⇔ x ≡ false
+¬T-≡ {false} = mk⇔ (const refl) (const id)
+¬T-≡ {true}  = mk⇔ (contradiction _) (λ ())
+
 T-≡ : ∀ {x} → T x ⇔ x ≡ true
 T-≡ {false} = mk⇔ (λ ())       (λ ())
 T-≡ {true}  = mk⇔ (const refl) (const _)
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index cc3c325a64..a837d6c564 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -54,6 +54,17 @@ cast {zero}  {zero}  eq k       = k
 cast {suc m} {suc n} eq zero    = zero
 cast {suc m} {suc n} eq (suc k) = suc (cast (cong ℕ.pred eq) k)
 
+-- Tests showing that cast does compute on constructors
+
+module _ .(eqs : suc m ≡ suc n) where
+
+  _ : cast eqs zero ≡ zero
+  _ = refl
+
+  _ : .(eq : m ≡ n) (k : Fin m) →
+      cast eqs (suc k) ≡ suc (cast eq k)
+  _ = λ eq k → refl
+
 ------------------------------------------------------------------------
 -- Conversions
 
@@ -77,7 +88,7 @@ fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
 fromℕ<″ zero    {suc _} _    = zero
 fromℕ<″ (suc m) {suc _} m<″n = suc (fromℕ<″ m (ℕ.s<″s⁻¹ m<″n))
 
--- canonical liftings of i:Fin m to larger index
+-- Canonical liftings of i:Fin m to larger index
 
 -- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
 infixl 5 _↑ˡ_
@@ -91,6 +102,7 @@ _↑ʳ_ : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
 zero    ↑ʳ i = i
 (suc n) ↑ʳ i = suc (n ↑ʳ i)
 
+
 -- reduce≥ "m + i" _ = "i".
 
 reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
new file mode 100644
index 0000000000..b35b02ffbc
--- /dev/null
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -0,0 +1,374 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bounded Natural numbers (Fin, without the runtime overhead)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Bounded.Base where
+
+open import Data.Bool.Base using (T; true; false; if_then_else_)
+import Data.Bool.Properties as Boolₚ
+open import Data.Empty using (⊥-elim)
+open import Data.Irrelevant as Irrelevant using (Irrelevant; [_]; pure; _<*>_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; z<s; s<s; s<s⁻¹; NonZero)
+import Data.Nat.Properties as ℕₚ
+import Data.Nat.DivMod as ℕₚ
+open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Refinement as Refinement using (Refinement; _,_; Refinement-syntax; proof)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
+
+open import Function.Base using (id; _$_; _∘_; λ∙; _on_)
+open import Function.Bundles using (Equivalence); open Equivalence using (from; to)
+
+open import Level using (0ℓ)
+
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; refl; cong; subst; sym; ≢-sym)
+open import Relation.Nullary.Decidable using (recompute; T?; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contraposition)
+
+private
+  variable
+    m n : ℕ
+
+------------------------------------------------------------------------
+-- Types
+
+-- Fin n is a type with n elements.
+
+Fin : ℕ → Set
+Fin n = [ m ∈ ℕ ∣ m ℕ.< n ]
+
+¬Fin0 : ¬ (Fin 0)
+¬Fin0 ()
+
+nonZeroIndex : Fin n → ℕ.NonZero n
+nonZeroIndex {n = suc _} _ = _
+
+-- Recovering constructors and pattern matching
+
+fzero : ∀ {n} → Fin (suc n)
+fzero = 0 , [ z<s ]
+
+fsuc : ∀ {n} → Fin n → Fin (suc n)
+fsuc = Refinement.map suc s<s
+
+data View : ∀ {n} (k : Fin n) → Set where
+  zero : View {suc n} fzero
+  suc  : (k : Fin n) → View (fsuc k)
+
+view : (k : Fin n) → View k
+view {suc n} (0 , prf)     = zero
+view {suc n} (suc k , prf) = suc (k , (| s<s⁻¹ prf |))
+
+view⁻¹ : {k : Fin n} → View k → Fin n
+view⁻¹ {k = k} _ = k
+
+-- A conversion: toℕ "i" = i.
+
+toℕ : Fin n → ℕ
+toℕ = Refinement.value
+
+-- A Fin-indexed variant of Fin.
+
+Fin′ : Fin n → Set
+Fin′ i = Fin (toℕ i)
+
+------------------------------------------------------------------------
+-- A cast that actually computes on constructors (as opposed to subst)
+
+cast : .(m ≡ n) → Fin m → Fin n
+cast {m = m} {n = n} eq
+  = Refinement.map id
+  $ subst (_ ℕ.<_) (recompute (m ℕₚ.≟ n) eq)
+
+-- Tests showing that cast does compute on constructors
+
+module _ .(eqs : suc m ≡ suc n) where
+
+  _ : cast eqs fzero ≡ fzero
+  _ = refl
+
+  _ : .(eq : m ≡ n) (k : Fin m) →
+      cast eqs (fsuc k) ≡ fsuc (cast eq k)
+  _ = λ eq k → refl
+
+------------------------------------------------------------------------
+-- Conversions
+
+-- toℕ is defined above.
+
+-- fromℕ n = "n".
+
+fromℕ : (n : ℕ) → Fin (suc n)
+fromℕ n = n , [ ℕₚ.n<1+n n ]
+
+-- fromℕ< {m} _ = "m".
+
+fromℕ< : .(m ℕ.< n) → Fin n
+fromℕ< m<n = _ , [ m<n ]
+
+fromℕ<ᵇ : T (m ℕ.<ᵇ n) → Fin n
+fromℕ<ᵇ p = fromℕ< (ℕₚ.<ᵇ⇒< _ _ p)
+
+-- fromℕ<″ m _ = "m".
+
+fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
+fromℕ<″ m m<″n = m , [ ℕₚ.<″⇒< m<″n ]
+
+-- Canonical liftings of i:Fin m to a larger index
+
+-- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
+infixl 5 _↑ˡ_
+_↑ˡ_ : ∀ {m} → Fin m → ∀ n → Fin (m ℕ.+ n)
+_↑ˡ_ {m} i n = Refinement.map id prf i where
+
+  prf : ∀ {k} → k ℕ.< m → k ℕ.< m ℕ.+ n
+  prf {k} k<m = let open ℕₚ.≤-Reasoning in begin-strict
+    k       ≡⟨ ℕₚ.+-identityʳ k ⟨
+    k ℕ.+ 0 <⟨ ℕₚ.+-mono-<-≤ k<m z≤n ⟩
+    m ℕ.+ n ∎
+
+-- injection on the right: n ↑ʳ "i" = "n + i" in Fin (n + m)
+infixr 5 _↑ʳ_
+_↑ʳ_ : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
+n ↑ʳ i = Refinement.map (n ℕ.+_) (ℕₚ.+-monoʳ-< n) i
+
+-- reduce≥ "m + i" _ = "i".
+
+reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
+reduce≥ {m = m} {n = n} (k , prf) m≤i
+  = k ℕ.∸ m , (| go prf [ m≤i ] |) where
+
+  go : k ℕ.< m ℕ.+ n → m ℕ.≤ k → k ℕ.∸ m ℕ.< n
+  go k<m+n m≤k = let open ℕₚ.≤-Reasoning in begin-strict
+    k ℕ.∸ m       <⟨ ℕₚ.∸-monoˡ-< k<m+n m≤k ⟩
+    m ℕ.+ n ℕ.∸ m ≡⟨ ℕₚ.m+n∸m≡n m n ⟩
+    n             ∎
+
+-- inject⋆ m "i" = "i".
+
+inject : ∀ {i : Fin n} → Fin′ i → Fin n
+inject {i = i} (k , k<i) = k , (| ℕₚ.<-trans k<i (proof i)|)
+
+inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
+inject! {i = i} (k , k<i)
+  = k , (| ℕₚ.<-≤-trans k<i (| ℕ.s≤s⁻¹ (proof i)|) |)
+
+inject₁ : Fin n → Fin (suc n)
+inject₁ (k , k<n) = k , (| ℕₚ.m<n⇒m<1+n k<n |)
+
+inject≤ : Fin m → .(m ℕ.≤ n) → Fin n
+inject≤ (k , k<m) m≤n
+  = k , (| ℕₚ.<-≤-trans k<m [ m≤n ] |)
+
+-- lower₁ "i" _ = "i".
+
+lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
+lower₁ (k , k<1+n) n≢i
+  = k , (| ℕₚ.≤∧≢⇒< (| ℕ.s≤s⁻¹ k<1+n |) [ ≢-sym n≢i ] |)
+
+lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n
+lower (k , _) k<n = k , [ k<n ]
+
+-- A strengthening injection into the minimal Fin fibre.
+
+strengthen : ∀ (i : Fin n) → Fin′ (fsuc i)
+strengthen (k , prf) = (k , [ ℕₚ.≤-refl ])
+
+-- splitAt m "i" = inj₁ "i"      if i < m
+--                 inj₂ "i - m"  if i ≥ m
+-- This is dual to splitAt from Data.Vec.
+
+splitAt : ∀ m {n} → Fin (m ℕ.+ n) → Fin m ⊎ Fin n
+splitAt m i@(k , prf) with T? (k ℕ.<ᵇ m)
+... | yes k<ᵇm = inj₁ (k , [ ℕₚ.<ᵇ⇒< k m k<ᵇm ])
+... | no  k≮ᵇm = inj₂ (reduce≥ i (ℕₚ.≮⇒≥ (k≮ᵇm ∘ ℕₚ.<⇒<ᵇ)))
+
+-- inverse of above function
+join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n)
+join m n = [ _↑ˡ n , m ↑ʳ_ ]′
+
+-- quotRem n "i" = "i % n" , "i / n"
+-- This is dual to group from Data.Vec.
+
+quotRem : ∀ n → Fin (m ℕ.* n) → Fin n × Fin m
+quotRem {m = m} zero i = ⊥-elim (¬Fin0 (subst Fin (ℕₚ.*-zeroʳ m) i))
+quotRem {m = m} n@(suc _) (i , i<m*n)
+  = (i ℕ.% n , [ ℕₚ.m%n<n i n ])
+  , (i ℕ./ n , (| ℕₚ.m<n*o⇒m/o<n i<m*n |))
+
+-- a variant of quotRem the type of whose result matches the order of multiplication
+remQuot : ∀ n → Fin (m ℕ.* n) → Fin m × Fin n
+remQuot i = Product.swap ∘ quotRem i
+
+quotient : ∀ n → Fin (m ℕ.* n) → Fin m
+quotient n = proj₁ ∘ remQuot n
+
+remainder : ∀ n → Fin (m ℕ.* n) → Fin n
+remainder {m} n = proj₂ ∘ remQuot {m} n
+
+-- inverse of remQuot
+combine : Fin m → Fin n → Fin (m ℕ.* n)
+combine {m = suc m} {n = n} (k , k<m) (l , l<n)
+  = (k ℕ.* n) ℕ.+ l , (| go (| ℕ.s≤s⁻¹ k<m |) l<n |)
+
+  where
+
+  go : k ℕ.≤ m → l ℕ.< n → k ℕ.* n ℕ.+ l ℕ.< suc m ℕ.* n
+  go k≤m l<n = let open ℕₚ.≤-Reasoning in begin-strict
+    k ℕ.* n ℕ.+ l <⟨ ℕₚ.+-mono-≤-< (ℕₚ.*-monoˡ-≤ n k≤m) l<n ⟩
+    m ℕ.* n ℕ.+ n ≡⟨ ℕₚ.+-comm (m ℕ.* n) n ⟩
+    n ℕ.+ m ℕ.* n ∎
+
+-- Next in progression after splitAt and remQuot
+finToFun : Fin (m ℕ.^ n) → (Fin n → Fin m)
+finToFun {m = m} {n = suc n} i j with view j
+... | zero    = quotient (m ℕ.^ n) i
+... | (suc j) = finToFun (remainder {m} (m ℕ.^ n) i) j
+
+-- inverse of above function
+funToFin : (Fin m → Fin n) → Fin (n ℕ.^ m)
+funToFin {zero}  f = fzero
+funToFin {suc m} f = combine (f fzero) (funToFin (f ∘ fsuc))
+
+------------------------------------------------------------------------
+-- Operations
+
+-- Folds.
+
+fold : ∀ {t} (T : ℕ → Set t) {m} →
+       (∀ {n} → T n → T (suc n)) →
+       (∀ {n} → T (suc n)) →
+       Fin m → T m
+fold T f x k with view k
+... | zero    = x
+... | (suc i) = f (fold T f x i)
+
+fold′ : ∀ {n t} (T : Fin (suc n) → Set t) →
+        (∀ i → T (inject₁ i) → T (fsuc i)) →
+        T fzero →
+        ∀ i → T i
+fold′ T f x k with view k
+... | zero = x
+fold′ {n = suc n} T f x k | (suc i)  =
+  f i (fold′ (T ∘ inject₁) (f ∘ inject₁) x i)
+
+-- Lifts functions.
+
+lift : ∀ k → (Fin m → Fin n) → Fin (k ℕ.+ m) → Fin (k ℕ.+ n)
+lift {n = n} k f i = [ _↑ˡ n , (k ↑ʳ_) ∘ f ]′ (splitAt k i)
+
+-- "i" + "j" = "i + j".
+
+infixl 6 _+_
+_+_ : ∀ (i : Fin m) (j : Fin n) → Fin (toℕ i ℕ.+ n)
+_+_ {m = m} {n = n} (i , i<m) (j , j<n)
+  = i ℕ.+ j , (| (ℕₚ.+-monoʳ-< i) j<n |)
+
+-- "i" - "j" = "i ∸ j".
+
+infixl 6 _-_
+_-_ : ∀ (i : Fin n) (j : Fin′ (fsuc i)) → Fin (n ℕ.∸ toℕ j)
+(i , i<n) - (j , j<1+i)
+  = i ℕ.∸ j
+  , (| ℕₚ.∸-monoˡ-< i<n (| ℕ.s≤s⁻¹ j<1+i |) |)
+
+-- m ℕ- "i" = "m ∸ i".
+
+infixl 6 _ℕ-_
+_ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
+n ℕ- (j , j<1+n)
+  = n ℕ.∸ j
+  , (| (ℕₚ.≤-reflexive ∘ sym ∘ (λ∙ ℕₚ.∸-suc) ∘ ℕ.s≤s⁻¹) j<1+n |)
+
+-- m ℕ-ℕ "i" = m ∸ i.
+
+infixl 6 _ℕ-ℕ_
+_ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
+n ℕ-ℕ (i , i<1+m) = n ℕ.∸ i
+
+-- pred "i" = "pred i".
+
+pred : Fin n → Fin n
+pred (k , k<n) = ℕ.pred k , (| (ℕₚ.≤-<-trans ℕₚ.pred[n]≤n) k<n |)
+
+-- opposite "i" = "pred n - i" (i.e. the additive inverse).
+
+opposite : Fin n → Fin n
+opposite {n = n@(suc m)} i@(k , _)
+  = m ℕ.∸ k , [ ℕₚ.m<n+o⇒m∸n<o m k (ℕₚ.m≤n+m n k) ]
+
+-- The function f(i,j) = if j>i then j-1 else j
+punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n
+punchOut {n = n} {i = i , i<1+n} {j = j , j<1+n} i≢j
+  = value , (| prf i<1+n (| ℕ.s≤s⁻¹ j<1+n |) |)
+  where
+  value = if i ℕ.<ᵇ j then ℕ.pred j else j
+
+  prf : i ℕ.< suc n → j ℕ.≤ n → value ℕ.< n
+  prf i<1+n j≤n with T? (i ℕ.<ᵇ j)
+  ... | yes i<j rewrite to Boolₚ.T-≡ i<j = let open ℕₚ.≤-Reasoning in begin
+    suc (ℕ.pred j) ≡⟨ ℕₚ.suc-pred j {{ℕ.≢-nonZero (ℕₚ.m<n⇒n≢0 (ℕₚ.<ᵇ⇒< i j i<j))}} ⟩
+    j              ≤⟨ j≤n ⟩
+    n              ∎
+  ... | no i≮j rewrite to Boolₚ.¬T-≡ i≮j = j<n
+
+    where
+    j<n : j ℕ.< n
+    j<n with ℕₚ.m<1+n⇒m<n∨m≡n i<1+n
+    ... | inj₁ i<n = ℕₚ.≤-<-trans (ℕₚ.≮⇒≥ (contraposition ℕₚ.<⇒<ᵇ i≮j)) i<n
+    ... | inj₂ refl = ℕₚ.≤∧≢⇒< j≤n (≢-sym (i≢j ∘ Refinement.value-injective))
+
+-- The function f(i,j) = if j≥i then j+1 else j
+punchIn : Fin (suc n) → Fin n → Fin (suc n)
+punchIn {n = n} (i , _) (j , j<n) = value , (| prf j<n |)
+  where
+  value = if j ℕ.<ᵇ i then j else suc j
+  prf : j ℕ.< n → value ℕ.< suc n
+  prf j<n with j ℕ.<ᵇ i
+  ... | true  = s<s (ℕₚ.<⇒≤ j<n)
+  ... | false = s<s j<n
+
+-- The function f(i,j) such that f(i,j) = if j≤i then j else j-1
+pinch : Fin n → Fin (suc n) → Fin n
+pinch {n = n} (i , i<n) (j , j<1+n) = value , (| prf i<n (| ℕ.s≤s⁻¹ j<1+n |) |)
+  where
+  value = if i ℕ.<ᵇ j then ℕ.pred j else j
+  prf : i ℕ.< n → j ℕ.≤ n → value ℕ.< n
+  prf i<n j≤n with T? (i ℕ.<ᵇ j)
+  ... | yes i<j rewrite to Boolₚ.T-≡ i<j = let open ℕₚ.≤-Reasoning in begin
+    suc (ℕ.pred j) ≡⟨ ℕₚ.suc-pred j {{ℕ.≢-nonZero (ℕₚ.m<n⇒n≢0 (ℕₚ.<ᵇ⇒< i j i<j))}} ⟩
+    j              ≤⟨ j≤n ⟩
+    n              ∎
+  ... | no i≮j rewrite to Boolₚ.¬T-≡ i≮j = let open ℕₚ.≤-Reasoning in begin-strict
+    j ≤⟨ ℕₚ.≮⇒≥ (contraposition ℕₚ.<⇒<ᵇ i≮j) ⟩
+    i <⟨ i<n ⟩
+    n ∎
+
+------------------------------------------------------------------------
+-- Order relations
+
+infix 4 _≤_ _≥_ _<_ _>_ _≰_ _≮_
+
+_≤_ : IRel Fin 0ℓ
+i ≤ j = toℕ i ℕ.≤ toℕ j
+
+_≥_ : IRel Fin 0ℓ
+i ≥ j = toℕ i ℕ.≥ toℕ j
+
+_<_ : IRel Fin 0ℓ
+i < j = toℕ i ℕ.< toℕ j
+
+_>_ : IRel Fin 0ℓ
+i > j = toℕ i ℕ.> toℕ j
+
+_≰_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≰ j = ¬ (i ≤ j)
+
+_≮_ : ∀ {n} → Rel (Fin n) 0ℓ
+i ≮ j = ¬ (i < j)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 0fe5b9dba9..6f8b85e38f 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -2187,6 +2187,9 @@ n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
 ≤″⇒≤ : _≤″_ ⇒ _≤_
 ≤″⇒≤ (k , refl) = m≤m+n _ k
 
+<″⇒< : _<″_ ⇒ _<_
+<″⇒< = ≤″⇒≤
+
 -- equivalence to the old definition of _≤″_
 
 ≤″-proof : (le : m ≤″ n) → let k , _ = le in m + k ≡ n
diff --git a/src/Function/Base.agda b/src/Function/Base.agda
index 1f8f3f0b18..9affb90225 100644
--- a/src/Function/Base.agda
+++ b/src/Function/Base.agda
@@ -107,6 +107,10 @@ f $- = f _
 λ- f = λ x → f
 {-# INLINE λ- #-}
 
+λ∙ : ∀ {A : Set a} {B : .A → Set b} → (.(x : A) → B x) → ((x : A) → B x)
+λ∙ f = λ x → f x
+{-# INLINE λ∙ #-}
+
 -- Case expressions (to be used with pattern-matching lambdas, see
 -- README.Case).
 
@@ -267,4 +271,3 @@ case_return_of_ = case_returning_of_
 "case_return_of_ was deprecated in v2.0.
 Please use case_returning_of_ instead."
 #-}
-