fixes agda#2568

Author: jamesmckinna

src/Data/Product/Function/Dependent/Propositional.agda

@@ -57,7 +57,7 @@ module _ where
          Σ I A ⇔ Σ J B
   Σ-⇔ {B = B} I↠J A⇔B = mk⇔
     (map (to  I↠J) (Equivalence.to A⇔B))
-    (map (to⁻ I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))
+    (map (section I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))
 
   -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣.
 
@@ -193,16 +193,16 @@ module _ where
     to′ : Σ I A → Σ J B
     to′ = map (to I↠J) (to A↠B)
 
-    backcast : ∀ {i} → B i → B (to I↠J (to⁻ I↠J i))
+    backcast : ∀ {i} → B i → B (to I↠J (section I↠J i))
     backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _))
 
     to⁻′ : Σ J B → Σ I A
-    to⁻′ = map (to⁻ I↠J) (Surjection.to⁻ A↠B ∘ backcast)
+    to⁻′ = map (section I↠J) (Surjection.section A↠B ∘ backcast)
 
     strictlySurjective′ : StrictlySurjective _≡_ to′
     strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡
       ( to∘to⁻ I↠J x
-      , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (to⁻ A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩
+      , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (section A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩
          ≡.subst B (to∘to⁻ I↠J x) (backcast y)                      ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩
          y                                                          ∎)
       ) where open ≡.≡-Reasoning
@@ -249,7 +249,7 @@ module _ where
       Σ I A ↔ Σ J B
   Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′
     (Surjection.to surjection′)
-    (Surjection.to⁻ surjection′)
+    (Surjection.section surjection′)
     (Surjection.to∘to⁻ surjection′)
     left-inverse-of
     where
@@ -260,7 +260,7 @@ module _ where
     surjection′ : Σ I A ↠ Σ J B
     surjection′ = Σ-↠ (↔⇒↠ (≃⇒↔ I≃J)) (↔⇒↠ A↔B)
 
-    left-inverse-of : ∀ p → Surjection.to⁻ surjection′ (Surjection.to surjection′ p) ≡ p
+    left-inverse-of : ∀ p → Surjection.section surjection′ (Surjection.to surjection′ p) ≡ p
     left-inverse-of (x , y) = to Σ-≡,≡↔≡
       ( _≃_.left-inverse-of I≃J x
       , (≡.subst A (_≃_.left-inverse-of I≃J x)

src/Data/Product/Function/Dependent/Setoid.agda

@@ -117,7 +117,7 @@ module _ where
     B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x))
     B-to = toFunction A⇔B
 
-    B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.to⁻ I↠J y))
+    B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.section I↠J y))
     B-from = record
       { to   = from      A⇔B ∘ cast      B (Surjection.to∘to⁻ I↠J _)
       ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _)
@@ -169,7 +169,7 @@ module _ where
     func = function (Surjection.function I↠J) (Surjection.function A↠B)
 
     to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
-    to⁻′ (j , y) = to⁻ I↠J j , to⁻ A↠B (cast B (Surjection.to∘to⁻ I↠J _) y)
+    to⁻′ (j , y) = section I↠J j , section A↠B (cast B (Surjection.to∘to⁻ I↠J _) y)
 
     strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func)
     strictlySurj (j , y) = to⁻′ (j , y) ,

src/Function/Bundles.agda

@@ -113,12 +113,17 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     open IsSurjection isSurjection public
       using
       ( strictlySurjective
+      ; section
       )
 
     to⁻ : B → A
     to⁻ = proj₁ ∘ surjective
+    {-# WARNING_ON_USAGE to⁻
+    "Warning: to⁻ was deprecated in v2.3.
+    Please use Function.Structures.IsSurjection.section instead. "
+    #-}
 
-    to∘to⁻ : ∀ x → to (to⁻ x) ≈₂ x
+    to∘to⁻ : ∀ x → to (section x) ≈₂ x
     to∘to⁻ = proj₂ ∘ strictlySurjective
 
 
@@ -146,8 +151,10 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; surjective = surjective
       }
 
-    open Injection  injection  public using (isInjection)
-    open Surjection surjection public using (isSurjection; to⁻;  strictlySurjective)
+    open Injection  injection  public
+      using (isInjection)
+    open Surjection surjection public
+      using (isSurjection; section; to∘to⁻; strictlySurjective)
 
     isBijection : IsBijection to
     isBijection = record

src/Function/Construct/Composition.agda

@@ -40,9 +40,10 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
 
   surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
                Surjective ≈₁ ≈₃ (g ∘ f)
-  surjective f-sur g-sur x with g-sur x
-  ... | y , gproof with f-sur y
-  ...   | z , fproof = z , gproof ∘ fproof
+  surjective f-sur g-sur x =
+    let y , gproof = g-sur x in
+    let z , fproof = f-sur y in
+        z , gproof ∘ fproof
 
   bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
               Bijective ≈₁ ≈₃ (g ∘ f)

src/Function/Construct/Symmetry.agda

@@ -71,15 +71,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
 
   private
     module IB = IsBijection isBij
-    f⁻¹       = proj₁ ∘ IB.surjective
 
   -- We can only flip a bijection if the witness produced by the
   -- surjection proof respects the equality on the codomain.
-  isBijection : Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹
-  isBijection f⁻¹-cong = record
+  isBijection : Congruent ≈₂ ≈₁ IB.section → IsBijection ≈₂ ≈₁ IB.section
+  isBijection section-cong = record
     { isInjection = record
       { isCongruent = record
-        { cong           = f⁻¹-cong
+        { cong           = section-cong
         ; isEquivalence₁ = IB.Eq₂.isEquivalence
         ; isEquivalence₂ = IB.Eq₁.isEquivalence
         }
@@ -93,7 +92,7 @@ module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_
   -- We can always flip a bijection if using the equality over the
   -- codomain is propositional equality.
   isBijection-≡ : IsBijection _≡_ ≈₁ _
-  isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong _)
+  isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong IB.section)
     where module IB = IsBijection isBij
 
 module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : B → A} where
@@ -132,13 +131,12 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where
 
   private
     module IB = Bijection bij
-    from      = proj₁ ∘ IB.surjective
 
   -- We can only flip a bijection if the witness produced by the
   -- surjection proof respects the equality on the codomain.
-  bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ from → Bijection S R
+  bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ IB.section → Bijection S R
   bijection cong = record
-    { to        = from
+    { to        = IB.section
     ; cong      = cong
     ; bijective = bijective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
     }
@@ -191,7 +189,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 -- Propositional bundles
 
 ⤖-sym : A ⤖ B → B ⤖ A
-⤖-sym b = bijection b (cong _)
+⤖-sym b = bijection b (cong section) where open Bijection b using (section)
 
 ⇔-sym : A ⇔ B → B ⇔ A
 ⇔-sym = equivalence

src/Function/Properties/Bijection.agda

@@ -60,13 +60,13 @@ trans = Composition.bijection
 Bijection⇒Inverse : Bijection S T → Inverse S T
 Bijection⇒Inverse bij = record
   { to        = to
-  ; from      = to⁻
+  ; from      = section
   ; to-cong   = cong
   ; from-cong = injective⇒to⁻-cong surjection injective
   ; inverse   = (λ y≈to⁻[x] → Eq₂.trans (cong y≈to⁻[x]) (to∘to⁻ _)) ,
                 (λ y≈to[x] → injective (Eq₂.trans (to∘to⁻ _) y≈to[x]))
   }
-  where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective
+  where open Bijection bij
 
 Bijection⇒Equivalence : Bijection T S → Equivalence T S
 Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse

src/Function/Properties/Surjection.agda

@@ -45,11 +45,11 @@ mkSurjection f surjective = record
 ↠⇒⟶ = Surjection.function
 
 ↠⇒↪ : A ↠ B → B ↪ A
-↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → proj₂ (strictlySurjective _)}
+↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → to∘to⁻ _ }
   where open Surjection s
 
 ↠⇒⇔ : A ↠ B → A ⇔ B
-↠⇒⇔ s = mk⇔ to (proj₁ ∘ surjective)
+↠⇒⇔ s = mk⇔ to section
   where open Surjection s
 
 ------------------------------------------------------------------------
@@ -69,12 +69,12 @@ trans = Compose.surjection
 injective⇒to⁻-cong : (surj : Surjection S T) →
                       (open Surjection surj) →
                       Injective Eq₁._≈_ Eq₂._≈_ to →
-                      Congruent Eq₂._≈_ Eq₁._≈_ to⁻
+                      Congruent Eq₂._≈_ Eq₁._≈_ section
 injective⇒to⁻-cong {T = T} surj injective {x} {y} x≈y = injective $ begin
-  to (to⁻ x) ≈⟨ to∘to⁻ x ⟩
-  x          ≈⟨ x≈y ⟩
-  y          ≈⟨ to∘to⁻ y ⟨
-  to (to⁻ y) ∎
+  to (section x) ≈⟨ to∘to⁻ x ⟩
+  x              ≈⟨ x≈y ⟩
+  y              ≈⟨ to∘to⁻ y ⟨
+  to (section y) ∎
   where
   open ≈-Reasoning T
   open Surjection surj

src/Function/Structures.agda

@@ -17,7 +17,7 @@ module Function.Structures {a b ℓ₁ ℓ₂}
   {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
-open import Data.Product.Base as Product using (∃; _×_; _,_)
+open import Data.Product.Base as Product using (∃; _×_; _,_; proj₁; proj₂)
 open import Function.Base
 open import Function.Definitions
 open import Level using (_⊔_)
@@ -69,6 +69,12 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   strictlySurjective : StrictlySurjective _≈₂_ f
   strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x)
 
+  section : B → A
+  section = proj₁ ∘ surjective
+
+  section-inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section
+  section-inverseˡ = λ y≈fx → (proj₂ ∘ surjective) _ y≈fx
+
 
 record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -87,7 +93,7 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     }
 
   open IsSurjection isSurjection public
-    using (strictlySurjective)
+    using (strictlySurjective; section)
 
 
 ------------------------------------------------------------------------