路径归纳隐含 [英] Path induction implied

问题描述

这是获取路径归纳以在 Agda 中工作的后续问题

我想知道这个结构什么时候可能更具表现力.在我看来，我们总是可以这样表达:

I wonder when that construct may be more expressive. It seems to me we can always express the same like so:

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 来自那个问题:

Here Agda will do path induction given the example which is the same as c : (x : A) -> C refl from that question:

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

看来这个函数是同构的:

It seems this function is isomorphic to:

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

这两种方式(f 与 pathInd)在功率上是否相同?

Are these two ways (f vs pathInd) identical in power?

推荐答案

pathInd 只是一个依赖消除器.这是一个同构的定义:

pathInd is just a dependent eliminator. Here is an isomorphic definition:

  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

有了这个，你就可以在_≡_上定义各种函数而无需进行模式匹配，例如:

Having this, you can define various functions on _≡_ without pattern-matching, for example:

  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] 所述:

But you can't prove uniqueness of identity proofs from J as described at [1]:

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

因此，您可以使用 Agda 的模式匹配表达更多内容，而不仅仅是使用 _≡_ 的依赖消除器.但是你可以使用 --without-K 选项:

So you can express more with Agda's pattern-matching, than with just a dependent eliminator for _≡_. But you can use the --without-K option:

{-# 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 现在不进行类型检查，导致此错误:

uip doesn't typecheck now, causing this error:

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/

这篇关于路径归纳隐含的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！