<div dir="ltr">Hi all,<br><div><br></div><div>I'm brand new to Agda and the Curry-Howard isomorphism (and really loving this new exploration of both!), and I have a <i>philosophical</i> objection to how the <font face="monospace"><b>absurd</b></font> function is used to generate whatever we need to complete a proof.</div><div><br></div><div>I understand how we are able to satisfy the Agda compiler with the definition of <font face="monospace"><b>absurd</b></font>; my objection isn't mechanical/technical.</div><div><br></div><div>What bothers me is a feeling that I'm "cheating" when I use this function that can never be called, in order to "produce" that which I need to complete my proof.</div><div><br></div><div>I wonder if someone could offer a different perspective on this, for consideration.</div><div><br></div><div>Thanks!</div><div>-db</div><div><br></div></div>