------------------------------------------------------------------------
-- The Agda standard library
--
-- Endomorphisms on a Set
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Endo.Propositional {a} (A : Set a) where
open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
open import Algebra.Core using (Op₁; Op₂)
import Algebra.Definitions.RawMonoid as RawMonoidDefinitions using (_×_)
import Algebra.Properties.Monoid.Mult as MonoidMultProperties using (×-homo-+)
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 (+-0-monoid; +-semigroup)
open import Data.Product.Base using (_,_)
open import Function.Base using (id; _∘′_; _∋_; flip)
open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
import Relation.Binary.PropositionalEquality.Properties as ≡
import Function.Endo.Setoid (≡.setoid A) as Setoid
------------------------------------------------------------------------
-- Basic type and raw bundles
Endo : Set a
Endo = A → A
private
_∘_ : Op₂ Endo
_∘_ = _∘′_
∘-id-rawMonoid : RawMonoid a a
∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≡_ ; _∙_ = _∘_ ; ε = id }
open RawMonoid ∘-id-rawMonoid
using ()
renaming (rawMagma to ∘-rawMagma)
------------------------------------------------------------------------
-- Conversion back and forth with the Setoid-based notion of Endomorphism
fromSetoidEndo : Setoid.Endo → Endo
fromSetoidEndo = _⟨$⟩_
toSetoidEndo : Endo → Setoid.Endo
toSetoidEndo f = record
{ to = f
; cong = cong f
}
------------------------------------------------------------------------
-- Structures
∘-isMagma : IsMagma _≡_ _∘_
∘-isMagma = record
{ isEquivalence = ≡.isEquivalence
; ∙-cong = cong₂ _∘_
}
∘-magma : Magma _ _
∘-magma = record { isMagma = ∘-isMagma }
∘-isSemigroup : IsSemigroup _≡_ _∘_
∘-isSemigroup = record
{ isMagma = ∘-isMagma
; assoc = λ _ _ _ → refl
}
∘-semigroup : Semigroup _ _
∘-semigroup = record { isSemigroup = ∘-isSemigroup }
∘-id-isMonoid : IsMonoid _≡_ _∘_ id
∘-id-isMonoid = record
{ isSemigroup = ∘-isSemigroup
; identity = (λ _ → refl) , (λ _ → refl)
}
∘-id-monoid : Monoid _ _
∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
------------------------------------------------------------------------
-- n-th iterated composition
infixr 8 _^_
_^_ : Endo → ℕ → Endo
_^_ = flip _×_ where open RawMonoidDefinitions ∘-id-rawMonoid using (_×_)
------------------------------------------------------------------------
-- Homomorphism
module _ (f : Endo) where
open MonoidMultProperties ∘-id-monoid using (×-homo-+)
^-homo : Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘_
^-homo = ×-homo-+ f
^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
^-isMagmaHomomorphism = record
{ isRelHomomorphism = record { cong = cong (f ^_) }
; homo = ^-homo
}
^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
^-isMonoidHomomorphism = record
{ isMagmaHomomorphism = ^-isMagmaHomomorphism
; ε-homo = refl
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4