From acd95241fe28787f6cfe003090f7581b2e4ad96f Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 8 Apr 2026 18:12:56 +0100
Subject: [PATCH 01/11] [ new ] Fin n as a refinement

This version has a better runtime representation
This version lets us have efficient implementations of
things like splitAt and quotRem
---
 CHANGELOG.md                   |   5 +
 src/Data/Fin/Base.agda         |  14 +-
 src/Data/Nat/Bounded/Base.agda | 339 +++++++++++++++++++++++++++++++++
 3 files changed, 357 insertions(+), 1 deletion(-)
 create mode 100644 src/Data/Nat/Bounded/Base.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 42844d01ef..fbbcd38e30 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -184,6 +184,11 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
+* A variation on `Fin` seen as a `Nat` refinement
+  ```
+  Data.Nat.Bounded.Base
+  ```
+
 * Refactoring of `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties` as smaller modules:
   ```
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup
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..baa630177c
--- /dev/null
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -0,0 +1,339 @@
+------------------------------------------------------------------------
+-- 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)
+import Data.Bool.Properties as Boolₚ
+open import Data.Empty using (⊥-elim)
+open import Data.Irrelevant as Irrelevant using (Irrelevant; [_])
+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)
+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)
+
+open import Level using (0ℓ)
+
+open import Relation.Binary 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 (¬_)
+
+private
+  variable
+    m n : ℕ
+
+------------------------------------------------------------------------
+-- Types
+
+-- Fin n is a type with n elements.
+
+Fin : ℕ → Set
+Fin n = [ m ∈ ℕ ∣ m ℕ.< n ]
+
+¬Fin0 : ¬ (Fin 0)
+¬Fin0 ()
+
+nonZero : Fin n → ℕ.NonZero n
+nonZero {suc n} k = _
+
+-- 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 , Irrelevant.map s<s⁻¹ prf)
+
+unview : {k : Fin n} → View k → Fin n
+unview {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".
+
+open import Relation.Binary using (_⇒_)
+
+<″⇒< : ℕ._<″_ ⇒ ℕ._<_
+<″⇒< = ℕₚ.≤″⇒≤
+
+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 , (Irrelevant.map go prf Irrelevant.<*> [ 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 , (Irrelevant.map ℕₚ.<-trans k<i Irrelevant.<*> Refinement.proof i)
+
+inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
+inject! {i = i} (k , k<i)
+  = k , (Irrelevant.map ℕₚ.<-≤-trans k<i
+        Irrelevant.<*> Irrelevant.map ℕ.s≤s⁻¹ (Refinement.proof i))
+
+inject₁ : Fin n → Fin (suc n)
+inject₁ (k , k<n)
+  = k , Irrelevant.map ℕₚ.m<n⇒m<1+n k<n
+
+inject≤ : Fin m → .(m ℕ.≤ n) → Fin n
+inject≤ (k , k<m) m≤n
+  = k , (Irrelevant.map ℕₚ.<-≤-trans k<m Irrelevant.<*> [ m≤n ])
+
+-- lower₁ "i" _ = "i".
+
+lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
+lower₁ (k , k<1+n) n≢i
+  = k , Irrelevant.map (λ prf → ℕₚ.≤∧≢⇒< (ℕ.s≤s⁻¹ prf) (≢-sym n≢i)) k<1+n
+
+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 , Irrelevant.map ℕₚ.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
+  , (Irrelevant.map go (Irrelevant.map ℕ.s≤s⁻¹ k<m) Irrelevant.<*> 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 , Irrelevant.map (ℕₚ.+-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
+  , (Irrelevant.map (λ i<n → ℕₚ.∸-monoˡ-< i<n ∘ ℕ.s≤s⁻¹) i<n
+     Irrelevant.<*> 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
+  , Irrelevant.map (λ j<1+n → ℕₚ.≤-reflexive $ sym $ ℕₚ.∸-suc (ℕ.s≤s⁻¹ j<1+n)) 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 , Irrelevant.map (ℕₚ.≤-<-trans ℕₚ.pred[n]≤n) k<n
+
+-- opposite "i" = "pred n - i" (i.e. the additive inverse).
+
+opposite : Fin n → Fin n
+opposite {n} i@(k , prf)
+  = n ℕ.∸ suc k
+  , [ ℕₚ.m<n+o⇒m∸n<o n (suc k) {n} ⦃ nonZero i ⦄ (ℕₚ.m<n+m n z<s) ]
+
+
+------------------------------------------------------------------------
+-- 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)

From 5a293916cabc9a11a72be7e997b86ae10068b929 Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 10:02:26 +0100
Subject: [PATCH 02/11] ASCII-fy

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Data/Nat/Bounded/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index baa630177c..eaa86f11e6 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -312,7 +312,7 @@ pred (k , k<n) = ℕ.pred k , Irrelevant.map (ℕₚ.≤-<-trans ℕₚ.pred[n]
 opposite : Fin n → Fin n
 opposite {n} i@(k , prf)
   = n ℕ.∸ suc k
-  , [ ℕₚ.m<n+o⇒m∸n<o n (suc k) {n} ⦃ nonZero i ⦄ (ℕₚ.m<n+m n z<s) ]
+  , [ ℕₚ.m<n+o⇒m∸n<o n (suc k) {n} {{ nonZero i}} (ℕₚ.m<n+m n z<s) ]
 
 
 ------------------------------------------------------------------------

From 22b633754edf0793e9152c42da649a6d46be4ba2 Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 10:02:51 +0100
Subject: [PATCH 03/11] Rename `nonZero`

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Data/Nat/Bounded/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index eaa86f11e6..fcdaef450a 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -46,8 +46,8 @@ Fin n = [ m ∈ ℕ ∣ m ℕ.< n ]
 ¬Fin0 : ¬ (Fin 0)
 ¬Fin0 ()
 
-nonZero : Fin n → ℕ.NonZero n
-nonZero {suc n} k = _
+nonZeroIndex : Fin n → ℕ.NonZero n
+nonZeroIndex {n = suc _} _ = _
 
 -- Recovering constructors and pattern matching
 

From 34af74ef56a0c8e5914e5a912b510772d38308c7 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 11:01:19 +0100
Subject: [PATCH 04/11] [ fix ] move lemma to Data.Nat.Properties

---
 CHANGELOG.md                   | 1 +
 src/Data/Nat/Bounded/Base.agda | 9 ++-------
 src/Data/Nat/Properties.agda   | 3 +++
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fbbcd38e30..737f3acce1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -396,6 +396,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/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index fcdaef450a..6a480174fe 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -24,7 +24,7 @@ open import Function.Bundles using (Equivalence); open Equivalence using (from)
 
 open import Level using (0ℓ)
 
-open import Relation.Binary using (Rel)
+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)
@@ -117,13 +117,8 @@ fromℕ<ᵇ p = fromℕ< (ℕₚ.<ᵇ⇒< _ _ p)
 
 -- fromℕ<″ m _ = "m".
 
-open import Relation.Binary using (_⇒_)
-
-<″⇒< : ℕ._<″_ ⇒ ℕ._<_
-<″⇒< = ℕₚ.≤″⇒≤
-
 fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
-fromℕ<″ m m<″n = m , [ <″⇒< m<″n ]
+fromℕ<″ m m<″n = m , [ ℕₚ.<″⇒< m<″n ]
 
 -- Canonical liftings of i:Fin m to a larger index
 
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

From c7ee749e567d4ecd09a0a1bb55c249d84f637852 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 11:03:18 +0100
Subject: [PATCH 05/11] [ cosmetic ] use idiom brackets

---
 src/Data/Nat/Bounded/Base.agda | 35 +++++++++++++++-------------------
 1 file changed, 15 insertions(+), 20 deletions(-)

diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index 6a480174fe..211795dbd1 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -11,12 +11,12 @@ module Data.Nat.Bounded.Base where
 open import Data.Bool.Base using (T; true; false)
 import Data.Bool.Properties as Boolₚ
 open import Data.Empty using (⊥-elim)
-open import Data.Irrelevant as Irrelevant using (Irrelevant; [_])
+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)
+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_)
@@ -63,7 +63,7 @@ data View : ∀ {n} (k : Fin n) → Set where
 
 view : (k : Fin n) → View k
 view {suc n} (0 , prf)     = zero
-view {suc n} (suc k , prf) = suc (k , Irrelevant.map s<s⁻¹ prf)
+view {suc n} (suc k , prf) = suc (k , (| s<s⁻¹ prf |))
 
 unview : {k : Fin n} → View k → Fin n
 unview {k = k} _ = k
@@ -142,7 +142,7 @@ n ↑ʳ i = Refinement.map (n ℕ.+_) (ℕₚ.+-monoʳ-< n) i
 
 reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
 reduce≥ {m = m} {n = n} (k , prf) m≤i
-  = k ℕ.∸ m , (Irrelevant.map go prf Irrelevant.<*> [ m≤i ]) where
+  = 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
@@ -153,27 +153,24 @@ reduce≥ {m = m} {n = n} (k , prf) m≤i
 -- inject⋆ m "i" = "i".
 
 inject : ∀ {i : Fin n} → Fin′ i → Fin n
-inject {i = i} (k , k<i)
-  = k , (Irrelevant.map ℕₚ.<-trans k<i Irrelevant.<*> Refinement.proof i)
+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 , (Irrelevant.map ℕₚ.<-≤-trans k<i
-        Irrelevant.<*> Irrelevant.map ℕ.s≤s⁻¹ (Refinement.proof i))
+  = k , (| ℕₚ.<-≤-trans k<i (| ℕ.s≤s⁻¹ (proof i)|) |)
 
 inject₁ : Fin n → Fin (suc n)
-inject₁ (k , k<n)
-  = k , Irrelevant.map ℕₚ.m<n⇒m<1+n k<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 , (Irrelevant.map ℕₚ.<-≤-trans k<m Irrelevant.<*> [ 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 , Irrelevant.map (λ prf → ℕₚ.≤∧≢⇒< (ℕ.s≤s⁻¹ prf) (≢-sym n≢i)) k<1+n
+  = k , (| (λ prf → ℕₚ.≤∧≢⇒< (ℕ.s≤s⁻¹ prf) (≢-sym n≢i)) k<1+n |)
 
 lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n
 lower (k , _) k<n = k , [ k<n ]
@@ -203,7 +200,7 @@ 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 , Irrelevant.map ℕₚ.m<n*o⇒m/o<n i<m*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
@@ -218,8 +215,7 @@ 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
-  , (Irrelevant.map go (Irrelevant.map ℕ.s≤s⁻¹ k<m) Irrelevant.<*> l<n)
+  = (k ℕ.* n) ℕ.+ l , (| go (| ℕ.s≤s⁻¹ k<m |) l<n |)
 
   where
 
@@ -272,7 +268,7 @@ lift {n = n} k f i = [ _↑ˡ n , (k ↑ʳ_) ∘ f ]′ (splitAt k i)
 infixl 6 _+_
 _+_ : ∀ (i : Fin m) (j : Fin n) → Fin (toℕ i ℕ.+ n)
 _+_ {m = m} {n = n} (i , i<m) (j , j<n)
-  = i ℕ.+ j , Irrelevant.map (ℕₚ.+-monoʳ-< i) j<n
+  = i ℕ.+ j , (| (ℕₚ.+-monoʳ-< i) j<n |)
 
 -- "i" - "j" = "i ∸ j".
 
@@ -280,8 +276,7 @@ infixl 6 _-_
 _-_ : ∀ (i : Fin n) (j : Fin′ (fsuc i)) → Fin (n ℕ.∸ toℕ j)
 (i , i<n) - (j , j<1+i)
   = i ℕ.∸ j
-  , (Irrelevant.map (λ i<n → ℕₚ.∸-monoˡ-< i<n ∘ ℕ.s≤s⁻¹) i<n
-     Irrelevant.<*> j<1+i)
+  , (| (λ i<n → ℕₚ.∸-monoˡ-< i<n ∘ ℕ.s≤s⁻¹) i<n j<1+i |)
 
 -- m ℕ- "i" = "m ∸ i".
 
@@ -289,7 +284,7 @@ infixl 6 _ℕ-_
 _ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
 n ℕ- (j , j<1+n)
   = n ℕ.∸ j
-  , Irrelevant.map (λ j<1+n → ℕₚ.≤-reflexive $ sym $ ℕₚ.∸-suc (ℕ.s≤s⁻¹ j<1+n)) j<1+n
+  , (| (λ j<1+n → ℕₚ.≤-reflexive $ sym $ ℕₚ.∸-suc (ℕ.s≤s⁻¹ j<1+n)) j<1+n |)
 
 -- m ℕ-ℕ "i" = m ∸ i.
 
@@ -300,7 +295,7 @@ n ℕ-ℕ (i , i<1+m) = n ℕ.∸ i
 -- pred "i" = "pred i".
 
 pred : Fin n → Fin n
-pred (k , k<n) = ℕ.pred k , Irrelevant.map (ℕₚ.≤-<-trans ℕₚ.pred[n]≤n) k<n
+pred (k , k<n) = ℕ.pred k , (| (ℕₚ.≤-<-trans ℕₚ.pred[n]≤n) k<n |)
 
 -- opposite "i" = "pred n - i" (i.e. the additive inverse).
 

From 7fbf99bcb3721628241692990f726e72d3899a7e Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 11:06:31 +0100
Subject: [PATCH 06/11] Simplify opposite

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Data/Nat/Bounded/Base.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index 211795dbd1..48b67176f3 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -300,9 +300,9 @@ 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} i@(k , prf)
-  = n ℕ.∸ suc k
-  , [ ℕₚ.m<n+o⇒m∸n<o n (suc k) {n} {{ nonZero i}} (ℕₚ.m<n+m n z<s) ]
+opposite {n = n@(suc m)} i@(k , _)
+  = m ℕ.∸ k , [ ℕₚ.m<n+o⇒m∸n<o m k (ℕₚ.m≤n+m n k) ]
+
 
 
 ------------------------------------------------------------------------

From 5a1a791eb35753cf0f747b810467e7c7c1f720f4 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 11:12:29 +0100
Subject: [PATCH 07/11] [ cleanup ] gadget to convert irrelevant-domains

---
 CHANGELOG.md                   | 5 +++++
 src/Data/Nat/Bounded/Base.agda | 8 ++++----
 src/Function/Base.agda         | 5 ++++-
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 737f3acce1..109a49c7cd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -122,6 +122,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     ↦   _∩?_
diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index 48b67176f3..0bdfc183b9 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -19,7 +19,7 @@ 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.Base using (id; _$_; _∘_; λ∙; _on_)
 open import Function.Bundles using (Equivalence); open Equivalence using (from)
 
 open import Level using (0ℓ)
@@ -170,7 +170,7 @@ inject≤ (k , k<m) m≤n
 
 lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
 lower₁ (k , k<1+n) n≢i
-  = k , (| (λ prf → ℕₚ.≤∧≢⇒< (ℕ.s≤s⁻¹ prf) (≢-sym n≢i)) k<1+n |)
+  = 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 ]
@@ -276,7 +276,7 @@ infixl 6 _-_
 _-_ : ∀ (i : Fin n) (j : Fin′ (fsuc i)) → Fin (n ℕ.∸ toℕ j)
 (i , i<n) - (j , j<1+i)
   = i ℕ.∸ j
-  , (| (λ i<n → ℕₚ.∸-monoˡ-< i<n ∘ ℕ.s≤s⁻¹) i<n j<1+i |)
+  , (| ℕₚ.∸-monoˡ-< i<n (| ℕ.s≤s⁻¹ j<1+i |) |)
 
 -- m ℕ- "i" = "m ∸ i".
 
@@ -284,7 +284,7 @@ infixl 6 _ℕ-_
 _ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
 n ℕ- (j , j<1+n)
   = n ℕ.∸ j
-  , (| (λ j<1+n → ℕₚ.≤-reflexive $ sym $ ℕₚ.∸-suc (ℕ.s≤s⁻¹ j<1+n)) j<1+n |)
+  , (| (ℕₚ.≤-reflexive ∘ sym ∘ (λ∙ ℕₚ.∸-suc) ∘ ℕ.s≤s⁻¹) j<1+n |)
 
 -- m ℕ-ℕ "i" = m ∸ i.
 
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."
 #-}
-

From 9c0c18ac1eede8e3fc6c0c424082c37679462947 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 11:19:17 +0100
Subject: [PATCH 08/11] =?UTF-8?q?[=20james=20]=20rename=20unview=20->=20vi?=
 =?UTF-8?q?ew=E2=81=BB=C2=B9?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat/Bounded/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index 0bdfc183b9..fcc7e44bea 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -65,8 +65,8 @@ view : (k : Fin n) → View k
 view {suc n} (0 , prf)     = zero
 view {suc n} (suc k , prf) = suc (k , (| s<s⁻¹ prf |))
 
-unview : {k : Fin n} → View k → Fin n
-unview {k = k} _ = k
+view⁻¹ : {k : Fin n} → View k → Fin n
+view⁻¹ {k = k} _ = k
 
 -- A conversion: toℕ "i" = i.
 

From 4c667b952ff6e267b4c589cc1e462de67118776f Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Thu, 9 Apr 2026 11:22:03 +0100
Subject: [PATCH 09/11] [ james ] More descriptive CHANGELOG entry

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 109a49c7cd..d307c955a5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -189,7 +189,7 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
-* A variation on `Fin` seen as a `Nat` refinement
+* A variation on `Fin` seen as a `Nat` refinement, with better runtime representation and performance.
   ```
   Data.Nat.Bounded.Base
   ```

From 2dc049f73db6a041c1a50cad8443b372aa13a79e Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Tue, 14 Apr 2026 10:29:17 +0100
Subject: [PATCH 10/11] [ tmp ] merging James' punch* functions

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Data/Nat/Bounded/Base.agda | 53 +++++++++++++++++++++++++++++++++-
 1 file changed, 52 insertions(+), 1 deletion(-)

diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index fcc7e44bea..8274dead6d 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -303,7 +303,58 @@ 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 , [ [p] ]} {j = j , [ [q] ]} i≢j  = value , (| prf |)
+  where
+  value = if i <ᵇ j then ℕ.pred j else j
+  prf : value ℕ.< n
+  prf using q ← recompute (j ℕₚ.≤? n) (ℕ.s≤s⁻¹ [q]) with i <ᵇ j in eq
+  ... | true  = j≤n
+    where
+    i<j : T (i ℕ.<ᵇ j)
+    i<j rewrite eq = _
+    j≤n : suc (ℕ.pred j) ℕ.≤ n
+    j≤n rewrite ℕₚ.suc-pred j {{ℕ.≢-nonZero (ℕₚ.m<n⇒n≢0 (ℕₚ.<ᵇ⇒< i j i<j))}} = q
+  ... | false = j<n
+    where
+    i≮j : ¬ T (i <ᵇ j)
+    i≮j rewrite eq = id
+    j<n : j ℕ.< n
+    j<n with ℕₚ.m<1+n⇒m<n∨m≡n (recompute (i ℕₚ.<? suc n) [p])
+    ... | inj₁ i<n = ℕₚ.≤-<-trans (ℕₚ.≮⇒≥ (contraposition ℕₚ.<⇒<ᵇ i≮j)) i<n
+    ... | inj₂ refl = ℕₚ.≤∧≢⇒< q (≢-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 , [ [p] ]) = value , (| prf |)
+  where
+  value = if j <ᵇ i then j else suc j
+  prf : value ℕ.< suc n
+  prf using p ← recompute (j ℕₚ.<? n) [p] with j <ᵇ i
+  ... | true  = s<s (ℕₚ.<⇒≤ p)
+  ... | false = s<s p
+
+-- 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 , [ [p] ]) (j , [ [q] ]) = value , (| prf |)
+  where
+  value = if i <ᵇ j then ℕ.pred j else j
+  prf : value ℕ.< n
+  prf using q ← recompute (j ℕₚ.≤? n) (ℕ.s≤s⁻¹ [q]) with i <ᵇ j in eq
+  ... | true  = j≤n
+    where
+    i<j : T (i ℕ.<ᵇ j)
+    i<j rewrite eq = _
+    j≤n : suc (ℕ.pred j) ℕ.≤ n
+    j≤n rewrite ℕₚ.suc-pred j {{ℕ.≢-nonZero (ℕₚ.m<n⇒n≢0 (ℕₚ.<ᵇ⇒< i j i<j))}} = q
+  ... | false = ℕₚ.≤-<-trans (ℕₚ.≮⇒≥ (contraposition ℕₚ.<⇒<ᵇ i≮j)) i<n
+    where
+    i≮j : ¬ T (i <ᵇ j)
+    i≮j rewrite eq = id
+    i<n : i ℕ.< n
+    i<n = recompute (i ℕₚ.<? n) [p]
 
 ------------------------------------------------------------------------
 -- Order relations

From ec9e4bdc08b00908b59da80b298249414de368bd Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 14 Apr 2026 10:56:30 +0100
Subject: [PATCH 11/11] [ cleanup ] avoid recompute, rebuilding (T (i < j))

---
 CHANGELOG.md                   |  6 +++
 src/Data/Bool/Properties.agda  |  6 ++-
 src/Data/Nat/Bounded/Base.agda | 76 ++++++++++++++++------------------
 3 files changed, 46 insertions(+), 42 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d307c955a5..7127932e63 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -287,6 +287,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
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/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
index 8274dead6d..b35b02ffbc 100644
--- a/src/Data/Nat/Bounded/Base.agda
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -8,7 +8,7 @@
 
 module Data.Nat.Bounded.Base where
 
-open import Data.Bool.Base using (T; true; false)
+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; _<*>_)
@@ -20,7 +20,7 @@ open import Data.Refinement as Refinement using (Refinement; _,_; Refinement-syn
 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)
+open import Function.Bundles using (Equivalence); open Equivalence using (from; to)
 
 open import Level using (0ℓ)
 
@@ -29,7 +29,7 @@ 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 (¬_)
+open import Relation.Nullary.Negation.Core using (¬_; contraposition)
 
 private
   variable
@@ -305,56 +305,50 @@ opposite {n = n@(suc m)} i@(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 , [ [p] ]} {j = j , [ [q] ]} i≢j  = value , (| prf |)
+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 : value ℕ.< n
-  prf using q ← recompute (j ℕₚ.≤? n) (ℕ.s≤s⁻¹ [q]) with i <ᵇ j in eq
-  ... | true  = j≤n
-    where
-    i<j : T (i ℕ.<ᵇ j)
-    i<j rewrite eq = _
-    j≤n : suc (ℕ.pred j) ℕ.≤ n
-    j≤n rewrite ℕₚ.suc-pred j {{ℕ.≢-nonZero (ℕₚ.m<n⇒n≢0 (ℕₚ.<ᵇ⇒< i j i<j))}} = q
-  ... | false = j<n
+  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
-    i≮j : ¬ T (i <ᵇ j)
-    i≮j rewrite eq = id
     j<n : j ℕ.< n
-    j<n with ℕₚ.m<1+n⇒m<n∨m≡n (recompute (i ℕₚ.<? suc n) [p])
+    j<n with ℕₚ.m<1+n⇒m<n∨m≡n i<1+n
     ... | inj₁ i<n = ℕₚ.≤-<-trans (ℕₚ.≮⇒≥ (contraposition ℕₚ.<⇒<ᵇ i≮j)) i<n
-    ... | inj₂ refl = ℕₚ.≤∧≢⇒< q (≢-sym (i≢j ∘ Refinement.value-injective))
+    ... | 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 , [ [p] ]) = value , (| prf |)
+punchIn {n = n} (i , _) (j , j<n) = value , (| prf j<n |)
   where
-  value = if j <ᵇ i then j else suc j
-  prf : value ℕ.< suc n
-  prf using p ← recompute (j ℕₚ.<? n) [p] with j <ᵇ i
-  ... | true  = s<s (ℕₚ.<⇒≤ p)
-  ... | false = s<s p
+  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 , [ [p] ]) (j , [ [q] ]) = value , (| prf |)
+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 : value ℕ.< n
-  prf using q ← recompute (j ℕₚ.≤? n) (ℕ.s≤s⁻¹ [q]) with i <ᵇ j in eq
-  ... | true  = j≤n
-    where
-    i<j : T (i ℕ.<ᵇ j)
-    i<j rewrite eq = _
-    j≤n : suc (ℕ.pred j) ℕ.≤ n
-    j≤n rewrite ℕₚ.suc-pred j {{ℕ.≢-nonZero (ℕₚ.m<n⇒n≢0 (ℕₚ.<ᵇ⇒< i j i<j))}} = q
-  ... | false = ℕₚ.≤-<-trans (ℕₚ.≮⇒≥ (contraposition ℕₚ.<⇒<ᵇ i≮j)) i<n
-    where
-    i≮j : ¬ T (i <ᵇ j)
-    i≮j rewrite eq = id
-    i<n : i ℕ.< n
-    i<n = recompute (i ℕₚ.<? n) [p]
+  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