title: Path induction implied
body: <p>This is a follow-up question to <a href="https://stackoverflow.com/questions/26634363/getting-path-induction-to-work-in-agda">Getting path induction to work in Agda</a></p>
  
  <p>I wonder when that construct may be more expressive. It seems to me we can always express the same like so:</p>
  
  <pre><code>f : forall {A} -&gt; {x y : A} -&gt; x == y -&gt; "some type"
  f refl = instance of "some type" for p == refl
  </code></pre>
  
  <p>Here Agda will do path induction given the example which is the same as <code>c : (x : A) -&gt; C refl</code> from that question:</p>
  
  <pre><code>pathInd : forall {A} -&gt; (C : {x y : A} -&gt; x == y -&gt; Set)
                       -&gt; (c : (x : A) -&gt; C refl)
                       -&gt; {x y : A} -&gt; (p : x == y) -&gt; C p
  </code></pre>
  
  <p>It seems this function is isomorphic to:</p>
  
  <pre><code>f' : forall {A} -&gt; {x y : A} -&gt; x == y -&gt; "some type"
  f' = pathInd (\p -&gt; "some type") (\x -&gt; f {x} refl)
  </code></pre>
  
  <p>Are these two ways (<code>f</code> vs <code>pathInd</code>) identical in power?</p>