Merge pull request #464 from jacquescomeaux/missing-merge-combinators

Minor reasoning combinator updates

Author: JacquesCarette

src/Categories/Category/Monoidal/Reasoning.agda

@@ -135,7 +135,15 @@ split₂ˡ {f = f} {g} {h} = begin
   id ⊗₁ g ∘ f ⊗₁ h      ∎
 
 -- The opposite, i.e. merge
-merge₂ʳ :  ∀ {X₁ Y₁ X₂ Y₂ Z₂} {f : X₁ ⇒ Y₁} {g : Y₂ ⇒ Z₂} {h : X₂ ⇒ Y₂} →
+merge₁ʳ : ∀ {X₁ Y₁ Z₁ X₂ Y₂} {f : Y₁ ⇒ Z₁} {g : X₁ ⇒ Y₁} {h : X₂ ⇒ Y₂} →
+          f ⊗₁ h ∘ g ⊗₁ id ≈ (f ∘ g) ⊗₁ h
+merge₁ʳ = Equiv.sym split₁ʳ
+
+merge₁ˡ : ∀ {X₁ Y₁ Z₁ X₂ Y₂} {f : Y₁ ⇒ Z₁} {g : X₁ ⇒ Y₁} {h : X₂ ⇒ Y₂} →
+          f ⊗₁ id ∘ g ⊗₁ h ≈ (f ∘ g) ⊗₁ h
+merge₁ˡ = Equiv.sym split₁ˡ
+
+merge₂ʳ : ∀ {X₁ Y₁ X₂ Y₂ Z₂} {f : X₁ ⇒ Y₁} {g : Y₂ ⇒ Z₂} {h : X₂ ⇒ Y₂} →
           f ⊗₁ g ∘ id ⊗₁ h ≈ f ⊗₁ (g ∘ h)
 merge₂ʳ = Equiv.sym split₂ʳ
 

src/Categories/Morphism/Reasoning/Core.agda

@@ -309,8 +309,8 @@ pull-first {f = f} {g = g} {a = a} {h = h} {i = i} eq = begin
 pull-center : g ∘ h ≈ a → f ∘ (g ∘ (h ∘ i)) ≈ f ∘ (a ∘ i)
 pull-center eq = ∘-resp-≈ʳ (pullˡ eq)
 
-push-center : g ∘ h ≈ a → f ∘ (a ∘ i) ≈ f ∘ (g ∘ (h ∘ i))
-push-center eq = Equiv.sym (pull-center eq)
+push-center : a ≈ g ∘ h → f ∘ (a ∘ i) ≈ f ∘ (g ∘ (h ∘ i))
+push-center eq = Equiv.sym (pull-center (Equiv.sym eq))
 
 intro-first : a ∘ b ≈ id → f ∘ g ≈ a ∘ ((b ∘ f) ∘ g)
 intro-first {a = a} {b = b} {f = f} {g = g} eq = begin