То есть он возвращает не int?
он возвращает пруф равенства
а равенство элементов типа X это функция от [0..1] -> X
то есть для a, b : X
p : a = b
это функция [0..1] -> X где
p 0 = a
p 1 = b
и p при этом является неприрывной
вот этот конструктор задает аксиому что между neg 0 и pos 0 существует неприрывный путь