在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.
可能会做您想要的。