Про них тоже же можно сказать, что это базовые сущности "из воздуха", из которых потом что-то конструируется

Но в любом случае, терминология настораживает. Кажется, что из конструктивного доказательства всегда можно извлечь конструкцию, а тут оказывается, что нет

LEM нам позволяет доказать, что любое утверждение разрешимо. Конструктивно это неверно.

Мы извлекаем категорную конструкцию, ну, то есть, в К-логике доказательство -- это тоже текст морфизма. Но объекты и некоторые морфизмы в ней могут не быть деревьями индуктивных типов.

Поэтому я предпочитаю говорить "интуиционистская логика" вместо "конструктивная математика".

Извлечь можно, только извне, а не внутри логики.

А, так то есть, прообразы сюръекции всё-таки как-то можно найти?

Не обязательно. Бывают очень хитрые функции. Ну, типа, характеристическая функция останавливающихся машин тьюринга.

Если есть конкретная функция f : A -> B и конкретное доказательство сюръективности f и конкретный элемент b : B, то можно выписать его прообраз. Но это всё не внутри логики.

Ну т.е. утверждение, которое я написал невозможно _доказать_ в этой логике

Но сделать вне неё это можно.

Хорошо, вот есть в Set конкретная функция, про которую известно, что она эпиморфизм. Из доказательства получаем, что это также сюръекция. Форма записи прообразов в утверждении сюръекции же будет как-то отражать рассуждение? Я имею в виду, если ничего не редуцировать

Причем даже не надо знать, что метатеория, в которой мы работаем, классическая. Достаточно знать, что она мощнее исходной теории в должном смысле.

OK. Я отвечу на вопрос "откуда берутся прообразы". Они берутся из доказательства эпиморфности. Оно для любой пары функций g,h : B -> Prop таких, что gf = hf. возвращает доказательство g = h. В этом доказательстве скрыта какая-то нетривиальная функция, которая позволяет для каждого b : B получить доказательство g(b) = h(b). А в этом доказательстве в свою очередь скрыто еще две нетривиальные функции. Одна позволяет из доказательства g(b) получить доказательство h(b), а другая наоборот. Если подставить теперь те g и h, то потом из одной из них можно будет извлечь этот прообраз.

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

Ок, это понятно

Осталось осознать, что эти g и h тоже строятся

Сами g и h не особо интересны. Вся соль скрыта в доказательстве эпиморфности, все нетривиальные функции из него берутся.

Ну и всё же, раз это характеристические функции, они получаются из того факта, что в Set есть классификатор подобъектов

Да, но вопрос же в том, откуда берется прообраз, и он берется по сути не из них.