From fd89b1f2a9d35258c37f3cf678c036a9644facbf Mon Sep 17 00:00:00 2001
From: GenericMonkey <pransrin@umich.edu>
Date: Fri, 21 Jul 2023 11:16:42 -0400
Subject: [PATCH] adding another example

---
 Cubical/Reflection/RecordEquiv/More.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Cubical/Reflection/RecordEquiv/More.agda b/Cubical/Reflection/RecordEquiv/More.agda
index a743fa66..0610ba4c 100644
--- a/Cubical/Reflection/RecordEquiv/More.agda
+++ b/Cubical/Reflection/RecordEquiv/More.agda
@@ -54,3 +54,21 @@ module _ where private
 
   foo-iso : Iso Foo (∀{A} → Baz A)
   unquoteDef foo-iso = defineRecordIsoΣ foo-iso (quote Foo)
+
+module _ where private
+  Bar : ℕ → Type
+  Bar 0 = Unit
+  Bar _ = ℕ
+
+  record Foo {n : ℕ} (b : Bar n) : Type where
+    field
+      foo : {a : ℕ} → Bar a
+      baz : Bar n
+      goo : b ≡ baz
+
+  Sigma : {n : ℕ} (b : Bar n) → Type
+  Sigma {n} b = Σ ({a : ℕ} → Bar a) (λ z → Σ (Bar n) (PathP (λ i → Bar n) b))
+
+  foo-iso : ∀ {x : ℕ} {b : Bar x} → Iso (Foo b) (Sigma b)
+  unquoteDef foo-iso = defineRecordIsoΣ foo-iso (quote Foo)
+