<div dir="ltr">Hi all,<div><br></div><div>I'm super new to Agda and the Agda community. Hopefully this is the right place to ask something like this, but please call me out if it isn't.</div><div><br></div><div><br></div><div>I'm working on an Agda development for a QTT formalization. I'm trying to use an intrinsically typed representation for terms, but run into unification issues when trying to define substitution. </div><div><br></div><div>Substitution:</div><div><img src="cid:ii_kfq9m0xt0" alt="Screen Shot 2020-09-30 at 8.34.38 PM.png" width="542" height="30"><br></div><div><br></div><div>Error message:</div><div><img src="cid:ii_kfq9m96s1" alt="Screen Shot 2020-09-30 at 8.34.50 PM.png" width="542" height="118"><br></div><div><br></div><div>Application def:</div><div><img src="cid:ii_kfq9mkfj2" alt="Screen Shot 2020-09-30 at 8.35.05 PM.png" width="363" height="88"><br></div><div><div><br></div><div>I'm sort of at a loss for how to get around this. Is the issue because of the functions in the return type? </div></div><div><br></div><div>More broadly, it seems like intrinsic typing is the Agda way of doing things, and gives a lot for free. And it works really well in the STLC example given in the PLFA textbook. But for a more complicated type system like this, I'm starting to think it might be easier to use extrinsic typing? I've also had to rely on the REWRITE pragma which I just learned isn't allowed in --safe due to potential non-convergence. </div><div>Does someone maybe have experience with this and could speak to pros/cons of using intrinsic vs extrinsic typing here?</div><div><br></div><div>Thanks,</div><div>Daniel</div></div>