Skip to content

Commit 8efb15d

Browse files
committed
fix: exports from Surjection and Bijection
1 parent 520b838 commit 8efb15d

File tree

1 file changed

+7
-1
lines changed

1 file changed

+7
-1
lines changed

src/Function/Bundles.agda

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
113113
using
114114
( strictlySurjective
115115
; section
116+
; section-inverseˡ
116117
; section-strictInverseˡ
117118
)
118119

@@ -158,7 +159,12 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
158159
open Injection injection public
159160
using (isInjection)
160161
open Surjection surjection public
161-
using (isSurjection; section; to∘to⁻; strictlySurjective)
162+
using (isSurjection
163+
; strictlySurjective
164+
; section
165+
; section-inverseˡ
166+
; section-strictInverseˡ
167+
)
162168

163169
isBijection : IsBijection to
164170
isBijection = record

0 commit comments

Comments
 (0)