From df1669f443cdcde4910937dc0f368e43b6dbd9cf Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Tue, 10 Oct 2023 23:56:18 +0200 Subject: [PATCH] Introduce the subuniverse P (#828) --- ...rg-extension-fundamental-theorem-of-identity-types.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 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 index 3e8347a4c7..2d00f2c7ce 100644 --- 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):