minor improvement

martinescardo · Oct 21, 2024 · 1e2e4a0 · 1e2e4a0
1 parent 61a7059
commit 1e2e4a0
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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 ρ