From 1eb6441aa065bb68aa5ad122f08a5f08fb56774f Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 28 Oct 2024 20:20:57 -0500
Subject: [PATCH] succ str on N x fib, closes #37

---
 src/ThesisWork/Pi3S2/SuccStr.agda | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/src/ThesisWork/Pi3S2/SuccStr.agda b/src/ThesisWork/Pi3S2/SuccStr.agda
index ba3ee18..8aab348 100644
--- a/src/ThesisWork/Pi3S2/SuccStr.agda
+++ b/src/ThesisWork/Pi3S2/SuccStr.agda
@@ -27,8 +27,23 @@ module _ where
   open import Data.Fin
   open import Data.Product
 
+  inc-k-inv : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+  inc-k-inv {k} (n , zero) = (suc n) , opposite zero
+  inc-k-inv {k} (n , suc k1) = n , inject₁ k1
+
+  inc : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+  inc {k} (n , k1) =
+    let result = inc-k-inv (n , opposite k1) in
+    (fst result) , opposite (snd result)
+
+  _ : inc {k = 3} (5 , fromℕ 2) ≡ (6 , zero)
+  _ = refl
+
+  -- _ : inc {k = 3} (5 , inject₁ (fromℕ 1)) ≡ (6 , zero)
+  -- _ = {!  refl !}
+
+  _ : inc {k = 5} (5 , fromℕ 4) ≡ (6 , zero)
+  _ = refl
+
   ℕ-k-SuccStr : (k : ℕ) → (ℕ × Fin k) → ℕ → (ℕ × Fin k)
-  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc where
-    inc : (ℕ × Fin k) → (ℕ × Fin k)
-    inc (n , k) with suc k
-    inc (n , k) | x = {!   !}
\ No newline at end of file
+  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc
\ No newline at end of file