<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
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>
</body>
</html>