From f00c802336e29154b8d02ba7bbec5a9d1d638adc Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 2 Jun 2024 17:35:56 +0200
Subject: [PATCH] functions returning subsings are also subsings

---
 golden-tests/tests/isprop-subsing/expected            | 2 ++
 golden-tests/tests/isprop-subsing/isprop-subsing.quox | 4 ++++
 golden-tests/tests/isprop-subsing/run                 | 2 ++
 3 files changed, 8 insertions(+)
 create mode 100644 golden-tests/tests/isprop-subsing/expected
 create mode 100644 golden-tests/tests/isprop-subsing/isprop-subsing.quox
 create mode 100644 golden-tests/tests/isprop-subsing/run

diff --git a/golden-tests/tests/isprop-subsing/expected b/golden-tests/tests/isprop-subsing/expected
new file mode 100644
index 0000000..8fbea7a
--- /dev/null
+++ b/golden-tests/tests/isprop-subsing/expected
@@ -0,0 +1,2 @@
+0.IsProp : 1.★ → ★
+0.feq : 1.(A : ★) → 1.(f : IsProp A) → 1.(g : IsProp A) → f ≡ g : IsProp A
diff --git a/golden-tests/tests/isprop-subsing/isprop-subsing.quox b/golden-tests/tests/isprop-subsing/isprop-subsing.quox
new file mode 100644
index 0000000..2117d08
--- /dev/null
+++ b/golden-tests/tests/isprop-subsing/isprop-subsing.quox
@@ -0,0 +1,4 @@
+def0 IsProp : ★ → ★ = λ A ⇒ (x y : A) → x ≡ y : A
+
+def0 feq : (A : ★) → (f g : IsProp A) → f ≡ g : IsProp A =
+  λ A f g ⇒ δ _ ⇒ f
diff --git a/golden-tests/tests/isprop-subsing/run b/golden-tests/tests/isprop-subsing/run
new file mode 100644
index 0000000..feb762b
--- /dev/null
+++ b/golden-tests/tests/isprop-subsing/run
@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" isprop-subsing.quox