В качестве грубого и неопознанного фона, в HoTT, выводится вывод из индуктивно определенного типа
Inductive paths {X : Type } : X -> X -> Type :=
| idpath : forall x: X, paths x x.
что позволяет сделать очень общую конструкцию
Lemma transport {X : Type } (P : X -> Type ){ x y : X} (γ : paths x y):
P x -> P y.
Proof.
induction γ.
exact (fun a => a).
Defined.
Lemma transport
станет основой тактики HoTT "replace" или "rewrite"; трюк, насколько я понимаю, был бы, полагая, что цель, которую вы или я можем абстрактно признать как
...
H : paths x y
[ Q : (G x) ]
_____________
(G y)
чтобы выяснить, что является необходимым зависимым типом G, чтобы мы могли apply (transport G H)
. До сих пор все, что я выяснил, это то, что
Ltac transport_along γ :=
match (type of γ) with
| ?a ~~> ?b =>
match goal with
|- ?F b => apply (transport F γ)
| _ => idtac "apparently couldn't abstract" b "from the goal." end
| _ => idtac "Are you sure" γ "is a path?" end.
недостаточно общего. То есть, первый idtac
используется довольно часто.
Вопрос:
[Есть ли | что такое] Правильное дело?