```------------------------------------------------------------------------
-- 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
open import Data.Product using (_,_)
open import Function.Base using (id; _∘_)
open import Function.Definitions
import Relation.Binary.Reasoning.Setoid as EqR

---------------------------------------------------------------------------------
-- 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 (f∘g=id , g∘f=id) homo x y = begin
g (x ∙₂ y)             ≈⟨ M₁.sym (g-cong (M₂.∙-cong (f∘g=id x) (f∘g=id y))) ⟩
g (f (g x) ∙₂ f (g y)) ≈⟨ M₁.sym (g-cong (homo (g x) (g y))) ⟩
g (f (g x ∙₁ g y))     ≈⟨ g∘f=id (g x ∙₁ g y) ⟩
g x ∙₁ g y             ∎
where open EqR 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ˡ (x ∙₂ y) ⟩
x ∙₂ y              ≈⟨ M₂.sym (M₂.∙-cong (invˡ x) (invˡ y)) ⟩
f (g x) ∙₂ f (g y)  ≈⟨ M₂.sym (homo (g x) (g y)) ⟩
f (g x ∙₁ g y)      ∎)
where open EqR M₂.setoid
```