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经常被使用。

问题是


[有一个|什么是正确的事?

最佳答案

关于对类型中的关系使用重写的bug,这将使您只说rewrite <- y.

同时,

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


可能会做您想要的。

10-06 10:30
查看更多