deniok

Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. ~~И мы знаем такое число, но никому не скажем, что это 2.~~ Обобщим это наблюдение, введя бинарное отношение принадлежности величины образу функции f как тип данных Агды

data Image_∋_ {X Y : Set}(f : X → Y) : Y → Set where
  im : (x : X) → Image f ∋ f x

Наличие всего одного конструктора отражает тот факт, что единственный способ сконструировать элемент образа f - выбрать аргумент x и применить f к этому x. Например, рассматривая функции

square : ℕ → ℕ
square n = n * n

cube  : ℕ → ℕ
cube n = n * n * n

легко заметить, что im 2 может выступить свидетельством того, что образ square содержит 4

lem-4-is-square : Image square ∋ 4
lem-4-is-square = im 2

или того, что образ cube содержит 8

lem-8-is-cube : Image cube ∋ 8
lem-8-is-cube = im 2

Перейдём теперь к построению обратной функции. Обратная к f функция может иметь в качестве области определения не все значения из Y, а только те, что принадлежат образу f. Чтобы Агда могла проконтролировать этот факт, мы должны, помимо самой функции и аргумента, передать ещё и соответствующий объект-свидетельство про этот аргумент

inv : {X Y : Set}(f : X → Y)(y : Y) → Image f ∋ y → X
inv f .(f x) (im x) = x

Теперь можно посчитать значение функции, обратной к квадрату в точке 4

my-value-is-2 : ℕ
my-value-is-2 = inv square 4 lem-4-is-square

и функции, обратной к кубу в точке 8

my-value-is-2-too : ℕ
my-value-is-2-too = inv cube 8 lem-8-is-cube

Если же мы попробуем написать

i-am-not-a-nat = inv square 5 {! !}

то Агда затребует от нас сконструировать для дырки объект ?0 : Image square ∋ 5, необитаемость которого очевидна.

Ремарка. Точечный образец в определении inv необходим для подсказки компилятору о том, что после связывания f в первом аргументе и x - в третьем единственное корректное значение второго аргумента это (f x).