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

[Andreas Nuyts]

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/2ecc6e0b/attachment.html>