Path induction implied

3
votes

This is a follow-up question to Getting path induction to work in 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

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)

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

2
typesagda
This could be helpful: homotopytypetheory.org/2011/04/10/… - user3237465
@user3237465 yes, i am reading through that. Yet my question is about Agda doing path induction for f. I don't see the use for pathInd, expressed as a function just like in HoTT, unless it is in some way more general than f. In other words, since to use pathInd one needs to replicate the same thing one needs to do to define f, I don't see if there is anything practical to be gained by introducing pathInd, except for exercise, which of course is a merit. - Sassa NF

2 Answers

6
votes

To provide a short answer: you're right, Agda's pattern matching implies the existence of a path-induction primitive. In fact, it has been shown that in a type theory with universes, dependent pattern matching is equivalent to the existence of induction primitives for inductive types and the so-called K axiom:

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

More recently, it has been shown that (the latest implementation of) Agda's --without-K option restricts pattern matching such that it is only equivalent with the existence of induction primitives for inductive types:

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

Full disclosure: I'm a co-author of the latter work.

5
votes

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

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

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 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/