16

ラフで未熟な背景として、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 の「置換」または「書き換え」戦術の中心になります。私が理解している限り、トリックは、あなたまたは私が抽象的に認識できる目標を想定することです.

...
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ものはかなり頻繁に使用されます。

質問は

[ありますか | 正しいことは何ですか？

4

2 に答える 2

5

タイプのリレーションに rewrite を使用することに関するバグがあります。rewrite <- y.

その間、

Ltac transport_along γ :=
  match (type of γ) with 
    | ?a ~~> ?b => pattern b; apply (transport _ y)
    | _ => idtac "Are you sure" γ "is a path?"
  end.

おそらくあなたが望むことをします。

于 2012-02-22T03:21:22.617 に答える