From 7f72ed56fbc6840ef2e463ca4b3cf41f9bf12e62 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 15 Apr 2024 22:40:58 +0200
Subject: [PATCH] add test for regularity

---
 golden-tests/tests/regularity/expected        |  1 +
 golden-tests/tests/regularity/regularity.quox | 12 ++++++++++++
 golden-tests/tests/regularity/run             |  2 ++
 3 files changed, 15 insertions(+)
 create mode 100644 golden-tests/tests/regularity/expected
 create mode 100644 golden-tests/tests/regularity/regularity.quox
 create mode 100644 golden-tests/tests/regularity/run

diff --git a/golden-tests/tests/regularity/expected b/golden-tests/tests/regularity/expected
new file mode 100644
index 0000000..5b9502a
--- /dev/null
+++ b/golden-tests/tests/regularity/expected
@@ -0,0 +1 @@
+0.reggie : 1.(A : ★) → 1.(AA : A ≡ A : ★) → 1.(s : A) → 1.(P : 1.A → ★) → 1.(P (coe (𝑖 ⇒ AA @𝑖) @0 @1 s)) → P s
diff --git a/golden-tests/tests/regularity/regularity.quox b/golden-tests/tests/regularity/regularity.quox
new file mode 100644
index 0000000..9a06dc7
--- /dev/null
+++ b/golden-tests/tests/regularity/regularity.quox
@@ -0,0 +1,12 @@
+-- this definition depends on coercion regularity in xtt. which is this
+-- (adapted to quox):
+--
+--           Ψ | Γ ⊢ 0 · A‹0/𝑖› = A‹1/𝑖› ⇐ ★
+-- ---------------------------------------------------------
+--  Ψ | Γ ⊢ π · coe (𝑖 ⇒ A) @p @q s ⇝ (s ∷ A‹1/𝑖›) ⇒ A‹1/𝑖›
+--
+-- otherwise, the types P (coe ⋯ s) and P s are incompatible
+
+def0 reggie : (A : ★) → (AA : A ≡ A : ★) → (s : A) →
+              (P : A → ★) → P (coe (𝑖 ⇒ AA @𝑖) s) → P s =
+  λ A AA s P p ⇒ p
diff --git a/golden-tests/tests/regularity/run b/golden-tests/tests/regularity/run
new file mode 100644
index 0000000..cbfda48
--- /dev/null
+++ b/golden-tests/tests/regularity/run
@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" regularity.quox