路径归纳暗示

Question

这是使路径归纳在Agda中起作用的后续问题

我想知道这个结构何时可能更具表现力.在我看来,我们总是这样表达:

f : forall {A} -> {x y : A} -> x == y -> "some type"
f refl = instance of "some type" for p == refl

在这里,Agda将根据c : (x : A) -> C refl与该问题相同的示例进行路径归纳:

pathInd : forall {A} -> (C : {x y : A} -> x == y -> Set)
                     -> (c : (x : A) -> C refl)
                     -> {x y : A} -> (p : x == y) -> C p

看来这个函数是同构的:

f' : forall {A} -> {x y : A} -> x == y -> "some type"
f' = pathInd (\p -> "some type") (\x -> f {x} refl)

这两种方式(fvs pathInd)的功率相同吗？

Answer 1

pathInd只是一个依赖消除器。这是一个同构定义：

  J : ? {? ?} {A : Set ?} {x y : A}
    -> (C : {x y : A} {p : x ? y} -> Set ?)
    -> ({x : A} -> C {x} {x})
    -> (p : x ? y) -> C {p = p}
  J _ b refl = b

有了这个，您可以在_?_不进行模式匹配的情况下定义各种功能，例如：

  sym : ? {?} {A : Set ?} {x y : A}
      -> x ? y
      -> y ? x
  sym = J (_ ? _) refl

  trans : ? {?} {A : Set ?} {x y z : A}
        -> x ? y
        -> y ? z -> x ? z
  trans = J (_ ? _ -> _ ? _) id

  cong : ? {? ?} {A : Set ?} {B : Set ?} {x y : A}
       -> (f : A -> B) 
       -> x ? y
       -> f x ? f y
  cong f = J (f _ ? f _) refl

  subst : ? {? ?} {A : Set ?} {x y : A}
        -> (C : A -> Set ?)
        -> x ? y
        -> C x -> C y
  subst C = J (C _ -> C _) id

但是您无法J根据[1]中的描述来证明身份证明的唯一性：

  uip : ? {?} {A : Set ?} {x y : A} -> (p q : x ? y) -> p ? q
  uip refl refl = refl

因此，您可以利用Agda的模式匹配来表达更多信息，而不仅仅依赖于_?_。但是您可以使用以下--without-K选项：

{-# OPTIONS --without-K #-}

open import Relation.Binary.PropositionalEquality  

uip : ? {?} {A : Set ?} {x y : A} -> (p q : x ? y) -> p ? q
uip refl refl = refl

uip 现在不进行类型检查，从而导致此错误：

Cannot eliminate reflexive equation x = x of type A because K has
been disabled.
when checking that the pattern refl has type x ? x

[1] http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/

Answer 2

提供一个简短的答案:你是对的,Agda的模式匹配意味着存在路径归纳原语.事实上,已经证明,在具有宇宙的类型理论中,依赖模式匹配等同于归纳类型的感应原语和所谓的K公理的存在:

http://link.springer.com/chapter/10.1007/11780274_27

最近,已经证明(最新实现)Agda的--without-K选项限制了模式匹配,使得它仅与感应类型的归纳原语的存在等效:

http://dl.acm.org/citation.cfm?id=2628136.2628139

完全披露:我是后者工作的合着者.