```------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic structures
------------------------------------------------------------------------

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

module Algebra.Morphism where

import Algebra.Morphism.Definitions as MorphismDefinitions
open import Algebra
import Algebra.Properties.Group as GroupP
open import Function hiding (Morphism)
open import Level
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as EqR

private
variable
a b ℓ₁ ℓ₂ : Level
A : Set a
B : Set b

------------------------------------------------------------------------
-- Re-export

module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where
open MorphismDefinitions A B _≈_ public

open import Algebra.Morphism.Structures public

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new definitions re-exported from
-- `Algebra.Morphism.Structures` as continuing support for the below is
-- no guaranteed.

-- Version 1.5

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Semigroup c₁ ℓ₁)
(To   : Semigroup c₂ ℓ₂) where

private
module F = Semigroup From
module T = Semigroup To
open Definitions F.Carrier T.Carrier T._≈_

record IsSemigroupMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_

IsSemigroupMorphism-syntax = IsSemigroupMorphism
syntax IsSemigroupMorphism-syntax From To F = F Is From -Semigroup⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Monoid c₁ ℓ₁)
(To   : Monoid c₂ ℓ₂) where

private
module F = Monoid From
module T = Monoid To
open Definitions F.Carrier T.Carrier T._≈_

record IsMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧
ε-homo  : Homomorphic₀ ⟦_⟧ F.ε T.ε

open IsSemigroupMorphism sm-homo public

IsMonoidMorphism-syntax = IsMonoidMorphism
syntax IsMonoidMorphism-syntax From To F = F Is From -Monoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : CommutativeMonoid c₁ ℓ₁)
(To   : CommutativeMonoid c₂ ℓ₂) where

private
module F = CommutativeMonoid From
module T = CommutativeMonoid To
open Definitions F.Carrier T.Carrier T._≈_

record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

open IsMonoidMorphism mn-homo public

IsCommutativeMonoidMorphism-syntax = IsCommutativeMonoidMorphism
syntax IsCommutativeMonoidMorphism-syntax From To F = F Is From -CommutativeMonoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : IdempotentCommutativeMonoid c₁ ℓ₁)
(To   : IdempotentCommutativeMonoid c₂ ℓ₂) where

private
module F = IdempotentCommutativeMonoid From
module T = IdempotentCommutativeMonoid To
open Definitions F.Carrier T.Carrier T._≈_

record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

open IsMonoidMorphism mn-homo public

isCommutativeMonoidMorphism :
IsCommutativeMonoidMorphism F.commutativeMonoid T.commutativeMonoid ⟦_⟧
isCommutativeMonoidMorphism = record { mn-homo = mn-homo }

IsIdempotentCommutativeMonoidMorphism-syntax = IsIdempotentCommutativeMonoidMorphism
syntax IsIdempotentCommutativeMonoidMorphism-syntax From To F = F Is From -IdempotentCommutativeMonoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Group c₁ ℓ₁)
(To   : Group c₂ ℓ₂) where

private
module F = Group From
module T = Group To
open Definitions F.Carrier T.Carrier T._≈_

record IsGroupMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

open IsMonoidMorphism mn-homo public

⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ \$ begin
⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
⟦ x F.⁻¹ F.∙ x ⟧     ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
⟦ F.ε ⟧              ≈⟨ ε-homo ⟩
T.ε ∎

IsGroupMorphism-syntax = IsGroupMorphism
syntax IsGroupMorphism-syntax From To F = F Is From -Group⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : AbelianGroup c₁ ℓ₁)
(To   : AbelianGroup c₂ ℓ₂) where

private
module F = AbelianGroup From
module T = AbelianGroup To
open Definitions F.Carrier T.Carrier T._≈_

record IsAbelianGroupMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
gp-homo : IsGroupMorphism F.group T.group ⟦_⟧

open IsGroupMorphism gp-homo public

IsAbelianGroupMorphism-syntax = IsAbelianGroupMorphism
syntax IsAbelianGroupMorphism-syntax From To F = F Is From -AbelianGroup⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Ring c₁ ℓ₁)
(To   : Ring c₂ ℓ₂) where

private
module F = Ring From
module T = Ring To
open Definitions F.Carrier T.Carrier T._≈_

record IsRingMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
+-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup
*-mn-homo   : ⟦_⟧ Is F.*-monoid -Monoid⟶ T.*-monoid

IsRingMorphism-syntax = IsRingMorphism
syntax IsRingMorphism-syntax From To F = F Is From -Ring⟶ To

{-# WARNING_ON_USAGE IsSemigroupMorphism
"Warning: IsSemigroupMorphism was deprecated in v1.5.
#-}
{-# WARNING_ON_USAGE IsMonoidMorphism
"Warning: IsMonoidMorphism was deprecated in v1.5.
#-}
{-# WARNING_ON_USAGE IsCommutativeMonoidMorphism
"Warning: IsCommutativeMonoidMorphism was deprecated in v1.5.
#-}
{-# WARNING_ON_USAGE IsIdempotentCommutativeMonoidMorphism
"Warning: IsIdempotentCommutativeMonoidMorphism was deprecated in v1.5.