1

我有以下设置（对不起，如果它对 MCVE 来说有点长）并试图证明最后一个定理，但我遇到了困难，因为它无法统一态射的类型，因为它们依赖于理论上不同的对象类型，即使对象类型相同。

是否有分解具有依赖类型的构造函数的一般策略？injection并inversion产生似乎无用的结果ob_fn（我可以很容易地证明等价定理）而不是morph_fn.

Inductive Cat := cons_cat (O : Type) (M : O -> O -> Type).

Definition ob (c : Cat) :=
    match c with cons_cat o _ => o end.

Definition morph (c : Cat) : ob c -> ob c -> Type :=
    match c with cons_cat _ m => m end.

Inductive Functor
    (A B : Cat)
        : Type :=
    cons_functor
        (ob_fn : ob A -> ob B)
        (morph_fn : forall {c d : ob A}, morph A c d -> morph B (ob_fn c) (ob_fn d)).

Definition ob_fn {A B : Cat} (f : Functor A B) : ob A -> ob B :=
    match f with cons_functor f' _ => f' end.

Definition morph_fn {A B : Cat} {c d : ob A} (f : Functor A B)
        : morph A c d -> morph B (ob_fn f c) (ob_fn f d) :=
    match f with cons_functor _ f' => f' c d end.

Theorem functor_decompose {A B : Cat} {o fm gm} : cons_functor A B o fm = cons_functor A B o gm -> fm = gm.
    intros H.
    assert (forall c d, @morph_fn A B c d (cons_functor A B o fm) = @morph_fn A B c d (cons_functor A B o gm)).
        intros.
        rewrite H.
4

1 回答 1

0

标准模式是将您的记录转换为 sigma 类型，并讨论 sigma 类型的相等性或字段的传输相等性。参见，例如，HoTT library中使用的这个版本functor_decompose。您可能还对inversion_sigmaCoq 8.7 的策略和相应的sigma 相等分类感兴趣。

于 2017-07-28T04:57:08.190 回答