[Agda] Cubical: "show", and families over HITs

[Andreas Nuyts]

Hi everyone,

First, for clarity, I meant C-u C-u C-c C-n instead of C-c C-c C-u C-n.

Anyway, I had not recognized

    transp (λ i → Test (seg i)) i0 (test true (λ _ → zero))


as a normal form, which apparently it is, so Q2 has been sufficiently 
answered for my purposes.

Best regards,
Andreas

On 28.07.21 09:35, Andreas Nuyts wrote:
> Hi everyone,
>
> I have two questions about Agda cubical, related to the following code:
>
>     {-# OPTIONS --cubical #-}
>     module hit-family-test where
>
>     open import Cubical.Data.Equality hiding (Sub) renaming (reflc to
>     refl)
>     open import Cubical.Data.Bool
>     open import Cubical.HITs.Interval
>     open import Cubical.Foundations.Everything hiding (Sub ; _∘_)
>
>     ---------------------------------
>
>     data Pest : Interval → Set where
>       pest : Bool → Pest zero
>
>     getPest : Pest one → Bool
>     getPest p = {!!} -- cannot match
>
>     ---------------------------------
>
>     data Test : Interval → Set where
>       test : ∀ {i} → Bool → i ≡ zero → Test i
>
>     getTest : Test one → Bool
>     getTest (test b p) = b
>
>     test-one : Bool → Test one
>     test-one b = subst Test seg (test b refl)
>
>     x : Test one
>     x = {!test-one true!}
>
>
> Q1: is Test the best workaround if you really want Pest?
>
> Q2: the hole for "x" type-checks, but I wanted to see what it computes 
> to. When I press C-c C-n, I get:
>
>     transp (λ i → Test (seg i)) i0 (test true (λ _ → zero))
>
>
> but when I press C-c C-c C-u C-n I get:
>
>     Not in scope:
>       show at <path>
>     when scope checking show
>
>
> I presume this "show" thing is something that should behave analogous 
> to Haskell's "show". I can't find anything relevant on 
> agda.readthedocs.io. Grepping the cubical library for "show" also 
> yields no results. What is this show and how do I get it in scope? 
> Should I implement it myself?
>
> Best regards,
> Andreas

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210728/0fb1d6bf/attachment.html>