Add trivial implication

martinescardo · May 21, 2024 · 866eee5 · 866eee5
1 parent f0431d1
commit 866eee5
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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