refactor: propagate exports of new lemmas

Author: jamesmckinna

src/Function/Bundles.agda

@@ -172,7 +172,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; surjective  = surjective
       }
 
-    open IsBijection isBijection public using (module Eq₁; module Eq₂)
+    open IsBijection isBijection public
+      using (module Eq₁; module Eq₂; inverseʳ; strictlyInverseʳ)
 
 
 ------------------------------------------------------------------------

src/Function/Structures.agda

@@ -97,6 +97,14 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   open IsSurjection isSurjection public
     using (strictlySurjective; section; inverseˡ; strictlyInverseˡ)
 
+  private module S = Section _≈₂_ surjective
+
+  inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section
+  inverseʳ = S.inverseʳ injective Eq₁.refl Eq₂.trans
+
+  strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f
+  strictlyInverseʳ = S.strictlyInverseʳ injective Eq₁.refl Eq₂.trans
+
 
 ------------------------------------------------------------------------
 -- Two element structures