[Agda] a stuck cubical Agda proof

[Ayberk Tosun]

Hi Jason,

On 22/05/2021 00:28, fdhzs2010 at hotmail.com wrote:
> 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)?

It boils down to the fact that ℕ is itself a set:

```
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) =
  isSetℕ (get-ℕ d) (get-ℕ d′) (λ k → get-ℕ (eq k)) (λ k → get-ℕ (eq′ k)) i j
```

Best,
Ayberk