Introduce the subuniverse P (#828)

UniMath · Oct 10, 2023 · df1669f · df1669f
1 parent d3f2e0c
commit df1669f
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
@@ -40,7 +40,8 @@ open import foundation.universe-levels
 
 The **Regensburg extension** of the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md)
-asserts that for any [pointed](structured-types.pointed-types.md)
+asserts that for any [subuniverse](foundation.subuniverses.md) `P`, and any
+[pointed](structured-types.pointed-types.md)
 [connected type](foundation.connected-types.md) `A` equipped with a type family
 `B` over `A`, the following are
 [logically equivalent](foundation.logical-equivalences.md):