[Agda] a stuck cubical Agda proof

[Jason -Zhong Sheng- Hu]

thank you very much.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Ayberk Tosun <a.tosun at pgr.bham.ac.uk>
Sent: May 21, 2021 5:40 PM
To: agda at lists.chalmers.se <agda at lists.chalmers.se>
Cc: fdhzs2010 at hotmail.com <fdhzs2010 at hotmail.com>
Subject: Re: [Agda] a stuck cubical Agda proof

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210521/7ffcfbbf/attachment.html>