Fix argument order of composition operators (#2121)

Author: MatthewDaggitt

CHANGELOG.md

@@ -29,6 +29,10 @@ Highlights
 Bug-fixes
 ---------
 
+* The combinators `_⟶-∘_`, `_↣-∘_`, `_↠-∘_`, `_⤖-∘_`, `_⇔-∘_`, `_↩-∘_`, `_↪-∘_`, `_↔-∘_`
+  in `Function.Construct.Composition` had their arguments in the wrong order. They have
+  been flipped so they can actually be used as a composition operator.
+
 * The following operators were missing a fixity declaration, which has now
   been fixed -
   ```

src/Data/Fin/Permutation.agda

@@ -104,7 +104,7 @@ reverse = permutation opposite opposite PC.reverse-involutive PC.reverse-involut
 
 infixr 9 _∘ₚ_
 _∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
-π₁ ∘ₚ π₂ = π₁ ↔-∘ π₂
+π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁
 
 -- Flip
 

src/Function/Construct/Composition.agda

@@ -9,7 +9,7 @@
 module Function.Construct.Composition where
 
 open import Data.Product.Base as Product using (_,_)
-open import Function.Base using (_∘_)
+open import Function.Base using (_∘_; flip)
 open import Function.Bundles
 open import Function.Definitions
 open import Function.Structures
@@ -199,31 +199,33 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
 ------------------------------------------------------------------------
 -- Propositional bundles
 
+-- Notice the flipped order of the arguments to mirror composition.
+
 infix 8 _⟶-∘_ _↣-∘_ _↠-∘_ _⤖-∘_ _⇔-∘_ _↩-∘_ _↪-∘_ _↔-∘_
 
-_⟶-∘_ : (A ⟶ B) → (B ⟶ C) → (A ⟶ C)
-_⟶-∘_ = function
+_⟶-∘_ : (B ⟶ C) → (A ⟶ B) → (A ⟶ C)
+_⟶-∘_ = flip function
 
-_↣-∘_ : A ↣ B → B ↣ C → A ↣ C
-_↣-∘_ = injection
+_↣-∘_ : B ↣ C → A ↣ B → A ↣ C
+_↣-∘_ = flip injection
 
-_↠-∘_ : A ↠ B → B ↠ C → A ↠ C
-_↠-∘_ = surjection
+_↠-∘_ : B ↠ C → A ↠ B → A ↠ C
+_↠-∘_ = flip surjection
 
-_⤖-∘_ : A ⤖ B → B ⤖ C → A ⤖ C
-_⤖-∘_ = bijection
+_⤖-∘_ : B ⤖ C → A ⤖ B → A ⤖ C
+_⤖-∘_ = flip bijection
 
-_⇔-∘_ : A ⇔ B → B ⇔ C → A ⇔ C
-_⇔-∘_ = equivalence
+_⇔-∘_ : B ⇔ C → A ⇔ B → A ⇔ C
+_⇔-∘_ = flip equivalence
 
-_↩-∘_ : A ↩ B → B ↩ C → A ↩ C
-_↩-∘_ = leftInverse
+_↩-∘_ : B ↩ C → A ↩ B → A ↩ C
+_↩-∘_ = flip leftInverse
 
-_↪-∘_  : A ↪ B → B ↪ C → A ↪ C
-_↪-∘_ = rightInverse
+_↪-∘_  : B ↪ C → A ↪ B → A ↪ C
+_↪-∘_ = flip rightInverse
 
-_↔-∘_ : A ↔ B → B ↔ C → A ↔ C
-_↔-∘_ = inverse
+_↔-∘_ : B ↔ C → A ↔ B → A ↔ C
+_↔-∘_ = flip inverse
 
 
 ------------------------------------------------------------------------

src/Function/Properties/Inverse.agda

@@ -55,7 +55,7 @@ isEquivalence = record
 ↔-sym = Symmetry.↔-sym
 
 ↔-trans : A ↔ B → B ↔ C → A ↔ C
-↔-trans = Composition._↔-∘_
+↔-trans = Composition.inverse
 
 -- need to η-expand for everything to line up properly
 ↔-isEquivalence : IsEquivalence {ℓ = ℓ} _↔_

src/Function/Related/Propositional.agda

@@ -256,14 +256,14 @@ K-reflexive P.refl = K-refl
 K-trans : Trans (Related {a} {b} k)
                 (Related {b} {c} k)
                 (Related {a} {c} k)
-K-trans {k = implication}        = Composition._⟶-∘_
-K-trans {k = reverseImplication} = flip Composition._⟶-∘_
-K-trans {k = equivalence}        = Composition._⇔-∘_
-K-trans {k = injection}          = Composition._↣-∘_
-K-trans {k = reverseInjection}   = flip Composition._↣-∘_
-K-trans {k = leftInverse}        = Composition._↪-∘_
-K-trans {k = surjection}         = Composition._↠-∘_
-K-trans {k = bijection}          = Composition._↔-∘_
+K-trans {k = implication}        = flip Composition._⟶-∘_
+K-trans {k = reverseImplication} = Composition._⟶-∘_
+K-trans {k = equivalence}        = flip Composition._⇔-∘_
+K-trans {k = injection}          = flip Composition._↣-∘_
+K-trans {k = reverseInjection}   = Composition._↣-∘_
+K-trans {k = leftInverse}        = flip Composition._↪-∘_
+K-trans {k = surjection}         = flip Composition._↠-∘_
+K-trans {k = bijection}          = flip Composition._↔-∘_
 
 SK-sym : ∀ {k} → Sym (Related {a} {b} ⌊ k ⌋)
                      (Related {b} {a} ⌊ k ⌋)