From 866eee5bca2226e6316ade56bc5c4b442f225f53 Mon Sep 17 00:00:00 2001
From: Sam Speight <sspeight93@gmail.com>
Date: Tue, 21 May 2024 19:13:56 +0100
Subject: [PATCH] Add trivial implication

---
 source/UF/SystemFNotionOfResizing.lagda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/source/UF/SystemFNotionOfResizing.lagda b/source/UF/SystemFNotionOfResizing.lagda
index cf737971c..1f0fe6b9e 100644
--- a/source/UF/SystemFNotionOfResizing.lagda
+++ b/source/UF/SystemFNotionOfResizing.lagda
@@ -73,6 +73,10 @@ Propositional-System-F-Resizing =
   (P : A → Ω 𝓤₀) →
    (Ɐ x ꞉ A , P x) holds is 𝓤₀ small
 
+system-F-resizing-implies-prop-system-F-resizing
+ : System-F-Resizing → Propositional-System-F-Resizing
+system-F-resizing-implies-prop-system-F-resizing 𝕣 A P = 𝕣 A (_holds ∘ P)
+
 \end{code}
 
 The propositional version is of course trivially implied by propositional