From 1e2e4a05f8b900797785301ca6e8d374fd554709 Mon Sep 17 00:00:00 2001
From: Martin Escardo <m.escardo@cs.bham.ac.uk>
Date: Mon, 21 Oct 2024 15:32:07 +0100
Subject: [PATCH] minor improvement

---
 source/InjectiveTypes/Subtypes.lagda | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/source/InjectiveTypes/Subtypes.lagda b/source/InjectiveTypes/Subtypes.lagda
index fdbd997ce..8e6e98693 100644
--- a/source/InjectiveTypes/Subtypes.lagda
+++ b/source/InjectiveTypes/Subtypes.lagda
@@ -38,7 +38,10 @@ module _ (D : 𝓤 ̇ )
    r = retraction ρ
 
    s : Σ P → D
-   s = pr₁
+   s = section ρ
+
+   _ : s ＝ pr₁
+   _ = refl
 
    rs : r ∘ s ∼ id
    rs = retract-condition ρ