<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Andreas,</p>
<p>For Q1, to eliminate from an inductive family, you need to be
general in the indices. The following works:<br>
</p>
<blockquote>
<p>getPest : ∀ {x} → Pest x → Bool<br>
getPest (pest x) = x</p>
</blockquote>
<p>Then you could specialize to x = one.<br>
</p>
<p>Best,<br>
Evan<br>
</p>
<div class="moz-cite-prefix">On 7/28/21 10:18 AM, Andreas Nuyts
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:f15c5561-055c-91ee-9a3a-a0578187b1c9@gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
Hi everyone,<br>
<br>
First, for clarity, I meant C-u C-u C-c C-n instead of C-c C-c C-u
C-n.<br>
<br>
Anyway, I had not recognized<br>
<br>
<blockquote>transp (λ i → Test (seg i)) i0 (test true (λ _ →
zero))<br>
</blockquote>
<br>
as a normal form, which apparently it is, so Q2 has been
sufficiently answered for my purposes.<br>
<br>
Best regards,<br>
Andreas<br>
<br>
<div class="moz-cite-prefix">On 28.07.21 09:35, Andreas Nuyts
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:cb2419f3-8c7e-b1f0-5ec8-2471831f576a@gmail.com">
Hi everyone,<br>
<br>
I have two questions about Agda cubical, related to the
following code:<br>
<br>
<blockquote>{-# OPTIONS --cubical #-}<br>
module hit-family-test where<br>
<br>
open import Cubical.Data.Equality hiding (Sub) renaming (reflc
to refl)<br>
open import Cubical.Data.Bool<br>
open import Cubical.HITs.Interval<br>
open import Cubical.Foundations.Everything hiding (Sub ; _∘_)<br>
<br>
---------------------------------<br>
<br>
data Pest : Interval → Set where<br>
pest : Bool → Pest zero<br>
<br>
getPest : Pest one → Bool<br>
getPest p = {!!} -- cannot match<br>
<br>
---------------------------------<br>
<br>
data Test : Interval → Set where<br>
test : ∀ {i} → Bool → i ≡ zero → Test i<br>
<br>
getTest : Test one → Bool<br>
getTest (test b p) = b<br>
<br>
test-one : Bool → Test one<br>
test-one b = subst Test seg (test b refl)<br>
<br>
x : Test one<br>
x = {!test-one true!}<br>
</blockquote>
<br>
Q1: is Test the best workaround if you really want Pest?<br>
<br>
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:<br>
<br>
<blockquote>transp (λ i → Test (seg i)) i0 (test true (λ _ →
zero))<br>
</blockquote>
<br>
but when I press C-c C-c C-u C-n I get:<br>
<br>
<blockquote>Not in scope:<br>
show at <path><br>
when scope checking show<br>
</blockquote>
<br>
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?<br>
<br>
Best regards,<br>
Andreas<br>
</blockquote>
<br>
</blockquote>
</body>
</html>