<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<font face="Courier New, Courier, monospace">Dear all,<br>
</font>
<p><font face="Courier New, Courier, monospace">Is there a Cubical
Agda equivalent of the following Agda statement for dependent
equality ? With appropriate imports the statement is accepted by
Cubical Agda. Obviously, the proof is not.</font></p>
<p><font face="Courier New, Courier, monospace">Best regards,</font></p>
<p><font face="Courier New, Courier, monospace"> - Vlad<br>
</font></p>
<pre style="margin-top: 0px; margin-right: 0px; margin-bottom: calc(var(--s-prose-spacing) + 0.4em); margin-left: 0px; padding: 12px; border: 0px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-variant-numeric: inherit; font-variant-east-asian: inherit; font-weight: 400; font-stretch: inherit; line-height: 1.30769; font-family: Consolas, Menlo, Monaco, "Lucida Console", "Liberation Mono", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Courier New", monospace, sans-serif; font-size: 13px; vertical-align: baseline; box-sizing: inherit; width: auto; max-height: 600px; overflow: auto; background-color: var(--highlight-bg); border-radius: 5px; overflow-wrap: normal; color: var(--highlight-color); letter-spacing: normal; orphans: 2; text-align: left; text-indent: 0px; text-transform: none; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;"><font face="Courier New, Courier, monospace"><code style="margin: 0px; padding: 0px; border: 0px none; font-style: inherit; font-variant: inherit; font-weight: inherit; font-stretch: inherit; line-height: inherit; font-size: 13px; vertical-align: baseline; box-sizing: inherit; background-color: transparent; white-space: inherit; color: var(--black-800); border-radius: 0px;">Σ-≡-intro :
∀ {α β}{A : Set α}{B : A → Set β}{a a' : A}{b : B a}{b' : B a'}
→ (Σ (a ≡ a') λ p → subst B p b ≡ b') → (a , b) ≡ (a' , b')
Σ-≡-intro (refl , refl) = refl
</code></font>
<code style="margin: 0px; padding: 0px; border: 0px; font-style: inherit; font-variant: inherit; font-weight: inherit; font-stretch: inherit; line-height: inherit; font-family: Consolas, Menlo, Monaco, "Lucida Console", "Liberation Mono", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Courier New", monospace, sans-serif; font-size: 13px; vertical-align: baseline; box-sizing: inherit; background-color: transparent; white-space: inherit; color: var(--black-800); border-radius: 0px;"></code></pre>
<code style="margin: 0px; padding: 0px; border: 0px; font-style:
inherit; font-variant: inherit; font-weight: inherit;
font-stretch: inherit; line-height: inherit; font-family:
Consolas, Menlo, Monaco, "Lucida Console",
"Liberation Mono", "DejaVu Sans Mono",
"Bitstream Vera Sans Mono", "Courier New",
monospace, sans-serif; font-size: 13px; vertical-align: baseline;
box-sizing: inherit; background-color: transparent; white-space:
inherit; color: var(--black-800); border-radius: 0px;"><br>
</code>
</body>
</html>