    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some properties of Magma homomorphisms
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Algebra.Morphism.Consequences where

    open import Algebra using (Magma)
    open import Algebra.Morphism.Definitions using (Homomorphic₂)
    open import Data.Product.Base using (_,_)
    open import Function.Base using (id; _∘_)
    open import Function.Definitions
      using (Injective; Congruent; Inverseᵇ; Inverseˡ)
    import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

    ------------------------------------------------------------------------
    -- If f and g are mutually inverse maps between A and B, g is congruent,
    -- f is a homomorphism, then g is a homomorphism.

    module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where

      private
        open module M₁ = Magma M₁ using () renaming (_≈_ to _≈₁_; _∙_ to _∙₁_)
        open module M₂ = Magma M₂ using () renaming (_≈_ to _≈₂_; _∙_ to _∙₂_)

      homomorphic₂-inv  : ∀ {f g} → Congruent _≈₂_ _≈₁_ g →
                          Inverseᵇ _≈₁_ _≈₂_ f g →
                          Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_  →
                          Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_
      homomorphic₂-inv {f} {g} g-cong (invˡ , invʳ) homo x y = begin
        g (x ∙₂ y)             ≈⟨ g-cong (M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl)) ⟨
        g (f (g x) ∙₂ f (g y)) ≈⟨ g-cong (homo (g x) (g y)) ⟨
        g (f (g x ∙₁ g y))     ≈⟨ invʳ M₂.refl ⟩
        g x ∙₁ g y             ∎
        where open ≈-Reasoning M₁.setoid

      homomorphic₂-inj  : ∀ {f g} → Injective _≈₁_ _≈₂_ f →
                          Inverseˡ _≈₁_ _≈₂_ f g →
                          Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_  →
                          Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_
      homomorphic₂-inj {f} {g} inj invˡ homo x y = inj (begin
        f (g (x ∙₂ y))      ≈⟨ invˡ M₁.refl ⟩
        x ∙₂ y              ≈⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟨
        f (g x) ∙₂ f (g y)  ≈⟨ homo (g x) (g y) ⟨
        f (g x ∙₁ g y)      ∎)
        where open ≈-Reasoning M₂.setoid