The half-integers

module elementary-number-theory.half-integers where

open import elementary-number-theory.addition-integers
open import elementary-number-theory.integers

open import foundation.coproduct-types
open import foundation.universe-levels

Idea

The half-integers are the numbers of the form x + ½, where x : ℤ.

Definition

The half-integers

ℤ+½ : UU lzero
ℤ+½ = ℤ

The disjoint union of the half-integers with the integers

½ℤ : UU lzero
½ℤ = ℤ+½ + ℤ

The zero element of ½ℤ

zero-½ℤ : ½ℤ
zero-½ℤ = inr zero-ℤ

Addition on ½ℤ

add-½ℤ : ½ℤ → ½ℤ → ½ℤ
add-½ℤ (inl x) (inl y) = inr (succ-ℤ (x +ℤ y))
add-½ℤ (inl x) (inr y) = inl (x +ℤ y)
add-½ℤ (inr x) (inl y) = inl (x +ℤ y)
add-½ℤ (inr x) (inr y) = inr (x +ℤ y)

infix  _+½ℤ_
_+½ℤ_ = add-½ℤ