type_arith.idr

(+) : Type -> Type -> Type
a + b = Either a b

record Iso (a : Type) (b : Type) where
  constructor MkIso
  to : a -> b
  from : b -> a
  leftInv : (x : a) -> from (to x) = x
  rightInv : (y : b) -> to (from y) = y

data (-) : Type -> Type -> Type where
  MkSub : (0 iso : Iso (c + b) a) -> c -> a - b

(*) : Type -> Type -> Type
x * y = (x, y)

data (/) : Type -> Type -> Type where
  MkDiv : (0 iso : Iso (c * b) a) -> c -> a / b

data Log : Type -> Type -> Type where
    MkLog : (0 iso : Iso (exponent -> base) a) -> exponent -> Log base a

log = Log

data Fin : Nat -> Type where
  FZ : Fin (S n)
  FS : Fin n -> Fin (S n)

example : Fin 10 / Fin 5
example = MkDiv iso (FS FZ) where
  0 iso : Iso (Fin 2 * Fin 5) (Fin 10)
  -- implementation left as exercise to the reader