michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

succ str on N x fib, closes #37

Browse source
This commit is contained in:
Michael Zhang 2024-10-28 20:20:57 -05:00
parent 4c435f3764
commit 1eb6441aa0
1 changed files with 19 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/ThesisWork/Pi3S2/SuccStr.agda
View file

@ -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 = {! !}
ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc