Аналогом индукции по пути в Coq является конструкция match. Вот как мы можем использовать его для определения (основанной) индукции пути, как описано в книге HoTT.

Set Implicit Arguments.

Definition J {A} {x : A} (P : forall y, x = y -> Type)
                 (H : P x eq_refl) : forall y p, P y p :=
  fun y p => match p with eq_refl => H end.

Тип этого определения гласит, что всякий раз, когда мы хотим доказать P y p, где

• y : A,
• p : x = y и
• P : forall y, x = y -> Type,

достаточно показать, что P x eq_refl выполняется. Мы можем использовать J, чтобы показать, что ваша g функция постоянна. (Я перефразировал определения, чтобы они соответствовали тем, которые даны в стандартной библиотеке Coq.)

Definition f (s : unit) : tt = tt := match s with tt => eq_refl end.
Definition g (p : tt = tt) : unit := match p return unit with eq_refl => tt end.

Definition g_tt p : g p = tt :=
  J (fun y q => match q return unit with eq_refl => tt end = tt)
    eq_refl p.

Сложная часть этого доказательства - выяснить, каким должен быть параметр P у J, что также относится к другим доказательствам, проводимым путем индукции по путям. Здесь мне пришлось развернуть определение g, потому что для него требуется аргумент типа tt = tt, тогда как q, использованный выше, имеет тип tt = y. В любом случае вы можете видеть, что P tt p по определению равно g p = tt, что мы и хотим доказать.

Мы можем сыграть шутку, чтобы показать, что p = eq_refl для любого p : tt = tt. В сочетании с предыдущим результатом это даст именно то, что вы хотите.

Definition result (p : tt = tt) : p = eq_refl :=
  J (fun y q =>
       unit_rect (fun z => tt = z -> Prop)
                 (fun u => u = eq_refl)
                 y q)
    eq_refl p.

И снова суть в параметре P. Мы используем принцип индукции для unit, который гласит, что мы можем определить что-то типа T x (для T : unit -> Type и x : tt) всякий раз, когда мы можем найти элемент T tt. Напомним, что результат этого приложения J должен иметь тип

P tt p

что в данном случае просто

unit_rect (fun z => tt = z -> Prop)
          (fun u => u = eq_refl)
          tt p
= (p = eq_refl)

по правилам расчета для unit_rect.

К сожалению, такого рода доказательства трудно воспроизвести с помощью тактического языка Coq, потому что часто возникают проблемы с определением того, каким P должно быть. Часто бывает проще самому определить, каким должно быть это значение, и явно записать термин доказательства.

Я не совсем понимаю, почему, но Coq также намного лучше разбирается в этой аннотации, если вы запишете термин доказательства с помощью match. Сравнивать:

Definition result' (p : tt = tt) : p = eq_refl :=
  match p with eq_refl => eq_refl end.

Хотя это выглядит намного проще, вы увидите, что фактический термин, выводимый Coq, намного сложнее, когда вы попытаетесь его распечатать. Попробуй!

Редактировать

Ах, я только что понял, что вы пытались использовать HoTT-версию Coq. У меня не установлена ​​эта версия, но я думаю, что адаптировать к ней мое решение не составит особого труда.