<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);">
Hi all,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
I find the following proof should be very easy but I am not sure how to discharge the last obligation. What am I missing here (both in code and conceptually)?<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<span style="font-family: "Courier New", monospace;">open import Cubical.Foundations.Prelude</span>
<div><span style="font-family: "Courier New", monospace;">open import Cubical.Data.Nat</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">data dot : Set where</span></div>
<div><span style="font-family: "Courier New", monospace;"> A B : dot</span></div>
<div><span style="font-family: "Courier New", monospace;"> Eq : A ≡ B</span></div>
<div><span style="font-family: "Courier New", monospace;"> IsSet : isSet dot</span></div>
<div><br>
</div>
<div><span style="font-family: "Courier New", monospace;">get-ℕ : dot → ℕ</span></div>
<div><span style="font-family: "Courier New", monospace;">get-ℕ A = 0</span></div>
<div><span style="font-family: "Courier New", monospace;">get-ℕ B = 0</span></div>
<div><span style="font-family: "Courier New", monospace;">get-ℕ (Eq i) = 0</span></div>
<span style="font-family: "Courier New", monospace;">get-ℕ (IsSet d d′ eq eq′ i j) = {!!}</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<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>
</body>
</html>