From c7d14558747d34b237f78ab61e63757628e71a04 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 7 Feb 2023 17:15:01 +0000
Subject: [PATCH 1/9] a view-based analysis of `punchOut`, `punchIn` and
 `pinch` from `Data.Fin`

---
 src/Data/Fin/Relation/Ternary/Pinch.agda    | 86 +++++++++++++++++++++
 src/Data/Fin/Relation/Ternary/PunchIn.agda  | 75 ++++++++++++++++++
 src/Data/Fin/Relation/Ternary/PunchOut.agda | 76 ++++++++++++++++++
 3 files changed, 237 insertions(+)
 create mode 100644 src/Data/Fin/Relation/Ternary/Pinch.agda
 create mode 100644 src/Data/Fin/Relation/Ternary/PunchIn.agda
 create mode 100644 src/Data/Fin/Relation/Ternary/PunchOut.agda

diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
new file mode 100644
index 0000000000..4a423acba7
--- /dev/null
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -0,0 +1,86 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The 'punchOut view' of the function `punchOut` defined on finite sets
+------------------------------------------------------------------------
+
+-- This example of a "view of a function via its graph relation" is inspired
+-- by Nathan van Doorn's recent PR#1913.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Relation.Ternary.Pinch where
+
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; _≤_; _<_; pinch)
+open import Data.Fin.Properties using (suc-injective)
+open import Data.Nat.Base as Nat using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; ∣_-_∣)
+open import Data.Nat.Properties using (≤-refl; <⇒≤; ∣n-n∣≡0)
+open import Function.Base using (id; _∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
+
+------------------------------------------------------------------------
+-- The View, considered as a ternary relation
+
+data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
+
+  any-zero : ∀ {n} (i : Fin (suc n))             → View i zero zero
+  zero-suc : ∀ {n} (j : Fin (suc n))             → View zero (suc j) j
+  suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
+
+-- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
+
+view : ∀ {n} i j → View {n} i j (pinch i j)
+view {suc _} i zero    = any-zero i
+view   zero    (suc j) = zero-suc j
+view   (suc i) (suc j) = suc-suc (view i j)
+
+-- The View is complete
+
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → k ≡ pinch i j
+view-complete (any-zero i) = refl
+view-complete (zero-suc j) = refl
+view-complete (suc-suc v)  = cong suc (view-complete v)
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+{- pinch-mono≤ -}
+j≤k⇒view-j≤view-k : ∀ {n} {i} {j k} {p q} → View {n} i j p → View {n} i k q →
+                     j ≤ k → p ≤ q
+j≤k⇒view-j≤view-k (any-zero _) _            _         = z≤n
+j≤k⇒view-j≤view-k (zero-suc _) (zero-suc _) (s≤s j≤k) = j≤k
+j≤k⇒view-j≤view-k (suc-suc v)  (suc-suc w)  (s≤s j≤k) = s≤s (j≤k⇒view-j≤view-k v w j≤k)
+
+pinch-mono≤ : ∀ {n} (i : Fin n) {j k} →
+                j ≤ k → pinch i j ≤ pinch i k
+pinch-mono≤ i {j} {k} = j≤k⇒view-j≤view-k (view i j) (view i k)
+
+{- pinch-cancel< -}
+view-j<view-k⇒j<k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+                     p < q → j < k
+view-j<view-k⇒j<k (any-zero _) (zero-suc _) _         = z<s
+view-j<view-k⇒j<k (any-zero _) (suc-suc _)  _         = z<s
+view-j<view-k⇒j<k (zero-suc _) (zero-suc _) p<q       = s<s p<q
+view-j<view-k⇒j<k (suc-suc v)  (suc-suc w)  (s<s p<q) = s<s (view-j<view-k⇒j<k v w p<q)
+
+pinch-cancel< : ∀ {n} (i : Fin (suc n)) {j k} →
+                  (pinch i j < pinch i k) → j < k
+pinch-cancel< i {j} {k} = view-j<view-k⇒j<k (view i j) (view i k)
+
+{- pinch-cancel≡ -}
+view-j≡view-k⇒∣j-k∣≤1 : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+                        p ≡ q → ∣ (toℕ j) - (toℕ k)∣ Nat.≤ 1
+view-j≡view-k⇒∣j-k∣≤1 v w refl = helper v w
+  where
+    helper : ∀ {n} {i j k} {r} → View {n} i j r → View {n} i k r →
+             ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
+    helper (any-zero _)    (any-zero _)    = z≤n
+    helper (any-zero zero) (zero-suc zero) = ≤-refl
+    helper (zero-suc zero) (any-zero zero) = ≤-refl
+    helper (zero-suc j)    (zero-suc j) rewrite ∣n-n∣≡0 (toℕ j) = z≤n
+    helper (suc-suc v)     (suc-suc w) = helper v w
+
+pinch-cancel≡ : ∀ {n} (i : Fin n) {j k} →
+                (pinch i j ≡ pinch i k) → ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
+pinch-cancel≡ i {j} {k} = view-j≡view-k⇒∣j-k∣≤1 (view i j) (view i k)
+
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
new file mode 100644
index 0000000000..f45aa1657d
--- /dev/null
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -0,0 +1,75 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The 'punchOut view' of the function `punchOut` defined on finite sets
+------------------------------------------------------------------------
+
+-- This example of a "view of a function via its graph relation" is inspired
+-- by Nathan van Doorn's recent PR#1913.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Relation.Ternary.PunchIn where
+
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn)
+open import Data.Fin.Properties using (suc-injective)
+open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
+open import Function.Base using (id; _∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
+
+------------------------------------------------------------------------
+-- The View, considered as a ternary relation
+
+data View : ∀ {n} (i : Fin (suc n)) (j : Fin n) (k : Fin (suc n)) → Set where
+
+  zero-suc : ∀ {n} (j : Fin n)                   → View zero j (suc j)
+  suc-zero : ∀ {n} (i : Fin (suc n))             → View (suc i) zero zero
+  suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
+
+-- The View enforces the codomain postcondition
+
+Codomain : ∀ {n} (i : Fin (suc n)) (j : Fin n) → Set
+Codomain i j = punchIn i j ≢ i
+
+view-codomain : ∀ {n} {i} {j} {k} → View {n} i j k → Codomain i j
+view-codomain (suc-suc v) = (view-codomain v) ∘ suc-injective
+
+-- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
+
+view : ∀ {n} i j → View {n} i j (punchIn i j)
+view zero         j  = zero-suc j
+view (suc i) zero    = suc-zero i
+view (suc i) (suc j) = suc-suc (view i j)
+
+-- The View is complete
+
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → k ≡ punchIn i j
+view-complete (zero-suc j) = refl
+view-complete (suc-zero i) = refl
+view-complete (suc-suc v)  = cong suc (view-complete v)
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+{- punchIn-mono≤ -}
+j≤k⇒view-j≤view-k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+                     j ≤ k → p ≤ q
+j≤k⇒view-j≤view-k (zero-suc _) (zero-suc _)  j≤k     = s≤s j≤k
+j≤k⇒view-j≤view-k (suc-zero i) _             _       = z≤n
+j≤k⇒view-j≤view-k (suc-suc v)  (suc-suc w) (s≤s j≤k) = s≤s (j≤k⇒view-j≤view-k v w j≤k)
+
+punchIn-mono≤ : ∀ {n} (i : Fin (suc n)) {j k} →
+                j ≤ k → punchIn i j ≤ punchIn i k
+punchIn-mono≤ i {j} {k} = j≤k⇒view-j≤view-k (view i j) (view i k)
+
+{- punchIn-cancel≤ -}
+view-j≤view-k⇒j≤k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+                     p ≤ q → j ≤ k
+view-j≤view-k⇒j≤k (zero-suc _) (zero-suc _) (s≤s p≤q) = p≤q
+view-j≤view-k⇒j≤k (suc-zero i) _            _         = z≤n
+view-j≤view-k⇒j≤k (suc-suc v)  (suc-suc w)  (s≤s p≤q) = s≤s (view-j≤view-k⇒j≤k v w p≤q)
+
+punchIn-cancel≤ : ∀ {n} (i : Fin (suc n)) {j k} →
+                  (punchIn i j ≤ punchIn i k) → j ≤ k
+punchIn-cancel≤ i {j} {k} = view-j≤view-k⇒j≤k (view i j) (view i k)
+
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
new file mode 100644
index 0000000000..25f5419b19
--- /dev/null
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -0,0 +1,76 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The 'punchOut view' of the function `punchOut` defined on finite sets
+------------------------------------------------------------------------
+
+-- This example of a "view of a function via its graph relation" is inspired
+-- by Nathan van Doorn's recent PR#1913.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Relation.Ternary.PunchOut where
+
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchOut)
+open import Data.Fin.Properties using (suc-injective)
+open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
+
+------------------------------------------------------------------------
+-- The View, considered as a ternary relation
+
+data View : ∀ {n} (i j : Fin (suc n)) (k : Fin n) → Set where
+
+  zero-suc : ∀ {n} (j : Fin n)                   → View zero (suc j) j
+  suc-zero : ∀ {n} (i : Fin (suc n))             → View (suc i) zero zero
+  suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
+
+-- The View enforces the precondition given by a Domain predicate
+
+Domain : ∀ {n} (i j : Fin (suc n)) → Set
+Domain i j = i ≢ j
+
+view-domain : ∀ {n} {i j} {k} → View {n} i j k → Domain i j
+view-domain (suc-suc v) = (view-domain v) ∘ suc-injective
+
+-- The View is sound, ie covers all telescopes satisfying that precondition
+
+view : ∀ {n} {i j} (d : Domain i j) → View {n} i j (punchOut d)
+view             {i = zero}  {j = zero}  d with () ← d refl
+view             {i = zero}  {j = suc j} d = zero-suc j
+view {n = suc _} {i = suc i} {j = zero}  d = suc-zero i
+view {n = suc _} {i = suc i} {j = suc j} d = suc-suc (view (d ∘ (cong suc)))
+
+-- The View is complete
+
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → k ≡ punchOut (view-domain v)
+view-complete (zero-suc j) = refl
+view-complete (suc-zero i) = refl
+view-complete (suc-suc v)  = cong suc (view-complete v)
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+{- punchOut-mono≤ -}
+j≤k⇒view-j≤view-k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+                     j ≤ k → p ≤ q
+j≤k⇒view-j≤view-k (zero-suc j) (zero-suc k)  (s≤s j≤k) = j≤k
+j≤k⇒view-j≤view-k (suc-zero i) _             _         = z≤n
+j≤k⇒view-j≤view-k (suc-suc vj) (suc-suc vk)  (s≤s j≤k) = s≤s (j≤k⇒view-j≤view-k vj vk j≤k)
+
+punchOut-mono≤ : ∀ {n} {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                 j ≤ k → punchOut i≢j ≤ punchOut i≢k
+punchOut-mono≤ i≢j i≢k = j≤k⇒view-j≤view-k (view i≢j) (view i≢k)
+
+{- punchOut-cancel≤ -}
+view-j≤view-k⇒j≤k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+                     p ≤ q → j ≤ k
+view-j≤view-k⇒j≤k (zero-suc j) (zero-suc k)  p≤q       = s≤s p≤q
+view-j≤view-k⇒j≤k (suc-zero i) _             _         = z≤n
+view-j≤view-k⇒j≤k (suc-suc vj) (suc-suc vk)  (s≤s p≤q) = s≤s (view-j≤view-k⇒j≤k vj vk p≤q)
+
+punchOut-cancel≤ : ∀ {n} {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                   (p≤q : punchOut i≢j ≤ punchOut i≢k) →  j ≤ k
+punchOut-cancel≤ i≢j i≢k = view-j≤view-k⇒j≤k (view i≢j) (view i≢k)
+

From b9052e2048435631c91ce9ab8ef2cc2ea6c64fdb Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 7 Feb 2023 23:43:23 +0000
Subject: [PATCH 2/9] tidied up comments

---
 src/Data/Fin/Relation/Ternary/Pinch.agda    | 2 +-
 src/Data/Fin/Relation/Ternary/PunchIn.agda  | 2 +-
 src/Data/Fin/Relation/Ternary/PunchOut.agda | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
index 4a423acba7..4b524af2ab 100644
--- a/src/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The 'punchOut view' of the function `punchOut` defined on finite sets
+-- The '`Pinch` view' of the function `pinch` defined on finite sets
 ------------------------------------------------------------------------
 
 -- This example of a "view of a function via its graph relation" is inspired
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index f45aa1657d..768c50662a 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The 'punchOut view' of the function `punchOut` defined on finite sets
+-- The '`PunchIn` view' of the function `punchIn` defined on finite sets
 ------------------------------------------------------------------------
 
 -- This example of a "view of a function via its graph relation" is inspired
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
index 25f5419b19..4f65b0dda2 100644
--- a/src/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The 'punchOut view' of the function `punchOut` defined on finite sets
+-- The '`PunchOut` view' of the function `punchOut` defined on finite sets
 ------------------------------------------------------------------------
 
 -- This example of a "view of a function via its graph relation" is inspired

From 2d8cbbb2c570cafc4ef67e475261ad92543ad750 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 11 Feb 2023 07:46:42 +0000
Subject: [PATCH 3/9] refactored into view, plus `README` illustrative examples

---
 README/Data/Fin/Relation/Ternary/PunchIn.agda | 44 ++++++++++++++
 src/Data/Fin/Relation/Ternary/PunchIn.agda    | 57 ++++++++++---------
 2 files changed, 74 insertions(+), 27 deletions(-)
 create mode 100644 README/Data/Fin/Relation/Ternary/PunchIn.agda

diff --git a/README/Data/Fin/Relation/Ternary/PunchIn.agda b/README/Data/Fin/Relation/Ternary/PunchIn.agda
new file mode 100644
index 0000000000..f7ca1ecf71
--- /dev/null
+++ b/README/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -0,0 +1,44 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'PunchIn' view of Fin
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored inthe ocnstructors of the view type
+--
+-- Using this view, we can exhibit the corresponding properties of the function
+-- deifned in `Data.Fin.Properties`
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module README.Data.Fin.Relation.Ternary.PunchInView where
+
+open import Data.Nat.Base using (ℕ; suc)
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn)
+open import Data.Fin.Relation.Ternary.PunchIn
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i
+punchInᵢ≢i i j = view-codomain (view i j)
+
+punchIn-injective : ∀ i (j k : Fin n) →
+                    punchIn i j ≡ punchIn i k → j ≡ k
+punchIn-injective i j k = view-injective (view i j) (view i k)
+
+punchIn-mono≤ : ∀ (i : Fin (suc n)) {j k} →
+                j ≤ k → punchIn i j ≤ punchIn i k
+punchIn-mono≤ i {j} {k} = view-mono-≤ (view i j) (view i k)
+
+punchIn-cancel≤ : ∀ (i : Fin (suc n)) {j k} →
+                  (punchIn i j ≤ punchIn i k) → j ≤ k
+punchIn-cancel≤ i {j} {k} = view-cancel-≤ (view i j) (view i k)
+
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index 768c50662a..ec192e1e9f 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -17,6 +17,11 @@ open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
 open import Function.Base using (id; _∘_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 
+private
+  variable
+    n : ℕ
+
+
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
@@ -28,48 +33,46 @@ data View : ∀ {n} (i : Fin (suc n)) (j : Fin n) (k : Fin (suc n)) → Set wher
 
 -- The View enforces the codomain postcondition
 
-Codomain : ∀ {n} (i : Fin (suc n)) (j : Fin n) → Set
+Codomain : ∀ (i : Fin (suc n)) (j : Fin n) → Set
 Codomain i j = punchIn i j ≢ i
 
-view-codomain : ∀ {n} {i} {j} {k} → View {n} i j k → Codomain i j
+view-codomain : ∀ {i} {j} {k} → View {n} i j k → Codomain i j
 view-codomain (suc-suc v) = (view-codomain v) ∘ suc-injective
 
 -- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
 
-view : ∀ {n} i j → View {n} i j (punchIn i j)
+view : ∀ i j → View {n} i j (punchIn i j)
 view zero         j  = zero-suc j
 view (suc i) zero    = suc-zero i
 view (suc i) (suc j) = suc-suc (view i j)
 
 -- The View is complete
 
-view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → k ≡ punchIn i j
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → k ≡ punchIn i j
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
 
 ------------------------------------------------------------------------
--- Properties of the function, derived from properties of the View
-
-{- punchIn-mono≤ -}
-j≤k⇒view-j≤view-k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
-                     j ≤ k → p ≤ q
-j≤k⇒view-j≤view-k (zero-suc _) (zero-suc _)  j≤k     = s≤s j≤k
-j≤k⇒view-j≤view-k (suc-zero i) _             _       = z≤n
-j≤k⇒view-j≤view-k (suc-suc v)  (suc-suc w) (s≤s j≤k) = s≤s (j≤k⇒view-j≤view-k v w j≤k)
-
-punchIn-mono≤ : ∀ {n} (i : Fin (suc n)) {j k} →
-                j ≤ k → punchIn i j ≤ punchIn i k
-punchIn-mono≤ i {j} {k} = j≤k⇒view-j≤view-k (view i j) (view i k)
-
-{- punchIn-cancel≤ -}
-view-j≤view-k⇒j≤k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
-                     p ≤ q → j ≤ k
-view-j≤view-k⇒j≤k (zero-suc _) (zero-suc _) (s≤s p≤q) = p≤q
-view-j≤view-k⇒j≤k (suc-zero i) _            _         = z≤n
-view-j≤view-k⇒j≤k (suc-suc v)  (suc-suc w)  (s≤s p≤q) = s≤s (view-j≤view-k⇒j≤k v w p≤q)
-
-punchIn-cancel≤ : ∀ {n} (i : Fin (suc n)) {j k} →
-                  (punchIn i j ≤ punchIn i k) → j ≤ k
-punchIn-cancel≤ i {j} {k} = view-j≤view-k⇒j≤k (view i j) (view i k)
+-- Properties of the View
+
+view-injective : ∀ {i j k} {p q} →
+                 View {n} i j p → View {n} i k q → p ≡ q → j ≡ k
+view-injective v w refl = aux v w where
+  aux : ∀ {i j k} {r} → View {n} i j r → View {n} i k r → j ≡ k
+  aux (zero-suc _) (zero-suc _) = refl
+  aux (suc-zero i) (suc-zero i) = refl
+  aux (suc-suc v) (suc-suc w)   = cong suc (aux v w)
+
+view-mono-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+              j ≤ k → p ≤ q
+view-mono-≤ (zero-suc _) (zero-suc _)  j≤k     = s≤s j≤k
+view-mono-≤ (suc-zero i) _             _       = z≤n
+view-mono-≤ (suc-suc v)  (suc-suc w) (s≤s j≤k) = s≤s (view-mono-≤ v w j≤k)
+
+view-cancel-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                p ≤ q → j ≤ k
+view-cancel-≤ (zero-suc _) (zero-suc _) (s≤s p≤q) = p≤q
+view-cancel-≤ (suc-zero i) _            _         = z≤n
+view-cancel-≤ (suc-suc v)  (suc-suc w)  (s≤s p≤q) = s≤s (view-cancel-≤ v w p≤q)
 

From 1dafbf4324a626cd63bb3fbc93cab6b7d400614a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 11 Feb 2023 07:50:03 +0000
Subject: [PATCH 4/9] typos

---
 README/Data/Fin/Relation/Ternary/PunchIn.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README/Data/Fin/Relation/Ternary/PunchIn.agda b/README/Data/Fin/Relation/Ternary/PunchIn.agda
index f7ca1ecf71..a00856351b 100644
--- a/README/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/README/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -5,15 +5,15 @@
 --
 -- This is an example of a view of a function defined over a datatype,
 -- such that the recursion and call-pattern(s) of the function are
--- precisely mirrored inthe ocnstructors of the view type
+-- precisely mirrored in the constructors of the view type
 --
 -- Using this view, we can exhibit the corresponding properties of the function
--- deifned in `Data.Fin.Properties`
+-- defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module README.Data.Fin.Relation.Ternary.PunchInView where
+module README.Data.Fin.Relation.Ternary.PunchIn where
 
 open import Data.Nat.Base using (ℕ; suc)
 open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn)

From 9b9c7b6777d7938935ea37d0e8591236fab1b5e2 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 11 Feb 2023 08:00:34 +0000
Subject: [PATCH 5/9] reworked comments

---
 README/Data/Fin/Relation/Ternary/PunchIn.agda |  4 +-
 src/Data/Fin/Relation/Ternary/Pinch.agda      |  8 ++--
 src/Data/Fin/Relation/Ternary/PunchIn.agda    |  8 ++--
 src/Data/Fin/Relation/Ternary/PunchOut.agda   | 47 +++++++++----------
 4 files changed, 33 insertions(+), 34 deletions(-)

diff --git a/README/Data/Fin/Relation/Ternary/PunchIn.agda b/README/Data/Fin/Relation/Ternary/PunchIn.agda
index a00856351b..0ac1aecaa9 100644
--- a/README/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/README/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -7,8 +7,8 @@
 -- such that the recursion and call-pattern(s) of the function are
 -- precisely mirrored in the constructors of the view type
 --
--- Using this view, we can exhibit the corresponding properties of the function
--- defined in `Data.Fin.Properties`
+-- Using this view, we can exhibit the corresponding properties of
+-- the function `punchIn` defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
index 4b524af2ab..9fa7fd7f1f 100644
--- a/src/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -3,9 +3,11 @@
 --
 -- The '`Pinch` view' of the function `pinch` defined on finite sets
 ------------------------------------------------------------------------
-
--- This example of a "view of a function via its graph relation" is inspired
--- by Nathan van Doorn's recent PR#1913.
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type,
+-- ie that we 'view the function via its graph relation'
 
 {-# OPTIONS --without-K --safe #-}
 
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index ec192e1e9f..6301792cbe 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -3,9 +3,11 @@
 --
 -- The '`PunchIn` view' of the function `punchIn` defined on finite sets
 ------------------------------------------------------------------------
-
--- This example of a "view of a function via its graph relation" is inspired
--- by Nathan van Doorn's recent PR#1913.
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type,
+-- ie that we 'view the function via its graph relation'
 
 {-# OPTIONS --without-K --safe #-}
 
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
index 4f65b0dda2..42ad2741d5 100644
--- a/src/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -1,10 +1,10 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The '`PunchOut` view' of the function `punchOut` defined on finite sets
+-- The '`PunchOut` view of the function `punchOut` defined on finite sets
 ------------------------------------------------------------------------
 
--- This example of a "view of a function via its graph relation" is inspired
+-- This example of a 'view of a function via its graph relation' is inspired
 -- by Nathan van Doorn's recent PR#1913.
 
 {-# OPTIONS --without-K --safe #-}
@@ -17,6 +17,11 @@ open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 
+private
+  variable
+    n : ℕ
+
+
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
@@ -28,10 +33,10 @@ data View : ∀ {n} (i j : Fin (suc n)) (k : Fin n) → Set where
 
 -- The View enforces the precondition given by a Domain predicate
 
-Domain : ∀ {n} (i j : Fin (suc n)) → Set
+Domain : ∀ (i j : Fin (suc n)) → Set
 Domain i j = i ≢ j
 
-view-domain : ∀ {n} {i j} {k} → View {n} i j k → Domain i j
+view-domain : ∀ {i j} {k} → View {n} i j k → Domain i j
 view-domain (suc-suc v) = (view-domain v) ∘ suc-injective
 
 -- The View is sound, ie covers all telescopes satisfying that precondition
@@ -44,7 +49,7 @@ view {n = suc _} {i = suc i} {j = suc j} d = suc-suc (view (d ∘ (cong suc)))
 
 -- The View is complete
 
-view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → k ≡ punchOut (view-domain v)
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → k ≡ punchOut (view-domain v)
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
@@ -52,25 +57,15 @@ view-complete (suc-suc v)  = cong suc (view-complete v)
 ------------------------------------------------------------------------
 -- Properties of the function, derived from properties of the View
 
-{- punchOut-mono≤ -}
-j≤k⇒view-j≤view-k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
-                     j ≤ k → p ≤ q
-j≤k⇒view-j≤view-k (zero-suc j) (zero-suc k)  (s≤s j≤k) = j≤k
-j≤k⇒view-j≤view-k (suc-zero i) _             _         = z≤n
-j≤k⇒view-j≤view-k (suc-suc vj) (suc-suc vk)  (s≤s j≤k) = s≤s (j≤k⇒view-j≤view-k vj vk j≤k)
-
-punchOut-mono≤ : ∀ {n} {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
-                 j ≤ k → punchOut i≢j ≤ punchOut i≢k
-punchOut-mono≤ i≢j i≢k = j≤k⇒view-j≤view-k (view i≢j) (view i≢k)
-
-{- punchOut-cancel≤ -}
-view-j≤view-k⇒j≤k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
-                     p ≤ q → j ≤ k
-view-j≤view-k⇒j≤k (zero-suc j) (zero-suc k)  p≤q       = s≤s p≤q
-view-j≤view-k⇒j≤k (suc-zero i) _             _         = z≤n
-view-j≤view-k⇒j≤k (suc-suc vj) (suc-suc vk)  (s≤s p≤q) = s≤s (view-j≤view-k⇒j≤k vj vk p≤q)
-
-punchOut-cancel≤ : ∀ {n} {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
-                   (p≤q : punchOut i≢j ≤ punchOut i≢k) →  j ≤ k
-punchOut-cancel≤ i≢j i≢k = view-j≤view-k⇒j≤k (view i≢j) (view i≢k)
+view-mono-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+              j ≤ k → p ≤ q
+view-mono-≤ (zero-suc j) (zero-suc k)  (s≤s j≤k) = j≤k
+view-mono-≤ (suc-zero i) _             _         = z≤n
+view-mono-≤ (suc-suc vj) (suc-suc vk)  (s≤s j≤k) = s≤s (view-mono-≤ vj vk j≤k)
+
+view-cancel-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                p ≤ q → j ≤ k
+view-cancel-≤ (zero-suc j) (zero-suc k)  p≤q       = s≤s p≤q
+view-cancel-≤ (suc-zero i) _             _         = z≤n
+view-cancel-≤ (suc-suc vj) (suc-suc vk)  (s≤s p≤q) = s≤s (view-cancel-≤ vj vk p≤q)
 

From 9c15e24b9e2790504e32950e88d1ce8764f0e99e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 11 Feb 2023 10:30:31 +0000
Subject: [PATCH 6/9] extensive refactoring; converse/inverse properties

---
 README/Data/Fin/Relation/Ternary/Pinch.agda   | 53 ++++++++++++
 README/Data/Fin/Relation/Ternary/PunchIn.agda | 16 ++--
 .../Data/Fin/Relation/Ternary/PunchOut.agda   | 59 +++++++++++++
 src/Data/Fin/Relation/Ternary/Pinch.agda      | 84 ++++++++++---------
 src/Data/Fin/Relation/Ternary/PunchIn.agda    |  2 +-
 src/Data/Fin/Relation/Ternary/PunchOut.agda   | 38 ++++++++-
 6 files changed, 201 insertions(+), 51 deletions(-)
 create mode 100644 README/Data/Fin/Relation/Ternary/Pinch.agda
 create mode 100644 README/Data/Fin/Relation/Ternary/PunchOut.agda

diff --git a/README/Data/Fin/Relation/Ternary/Pinch.agda b/README/Data/Fin/Relation/Ternary/Pinch.agda
new file mode 100644
index 0000000000..01ccb07826
--- /dev/null
+++ b/README/Data/Fin/Relation/Ternary/Pinch.agda
@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'Pinch' view of Fin
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type
+--
+-- Using this view, we can exhibit the corresponding properties of
+-- the function `punchIn` defined in `Data.Fin.Properties`
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module README.Data.Fin.Relation.Ternary.Pinch where
+
+open import Data.Nat.Base as Nat using (ℕ; suc; ∣_-_∣)
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; _≤_; _<_; pinch)
+open import Data.Fin.Relation.Ternary.Pinch
+open import Data.Product using (_,_; ∃)
+open import Function.Definitions.Core2 using (Surjective)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+pinch-surjective : ∀ (i : Fin n) → Surjective _≡_ (pinch i)
+pinch-surjective i k
+  with j , v ← view-surjective i k
+  with refl ← view-complete v = j , refl
+
+pinch-injective : ∀ {i : Fin n} {j k : Fin (ℕ.suc n)} →
+                  suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k
+pinch-injective {n = n} {i} {j} {k} = view-injective (view i j) (view i k)
+
+pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
+pinch-mono-≤ i {j} {k} = view-mono-≤ (view i j) (view i k)
+
+pinch-cancel-< : ∀ (i : Fin (suc n)) {j k} →
+                (pinch i j < pinch i k) → j < k
+pinch-cancel-< i {j} {k} = view-cancel-< (view i j) (view i k)
+
+pinch-≡⇒∣j-k∣≤1 : ∀ (i : Fin n) {j k} →
+                  (pinch i j ≡ pinch i k) → ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
+pinch-≡⇒∣j-k∣≤1 i {j} {k} = view-j≡view-k⇒∣j-k∣≤1 (view i j) (view i k)
+
diff --git a/README/Data/Fin/Relation/Ternary/PunchIn.agda b/README/Data/Fin/Relation/Ternary/PunchIn.agda
index 0ac1aecaa9..d538abcba3 100644
--- a/README/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/README/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -18,6 +18,8 @@ module README.Data.Fin.Relation.Ternary.PunchIn where
 open import Data.Nat.Base using (ℕ; suc)
 open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn)
 open import Data.Fin.Relation.Ternary.PunchIn
+open import Function.Definitions using (Injective)
+open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
 
 private
@@ -30,15 +32,13 @@ private
 punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i
 punchInᵢ≢i i j = view-codomain (view i j)
 
-punchIn-injective : ∀ i (j k : Fin n) →
-                    punchIn i j ≡ punchIn i k → j ≡ k
-punchIn-injective i j k = view-injective (view i j) (view i k)
+punchIn-injective : ∀ (i : Fin (suc n)) → Injective _≡_ _≡_ (punchIn i)
+punchIn-injective i {j} {k} = view-injective (view i j) (view i k)
 
-punchIn-mono≤ : ∀ (i : Fin (suc n)) {j k} →
-                j ≤ k → punchIn i j ≤ punchIn i k
-punchIn-mono≤ i {j} {k} = view-mono-≤ (view i j) (view i k)
+punchIn-mono-≤ : ∀ (i : Fin (suc n)) → (punchIn i) Preserves _≤_ ⟶ _≤_
+punchIn-mono-≤ i {j} {k} = view-mono-≤ (view i j) (view i k)
 
-punchIn-cancel≤ : ∀ (i : Fin (suc n)) {j k} →
+punchIn-cancel-≤ : ∀ (i : Fin (suc n)) {j k} →
                   (punchIn i j ≤ punchIn i k) → j ≤ k
-punchIn-cancel≤ i {j} {k} = view-cancel-≤ (view i j) (view i k)
+punchIn-cancel-≤ i {j} {k} = view-cancel-≤ (view i j) (view i k)
 
diff --git a/README/Data/Fin/Relation/Ternary/PunchOut.agda b/README/Data/Fin/Relation/Ternary/PunchOut.agda
new file mode 100644
index 0000000000..e8f30df7a2
--- /dev/null
+++ b/README/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'PunchOut' view of Fin
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type
+--
+-- Using this view, we can exhibit the corresponding properties of
+-- the function `punchIn` defined in `Data.Fin.Properties`
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module README.Data.Fin.Relation.Ternary.PunchOut where
+
+open import Data.Nat.Base using (ℕ; suc)
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn; punchOut)
+open import Data.Fin.Properties using (punchInᵢ≢i)
+open import Data.Fin.Relation.Ternary.PunchIn as PunchIn using ()
+open import Data.Fin.Relation.Ternary.PunchOut
+open import Function.Base using (_∘_)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; sym)
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+punchOut-injective : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                    punchOut i≢j ≡ punchOut i≢k → j ≡ k
+punchOut-injective i≢j i≢k = view-injective (view i≢j) (view i≢k)
+
+punchOut-cong : ∀ (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
+                j ≡ k → punchOut i≢j ≡ punchOut i≢k
+punchOut-cong i {i≢j = i≢j} {i≢k = i≢k} = view-cong (view i≢j) (view i≢k)
+
+punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                j ≤ k → punchOut i≢j ≤ punchOut i≢k
+punchOut-mono-≤ i≢j i≢k = view-mono-≤ (view i≢j) (view i≢k)
+
+punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                  (punchOut i≢j ≤ punchOut i≢k) → j ≤ k
+punchOut-cancel-≤ i≢j i≢k = view-cancel-≤ (view i≢j) (view i≢k)
+
+-- punchOut and punchIn are mutual inverses,
+-- because their corresponding View s are converses
+
+punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
+                   punchIn i (punchOut i≢j) ≡ j
+punchIn-punchOut = PunchIn.view-complete ∘ view-view⁻¹ ∘ view
+
+punchOut-punchIn : ∀ i {j : Fin n} →
+                   punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
+punchOut-punchIn i {j} = view-complete (view⁻¹-view (PunchIn.view i j))
diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
index 9fa7fd7f1f..4d7b92dbfb 100644
--- a/src/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -17,9 +17,15 @@ open import Data.Fin.Base using (Fin; zero; suc; toℕ; _≤_; _<_; pinch)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; ∣_-_∣)
 open import Data.Nat.Properties using (≤-refl; <⇒≤; ∣n-n∣≡0)
+open import Data.Product using (_,_; ∃)
 open import Function.Base using (id; _∘_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 
+private
+  variable
+    n : ℕ
+
+
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
@@ -38,7 +44,7 @@ view   (suc i) (suc j) = suc-suc (view i j)
 
 -- The View is complete
 
-view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → k ≡ pinch i j
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → pinch i j ≡ k
 view-complete (any-zero i) = refl
 view-complete (zero-suc j) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
@@ -46,43 +52,45 @@ view-complete (suc-suc v)  = cong suc (view-complete v)
 ------------------------------------------------------------------------
 -- Properties of the function, derived from properties of the View
 
-{- pinch-mono≤ -}
-j≤k⇒view-j≤view-k : ∀ {n} {i} {j k} {p q} → View {n} i j p → View {n} i k q →
-                     j ≤ k → p ≤ q
-j≤k⇒view-j≤view-k (any-zero _) _            _         = z≤n
-j≤k⇒view-j≤view-k (zero-suc _) (zero-suc _) (s≤s j≤k) = j≤k
-j≤k⇒view-j≤view-k (suc-suc v)  (suc-suc w)  (s≤s j≤k) = s≤s (j≤k⇒view-j≤view-k v w j≤k)
-
-pinch-mono≤ : ∀ {n} (i : Fin n) {j k} →
-                j ≤ k → pinch i j ≤ pinch i k
-pinch-mono≤ i {j} {k} = j≤k⇒view-j≤view-k (view i j) (view i k)
-
-{- pinch-cancel< -}
-view-j<view-k⇒j<k : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
-                     p < q → j < k
-view-j<view-k⇒j<k (any-zero _) (zero-suc _) _         = z<s
-view-j<view-k⇒j<k (any-zero _) (suc-suc _)  _         = z<s
-view-j<view-k⇒j<k (zero-suc _) (zero-suc _) p<q       = s<s p<q
-view-j<view-k⇒j<k (suc-suc v)  (suc-suc w)  (s<s p<q) = s<s (view-j<view-k⇒j<k v w p<q)
-
-pinch-cancel< : ∀ {n} (i : Fin (suc n)) {j k} →
-                  (pinch i j < pinch i k) → j < k
-pinch-cancel< i {j} {k} = view-j<view-k⇒j<k (view i j) (view i k)
-
-{- pinch-cancel≡ -}
-view-j≡view-k⇒∣j-k∣≤1 : ∀ {n} {i j k} {p q} → View {n} i j p → View {n} i k q →
+view-surjective : ∀ (i k : Fin n) → ∃ λ j → View i j k
+view-surjective zero    k       = suc k , zero-suc k
+view-surjective (suc i) zero    = zero , any-zero (suc i)
+view-surjective (suc i) (suc k) with j , v ← view-surjective i k = suc j , suc-suc v
+
+view-injective : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                 suc i ≢ j → suc i ≢ k → p ≡ q → j ≡ k
+view-injective v w [i+1]≢j [i+1]≢k refl = aux v w [i+1]≢j [i+1]≢k where
+  aux : ∀ {i j k} {r} → View {n} i j r → View {n} i k r →
+        suc i ≢ j → suc i ≢ k → j ≡ k
+  aux (any-zero _) (any-zero _)     [i+1]≢j [i+1]≢k = refl
+  aux (any-zero _) (zero-suc .zero) [i+1]≢j [i+1]≢k with () ← [i+1]≢k refl
+  aux (zero-suc _) (any-zero .zero) [i+1]≢j [i+1]≢k with () ← [i+1]≢j refl
+  aux (zero-suc _) (zero-suc _)     [i+1]≢j [i+1]≢k = refl
+  aux (suc-suc v)  (suc-suc w)      [i+1]≢j [i+1]≢k
+    = cong suc (aux v w ([i+1]≢j ∘ cong suc) ([i+1]≢k ∘ cong suc))
+
+view-mono-≤ : ∀ {i} {j k} {p q} → View {n} i j p → View {n} i k q →
+              j ≤ k → p ≤ q
+view-mono-≤ (any-zero _) _            _         = z≤n
+view-mono-≤ (zero-suc _) (zero-suc _) (s≤s j≤k) = j≤k
+view-mono-≤ (suc-suc v)  (suc-suc w)  (s≤s j≤k) = s≤s (view-mono-≤ v w j≤k)
+
+view-cancel-< : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                p < q → j < k
+view-cancel-< (any-zero _) (zero-suc _) _         = z<s
+view-cancel-< (any-zero _) (suc-suc _)  _         = z<s
+view-cancel-< (zero-suc _) (zero-suc _) p<q       = s<s p<q
+view-cancel-< (suc-suc v)  (suc-suc w)  (s<s p<q) = s<s (view-cancel-< v w p<q)
+
+view-j≡view-k⇒∣j-k∣≤1 : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
                         p ≡ q → ∣ (toℕ j) - (toℕ k)∣ Nat.≤ 1
-view-j≡view-k⇒∣j-k∣≤1 v w refl = helper v w
+view-j≡view-k⇒∣j-k∣≤1 v w refl = aux v w
   where
-    helper : ∀ {n} {i j k} {r} → View {n} i j r → View {n} i k r →
-             ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
-    helper (any-zero _)    (any-zero _)    = z≤n
-    helper (any-zero zero) (zero-suc zero) = ≤-refl
-    helper (zero-suc zero) (any-zero zero) = ≤-refl
-    helper (zero-suc j)    (zero-suc j) rewrite ∣n-n∣≡0 (toℕ j) = z≤n
-    helper (suc-suc v)     (suc-suc w) = helper v w
-
-pinch-cancel≡ : ∀ {n} (i : Fin n) {j k} →
-                (pinch i j ≡ pinch i k) → ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
-pinch-cancel≡ i {j} {k} = view-j≡view-k⇒∣j-k∣≤1 (view i j) (view i k)
+    aux : ∀ {n} {i j k} {r} → View {n} i j r → View {n} i k r →
+          ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
+    aux (any-zero _)    (any-zero _)    = z≤n
+    aux (any-zero zero) (zero-suc zero) = ≤-refl
+    aux (zero-suc zero) (any-zero zero) = ≤-refl
+    aux (zero-suc j)    (zero-suc j) rewrite ∣n-n∣≡0 (toℕ j) = z≤n
+    aux (suc-suc v)     (suc-suc w) = aux v w
 
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index 6301792cbe..937c40e3a9 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -50,7 +50,7 @@ view (suc i) (suc j) = suc-suc (view i j)
 
 -- The View is complete
 
-view-complete : ∀ {i j} {k} (v : View {n} i j k) → k ≡ punchIn i j
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → punchIn i j ≡ k
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
index 42ad2741d5..858ac49e5e 100644
--- a/src/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -3,9 +3,11 @@
 --
 -- The '`PunchOut` view of the function `punchOut` defined on finite sets
 ------------------------------------------------------------------------
-
--- This example of a 'view of a function via its graph relation' is inspired
--- by Nathan van Doorn's recent PR#1913.
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type,
+-- ie that we 'view the function via its graph relation'
 
 {-# OPTIONS --without-K --safe #-}
 
@@ -13,6 +15,7 @@ module Data.Fin.Relation.Ternary.PunchOut where
 
 open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchOut)
 open import Data.Fin.Properties using (suc-injective)
+open import Data.Fin.Relation.Ternary.PunchIn as PunchIn using ()
 open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
@@ -49,7 +52,7 @@ view {n = suc _} {i = suc i} {j = suc j} d = suc-suc (view (d ∘ (cong suc)))
 
 -- The View is complete
 
-view-complete : ∀ {i j} {k} (v : View {n} i j k) → k ≡ punchOut (view-domain v)
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → punchOut (view-domain v) ≡ k
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
@@ -57,6 +60,22 @@ view-complete (suc-suc v)  = cong suc (view-complete v)
 ------------------------------------------------------------------------
 -- Properties of the function, derived from properties of the View
 
+view-cong : ∀ {i j k} {p q} →
+                 View {n} i j p → View {n} i k q → j ≡ k → p ≡ q
+view-cong v w refl = aux v w where
+  aux : ∀ {i j} {p q} → View {n} i j p → View {n} i j q → p ≡ q
+  aux (zero-suc _) (zero-suc _) = refl
+  aux (suc-zero i) (suc-zero i) = refl
+  aux (suc-suc v)  (suc-suc w)  = cong suc (aux v w)
+
+view-injective : ∀ {i j k} {p q} →
+                 View {n} i j p → View {n} i k q → p ≡ q → j ≡ k
+view-injective v w refl = aux v w where
+  aux : ∀ {i j k} {r} → View {n} i j r → View {n} i k r → j ≡ k
+  aux (zero-suc _) (zero-suc _) = refl
+  aux (suc-zero i) (suc-zero i) = refl
+  aux (suc-suc v)  (suc-suc w)  = cong suc (aux v w)
+
 view-mono-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
               j ≤ k → p ≤ q
 view-mono-≤ (zero-suc j) (zero-suc k)  (s≤s j≤k) = j≤k
@@ -69,3 +88,14 @@ view-cancel-≤ (zero-suc j) (zero-suc k)  p≤q       = s≤s p≤q
 view-cancel-≤ (suc-zero i) _             _         = z≤n
 view-cancel-≤ (suc-suc vj) (suc-suc vk)  (s≤s p≤q) = s≤s (view-cancel-≤ vj vk p≤q)
 
+-- PunchOut.View and PunchIn.View are mutual converses
+
+view-view⁻¹ : ∀ {i j} {k} → View {n} i j k → PunchIn.View {n} i k j
+view-view⁻¹ (zero-suc _) = PunchIn.zero-suc _
+view-view⁻¹ (suc-zero i) = PunchIn.suc-zero i
+view-view⁻¹ (suc-suc v)  = PunchIn.suc-suc (view-view⁻¹ v)
+
+view⁻¹-view : ∀ {i j} {k} → PunchIn.View {n} i k j → View {n} i j k
+view⁻¹-view (PunchIn.zero-suc _) = zero-suc _
+view⁻¹-view (PunchIn.suc-zero i) = suc-zero i
+view⁻¹-view (PunchIn.suc-suc v)  = suc-suc (view⁻¹-view v)

From 6e1fb643443286e2668f31159b49788e21a79018 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 11 Feb 2023 11:10:43 +0000
Subject: [PATCH 7/9] added inthe interpretation functions

---
 README/Data/Fin/Relation/Ternary/PunchOut.agda |  2 +-
 src/Data/Fin/Relation/Ternary/Pinch.agda       | 15 ++++++++++++++-
 src/Data/Fin/Relation/Ternary/PunchIn.agda     | 15 ++++++++++++++-
 src/Data/Fin/Relation/Ternary/PunchOut.agda    | 15 ++++++++++++++-
 4 files changed, 43 insertions(+), 4 deletions(-)

diff --git a/README/Data/Fin/Relation/Ternary/PunchOut.agda b/README/Data/Fin/Relation/Ternary/PunchOut.agda
index e8f30df7a2..aebc9e4a83 100644
--- a/README/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/README/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -8,7 +8,7 @@
 -- precisely mirrored in the constructors of the view type
 --
 -- Using this view, we can exhibit the corresponding properties of
--- the function `punchIn` defined in `Data.Fin.Properties`
+-- the function `punchOut` defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
index 4d7b92dbfb..f7546cc867 100644
--- a/src/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -29,6 +29,9 @@ private
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
 data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
 
   any-zero : ∀ {n} (i : Fin (suc n))             → View i zero zero
@@ -37,14 +40,24 @@ data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
 
 -- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
 
+-- The recursion/pattern analysis of the original definition of `pinch`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
 view : ∀ {n} i j → View {n} i j (pinch i j)
 view {suc _} i zero    = any-zero i
 view   zero    (suc j) = zero-suc j
 view   (suc i) (suc j) = suc-suc (view i j)
 
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i j} {k} .(v : View {n} i j k) → Fin n
+⟦_⟧ {n = n} {i} {j} {k} _ = pinch i j
+
 -- The View is complete
 
-view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → pinch i j ≡ k
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
 view-complete (any-zero i) = refl
 view-complete (zero-suc j) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index 937c40e3a9..d4d709aa4d 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -27,6 +27,9 @@ private
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
 data View : ∀ {n} (i : Fin (suc n)) (j : Fin n) (k : Fin (suc n)) → Set where
 
   zero-suc : ∀ {n} (j : Fin n)                   → View zero j (suc j)
@@ -43,14 +46,24 @@ view-codomain (suc-suc v) = (view-codomain v) ∘ suc-injective
 
 -- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
 
+-- The recursion/pattern analysis of the original definition of `punchIn`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
 view : ∀ i j → View {n} i j (punchIn i j)
 view zero         j  = zero-suc j
 view (suc i) zero    = suc-zero i
 view (suc i) (suc j) = suc-suc (view i j)
 
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i} {j} {k} .(v : View {n} i j k) → Fin (suc n)
+⟦_⟧ {n = n} {i} {j} {k} _ = punchIn i j
+
 -- The View is complete
 
-view-complete : ∀ {i j} {k} (v : View {n} i j k) → punchIn i j ≡ k
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
index 858ac49e5e..2fb1685e97 100644
--- a/src/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -28,6 +28,9 @@ private
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
 data View : ∀ {n} (i j : Fin (suc n)) (k : Fin n) → Set where
 
   zero-suc : ∀ {n} (j : Fin n)                   → View zero (suc j) j
@@ -44,15 +47,25 @@ view-domain (suc-suc v) = (view-domain v) ∘ suc-injective
 
 -- The View is sound, ie covers all telescopes satisfying that precondition
 
+-- The recursion/pattern analysis of the original definition of `punchOut`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
 view : ∀ {n} {i j} (d : Domain i j) → View {n} i j (punchOut d)
 view             {i = zero}  {j = zero}  d with () ← d refl
 view             {i = zero}  {j = suc j} d = zero-suc j
 view {n = suc _} {i = suc i} {j = zero}  d = suc-zero i
 view {n = suc _} {i = suc i} {j = suc j} d = suc-suc (view (d ∘ (cong suc)))
 
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i j} {k} (v : View {n} i j k) → Fin n
+⟦ v ⟧ = punchOut (view-domain v)
+
 -- The View is complete
 
-view-complete : ∀ {i j} {k} (v : View {n} i j k) → punchOut (view-domain v) ≡ k
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)

From 97ce059cb62985dc098654ac6833679311e56e7a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 11 Feb 2023 15:13:40 +0000
Subject: [PATCH 8/9] added original function definitions in comments

---
 src/Data/Fin/Relation/Ternary/Pinch.agda    | 10 ++++++++++
 src/Data/Fin/Relation/Ternary/PunchIn.agda  |  9 +++++++++
 src/Data/Fin/Relation/Ternary/PunchOut.agda | 18 ++++++++++++++----
 3 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
index f7546cc867..2f449d815f 100644
--- a/src/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -33,6 +33,16 @@ private
 -- function definition; recursive calls are represented by inductive premises
 
 data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
+{-
+
+-- `pinch` is 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 {suc n} _       zero    = zero
+pinch {suc n} zero    (suc j) = j
+pinch {suc n} (suc i) (suc j) = suc (pinch i j)
+
+-}
 
   any-zero : ∀ {n} (i : Fin (suc n))             → View i zero zero
   zero-suc : ∀ {n} (j : Fin (suc n))             → View zero (suc j) j
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index d4d709aa4d..2ba4581830 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -31,7 +31,16 @@ private
 -- function definition; recursive calls are represented by inductive premises
 
 data View : ∀ {n} (i : Fin (suc n)) (j : Fin n) (k : Fin (suc n)) → Set where
+{-
 
+-- `punchIn` is the function f(i,j) = if j≥i then j+1 else j
+
+punchIn : Fin (suc n) → Fin n → Fin (suc n)
+punchIn zero    j       = suc j
+punchIn (suc i) zero    = zero
+punchIn (suc i) (suc j) = suc (punchIn i j)
+
+-}
   zero-suc : ∀ {n} (j : Fin n)                   → View zero j (suc j)
   suc-zero : ∀ {n} (i : Fin (suc n))             → View (suc i) zero zero
   suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
index 2fb1685e97..70bf14b1a8 100644
--- a/src/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -32,7 +32,17 @@ private
 -- function definition; recursive calls are represented by inductive premises
 
 data View : ∀ {n} (i j : Fin (suc n)) (k : Fin n) → Set where
+{-
 
+-- `punchOut` is the function f(i,j) = if j>i then j-1 else j
+
+punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n
+punchOut {_}     {zero}   {zero}  i≢j = ⊥-elim (i≢j refl)
+punchOut {_}     {zero}   {suc j} _   = j
+punchOut {suc _} {suc i}  {zero}  _   = zero
+punchOut {suc _} {suc i}  {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))
+
+-}
   zero-suc : ∀ {n} (j : Fin n)                   → View zero (suc j) j
   suc-zero : ∀ {n} (i : Fin (suc n))             → View (suc i) zero zero
   suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
@@ -73,16 +83,16 @@ view-complete (suc-suc v)  = cong suc (view-complete v)
 ------------------------------------------------------------------------
 -- Properties of the function, derived from properties of the View
 
-view-cong : ∀ {i j k} {p q} →
-                 View {n} i j p → View {n} i k q → j ≡ k → p ≡ q
+view-cong : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+            j ≡ k → p ≡ q
 view-cong v w refl = aux v w where
   aux : ∀ {i j} {p q} → View {n} i j p → View {n} i j q → p ≡ q
   aux (zero-suc _) (zero-suc _) = refl
   aux (suc-zero i) (suc-zero i) = refl
   aux (suc-suc v)  (suc-suc w)  = cong suc (aux v w)
 
-view-injective : ∀ {i j k} {p q} →
-                 View {n} i j p → View {n} i k q → p ≡ q → j ≡ k
+view-injective : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                 p ≡ q → j ≡ k
 view-injective v w refl = aux v w where
   aux : ∀ {i j k} {r} → View {n} i j r → View {n} i k r → j ≡ k
   aux (zero-suc _) (zero-suc _) = refl

From 98ca1045b98fc4c62630c5cf3e6ce5862e2c4ece Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 15 May 2023 12:56:56 +0100
Subject: [PATCH 9/9] made `cubical-compatible`

---
 README/Data/Fin/Relation/Ternary/Pinch.agda    | 2 +-
 README/Data/Fin/Relation/Ternary/PunchIn.agda  | 2 +-
 README/Data/Fin/Relation/Ternary/PunchOut.agda | 2 +-
 src/Data/Fin/Relation/Ternary/Pinch.agda       | 2 +-
 src/Data/Fin/Relation/Ternary/PunchIn.agda     | 2 +-
 src/Data/Fin/Relation/Ternary/PunchOut.agda    | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/README/Data/Fin/Relation/Ternary/Pinch.agda b/README/Data/Fin/Relation/Ternary/Pinch.agda
index 01ccb07826..e0d2b9e453 100644
--- a/README/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/README/Data/Fin/Relation/Ternary/Pinch.agda
@@ -11,7 +11,7 @@
 -- the function `punchIn` defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Data.Fin.Relation.Ternary.Pinch where
 
diff --git a/README/Data/Fin/Relation/Ternary/PunchIn.agda b/README/Data/Fin/Relation/Ternary/PunchIn.agda
index d538abcba3..ae04b2774b 100644
--- a/README/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/README/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -11,7 +11,7 @@
 -- the function `punchIn` defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Data.Fin.Relation.Ternary.PunchIn where
 
diff --git a/README/Data/Fin/Relation/Ternary/PunchOut.agda b/README/Data/Fin/Relation/Ternary/PunchOut.agda
index aebc9e4a83..557c7ddc7c 100644
--- a/README/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/README/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -11,7 +11,7 @@
 -- the function `punchOut` defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Data.Fin.Relation.Ternary.PunchOut where
 
diff --git a/src/Data/Fin/Relation/Ternary/Pinch.agda b/src/Data/Fin/Relation/Ternary/Pinch.agda
index 2f449d815f..26db16461c 100644
--- a/src/Data/Fin/Relation/Ternary/Pinch.agda
+++ b/src/Data/Fin/Relation/Ternary/Pinch.agda
@@ -9,7 +9,7 @@
 -- precisely mirrored in the constructors of the view type,
 -- ie that we 'view the function via its graph relation'
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module Data.Fin.Relation.Ternary.Pinch where
 
diff --git a/src/Data/Fin/Relation/Ternary/PunchIn.agda b/src/Data/Fin/Relation/Ternary/PunchIn.agda
index 2ba4581830..1c000a8e4d 100644
--- a/src/Data/Fin/Relation/Ternary/PunchIn.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchIn.agda
@@ -9,7 +9,7 @@
 -- precisely mirrored in the constructors of the view type,
 -- ie that we 'view the function via its graph relation'
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module Data.Fin.Relation.Ternary.PunchIn where
 
diff --git a/src/Data/Fin/Relation/Ternary/PunchOut.agda b/src/Data/Fin/Relation/Ternary/PunchOut.agda
index 70bf14b1a8..f27a635e7f 100644
--- a/src/Data/Fin/Relation/Ternary/PunchOut.agda
+++ b/src/Data/Fin/Relation/Ternary/PunchOut.agda
@@ -9,7 +9,7 @@
 -- precisely mirrored in the constructors of the view type,
 -- ie that we 'view the function via its graph relation'
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module Data.Fin.Relation.Ternary.PunchOut where