------------------------------------------------------------------------
-- The Agda standard library
--
-- Endomorphisms on a Setoid
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (Setoid)

module Function.Endo.Setoid {c e} (S : Setoid c e) where

open import Agda.Builtin.Equality using (_≡_)

open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
import Algebra.Properties.Monoid.Mult as MonoidMultProperties
open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
open import Algebra.Morphism
  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
open Definitions using (Homomorphic₂)
open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
open import Data.Product.Base using (_,_)
open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
open import Function.Construct.Identity using () renaming (function to identity)
open import Function.Construct.Composition using () renaming (function to _∘_)
open import Function.Relation.Binary.Setoid.Equality as Eq using (_⇨_)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (_Preserves_⟶_)

private
  open module E = Setoid (S ⇨ S) hiding (refl)
  module S = Setoid S
  open Func using (cong)


------------------------------------------------------------------------
-- Basic type and raw bundles

Endo : Set _
Endo = S ⟶ₛ S

private
  id : Endo
  id = identity S

  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
  ∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≈_ ; _∙_ = _∘_ ; ε = id }

  open RawMonoid ∘-id-rawMonoid
    using ()
    renaming (rawMagma to ∘-rawMagma)

--------------------------------------------------------------
-- Structures

∘-isMagma : IsMagma _≈_ _∘_
∘-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = λ {_} {_} {_} {k} f≈g h≈k x → S.trans (h≈k _) (cong k (f≈g x))
  }

∘-magma : Magma (c ⊔ e) (c ⊔ e)
∘-magma = record { isMagma = ∘-isMagma }

∘-isSemigroup : IsSemigroup _≈_ _∘_
∘-isSemigroup = record
  { isMagma = ∘-isMagma
  ; assoc   = λ _ _ _ _ → S.refl
  }

∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
∘-semigroup = record { isSemigroup = ∘-isSemigroup }

∘-id-isMonoid : IsMonoid _≈_ _∘_ id
∘-id-isMonoid = record
  { isSemigroup = ∘-isSemigroup
  ; identity    = (λ _ _ → S.refl) , (λ _ _ → S.refl)
  }

∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
∘-id-monoid = record { isMonoid = ∘-id-isMonoid }

------------------------------------------------------------------------
-- -- n-th iterated composition

infixr  _^_

_^_ : Endo → ℕ → Endo
f ^ n = n × f where open RawMonoidDefinitions ∘-id-rawMonoid using (_×_)

------------------------------------------------------------------------
-- Homomorphism

module _ (f : Endo) where

  open MonoidMultProperties ∘-id-monoid using (×-congˡ; ×-homo-+)

  ^-cong₂ : (f ^_) Preserves _≡_ ⟶ _≈_
  ^-cong₂ = ×-congˡ {f}

  ^-homo : Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
  ^-homo = ×-homo-+ f

  ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
  ^-isMagmaHomomorphism = record
    { isRelHomomorphism = record { cong = ^-cong₂ }
    ; homo = ^-homo
    }

  ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
  ^-isMonoidHomomorphism = record
    { isMagmaHomomorphism = ^-isMagmaHomomorphism
    ; ε-homo = λ _ → S.refl
    }