<div dir="ltr">Hi, I&#39;m trying to do an exercise from &quot;Dependent Types at Work&quot;. The exercise is from section 4.4 and asks to prove eq-succ and eq-mult-rec. My problem is I don&#39;t understand some of the typing issues.<div>

<br></div><div>Here&#39;s what I have so far:</div><div><br></div><div>&gt;&gt;&gt;</div><div><div>module exercises where</div><div><br></div><div>--</div><div><br></div><div>data Nat : Set where</div><div>  zero : Nat</div>

<div>  succ : Nat -&gt; Nat</div><div><br></div><div>_+_ : Nat -&gt; Nat -&gt; Nat</div><div>zero + m = m</div><div>succ n + m = succ (n + m)</div><div><br></div><div>natrec : {C : Nat -&gt; Set} -&gt; (C zero) -&gt;</div>
<div>         ((m : Nat) -&gt; C m -&gt; C (succ m)) -&gt; (n : Nat) -&gt; C n</div><div>natrec p h zero = p</div>
<div>natrec p h (succ n) = h n (natrec p h n)</div><div><br></div><div>plus : Nat -&gt; Nat -&gt; Nat</div><div>plus n m = natrec m (λ x y -&gt; succ y) n</div><div><br></div><div>--<br></div><div><br></div><div>data _==_ {A : Set} : A -&gt; A -&gt; Set where</div>

<div>  refl : (a : A) -&gt; a == a</div><div><br></div><div>subst : {A : Set} -&gt; {C : A -&gt; Set} -&gt; {a&#39; a&#39;&#39; : A} -&gt;</div><div>        a&#39; == a&#39;&#39; -&gt; C a&#39; -&gt; C a&#39;&#39;</div><div>

subst (refl a) c = c</div><div><br></div><div>--</div><div><br></div><div>eq-succ : {n m : Nat} -&gt; n == m -&gt; succ n == succ m</div><div>eq-succ (refl m) = refl (succ m)</div><div><br></div><div>eq-plus-rec : (n m : Nat) -&gt; (n + m) == (plus n m)</div>

<div>eq-plus-rec n m = natrec (refl m) (λ j ih -&gt; {! !}) n</div></div><div><br></div><div>&lt;&lt;&lt;</div><div><br></div><div>When I replace the hole with &#39;eq-succ ih&#39;, like it is in the pdf, agda gives an error:</div>
<div><br></div><div>&gt;&gt;&gt;</div><div>Refuse to construct infinite term by instantiating _47 to succ</div><div>(_n_47 n m k)</div><div>when checking that the expression eq-succ ih has type</div><div>_n_47 n m (succ k) == _m_48 n m (succ k)</div>
<div>&lt;&lt;&lt;</div><div><br></div><div>Sticking a hole in there to try and typing &#39;c-c c-,&#39; to try and understand what&#39;s happening agda tells me:</div><div><br></div><div>&gt;&gt;&gt;</div><div>ih : _C_41 n m k&#39;</div>
<div>k&#39; : Nat</div><div>m : Nat</div><div>n : Nat</div><div>&lt;&lt;&lt;</div><div><br></div><div>Typing &#39;c-c c-l&#39; to see what _C_41 is tells me that it has type &#39;Nat -&gt; Set&#39;. So is ih a parameterized type? Or is it just a list of types?</div>
<div><br></div><div>If I put &#39;eq-succ ih&#39; in the hole and type &#39;c-c c-.&#39; agda tells me</div><div><br></div><div>&gt;&gt;&gt;</div><div>Goal: _n_50 n m (succ k&#39;) == _m_51 n m (succ k&#39;)</div><div>Have: succ (_n_50 n m k&#39;) == succ (_m_51 n m k&#39;)</div>
<div>----</div><div>ih : _n_50 n m k&#39; == _m_51 n m k&#39;</div><div>...</div><div>&lt;&lt;&lt;</div><div><br></div><div>So I see that to make the definition work I somehow have to move the succ from the outside to the k&#39; but I don&#39;t know what _n_50 n m k&#39; is.</div>
<div><br></div><div>So three questions; how is it I&#39;m constructing an infinite type when I replace the hole with &#39;eq-succ ih&#39;? What is &#39;_C_41 n m k&#39;&#39; and &#39;_n_50 n m k&#39;&#39; and what do I do with them? It&#39;s probably a stupid question but I&#39;m stumped.</div>

</div>