[Agda] a stuck cubical Agda proof

[Jason -Zhong Sheng- Hu]

Hi all,

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)?

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat

data dot : Set where
  A B : dot
  Eq : A ≡ B
  IsSet : isSet dot

get-ℕ : dot → ℕ
get-ℕ A                       = 0
get-ℕ B                       = 0
get-ℕ (Eq i)                  = 0
get-ℕ (IsSet d d′ eq eq′ i j) = {!!}


Thanks,
Jason Hu
https://hustmphrrr.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210521/6a93e291/attachment.html>