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

[Evan Cavallo]

Hi Andreas,

For Q1, to eliminate from an inductive family, you need to be general in 
the indices. The following works:

    getPest : ∀ {x} → Pest x → Bool
    getPest (pest x) = x

Then you could specialize to x = one.

Best,
Evan

On 7/28/21 10:18 AM, Andreas Nuyts wrote:
> 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/9057dee9/attachment.html>