<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
thank you very much. <br>
</div>
<div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div>
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
</div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Ayberk Tosun <a.tosun@pgr.bham.ac.uk><br>
<b>Sent:</b> May 21, 2021 5:40 PM<br>
<b>To:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Cc:</b> fdhzs2010@hotmail.com <fdhzs2010@hotmail.com><br>
<b>Subject:</b> Re: [Agda] a stuck cubical Agda proof</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Hi Jason,<br>
<br>
On 22/05/2021 00:28, fdhzs2010@hotmail.com wrote:<br>
> I find the following proof should be very easy but I am not sure how to<br>
> discharge the last obligation. What am I missing here (both in code and<br>
> conceptually)?<br>
<br>
It boils down to the fact that ℕ is itself a set:<br>
<br>
```<br>
open import Cubical.Foundations.Prelude<br>
open import Cubical.Data.Nat<br>
<br>
data dot : Set where<br>
A B : dot<br>
Eq : A ≡ B<br>
IsSet : isSet dot<br>
<br>
get-ℕ : dot → ℕ<br>
get-ℕ A = 0<br>
get-ℕ B = 0<br>
get-ℕ (Eq i) = 0<br>
get-ℕ (IsSet d d′ eq eq′ i j) =<br>
isSetℕ (get-ℕ d) (get-ℕ d′) (λ k → get-ℕ (eq k)) (λ k → get-ℕ (eq′ k)) i j<br>
```<br>
<br>
Best,<br>
Ayberk<br>
</div>
</span></font></div>
</body>
</html>