Kubus

intlib/int.ktt

Natural numbers and integers; the successor equivalence of the integers.

9 declarations, all certified by the kernel · source

1import equiv
2
3✓data Nat : U := zero | suc (n : Nat)
4
5✓def add (m : Nat) : Nat -> Nat
6 | zero => m
7 | suc n => suc (add m n)
8
9✓def addZero : (n : Nat) -> Path Nat (add zero n) n
10 | zero => \i -> zero
11 | suc n => \i -> suc (addZero n i)
13✓data Int : U := pos (n : Nat) | negsuc (n : Nat)
15✓def sucInt : Int -> Int
16 | pos n => pos (suc n)
18 | negsuc (suc n) => negsuc n
20✓def predInt : Int -> Int
22 | pos (suc n) => pos n
23 | negsuc n => negsuc (suc n)
25✓def sucPred : (z : Int) -> Path Int (sucInt (predInt z)) z
26 | pos zero => \i -> pos zero
27 | pos (suc n) => \i -> pos (suc n)
28 | negsuc n => \i -> negsuc n
30✓def predSuc : (z : Int) -> Path Int (predInt (sucInt z)) z
31 | pos n => \i -> pos n
32 | negsuc zero => \i -> negsuc zero
33 | negsuc (suc n) => \i -> negsuc (suc n)
35✓def sucPathInt : Path U Int Int := isoToPath sucInt predInt sucPred predSuc