Relations
{-# OPTIONS --allow-unsolved-metas --without-K #-} open import Level using (Level; Lift) import Level as L open import Relation.Binary using (Rel; Decidable; Symmetric; Reflexive; Transitive; IsEquivalence) import Relation.Binary.PropositionalEquality as ≡ open import Relation.Binary.PropositionalEquality using (_≡_; _≗_) open import Function.Base module Relation where private variable ℓ ℓ' ℓ'' : Level A : Set ℓ B : Set ℓ' C : Set ℓ''
Equivalence Closure
_⊆_ : (S : Rel A ℓ') (R : Rel A ℓ'') → Set _ _⊆_ S R = ∀ {x} {y} → S x y → R x y data Reflexive-Closure {A : Set ℓ} (R : A → A → Set ℓ') : A → A → Set (ℓ L.⊔ ℓ') where in-R : ∀ {x} {y} → R x y → Reflexive-Closure R x y Δ : ∀ {x} → Reflexive-Closure R x x refl-ump : {A : Set ℓ} {S R : A → A → Set ℓ'} → R ⊆ S → Reflexive S → (Reflexive-Closure R) ⊆ S refl-ump R⊆S S-refl (in-R Rxy) = R⊆S Rxy refl-ump R⊆S S-refl Δ = S-refl data Equiv-Closure {A : Set ℓ} (R : A → A → Set ℓ') : A → A → Set (ℓ L.⊔ ℓ') where in-R : ∀ {x} {y} → R x y → Equiv-Closure R x y reflC : ∀ {x} → Equiv-Closure R x x symC : ∀ {x} {y} → R x y → Equiv-Closure R y x transC : ∀ {x} {y} {z} → Equiv-Closure R x y → Equiv-Closure R y z → Equiv-Closure R x z Equiv-Closure-sym : ∀(R : A → A → Set ℓ') → Symmetric (Equiv-Closure R) Equiv-Closure-sym R (in-R Rxy) = symC Rxy Equiv-Closure-sym R reflC = reflC Equiv-Closure-sym R (symC Rxy) = in-R Rxy Equiv-Closure-sym R (transC Rxy Ryz) = transC (Equiv-Closure-sym R Ryz) (Equiv-Closure-sym R Rxy)
Ende der Vorlesung am 08.Juni 2026
Equiv-Closure-IsEquivalence : ∀(R : A → A → Set ℓ') → IsEquivalence (Equiv-Closure R) Equiv-Closure-IsEquivalence R = record { refl = reflC ; sym = Equiv-Closure-sym R ; trans = transC } module Equiv-UMP {ℓ' ℓ'' : Level} (R : A → A → Set ℓ') (S : A → A → Set ℓ'') (S-Equiv : IsEquivalence S) (R⊆S : R ⊆ S) where open IsEquivalence S-Equiv ump : (Equiv-Closure R) ⊆ S ump (in-R Rxy) = R⊆S Rxy ump reflC = refl ump (symC Rxy) = sym (R⊆S Rxy) ump (transC R*xy R*yz) = trans (ump R*xy) (ump R*yz)
Closure Operator
module Closure (X : Set ℓ) (_≤_ : Rel X ℓ') where record _closure (P : X → Set ℓ'') : Set (ℓ L.⊔ ℓ' L.⊔ ℓ'') where field cl : X → X extensive : ∀ x → x ≤ cl x cl-prop : ∀ x → P (cl x) ump : ∀ x y → P y → x ≤ y → cl x ≤ y monotone : Transitive _≤_ → ∀ x y → x ≤ y → cl x ≤ cl y monotone ≤-trans x y x≤y = ump x (cl y) (cl-prop y) (≤-trans x≤y (extensive y)) idempotent : Reflexive _≤_ → ∀ x → P x → cl x ≤ x idempotent ≤-refl x x∈P = ump x x x∈P ≤-refl module Example {A : Set ℓ} where open Closure (Rel A ℓ) _⊆_ example-equiv-closure : IsEquivalence closure example-equiv-closure = record { cl = Equiv-Closure ; extensive = λ R Rxy → in-R Rxy ; cl-prop = Equiv-Closure-IsEquivalence ; ump = Equiv-UMP.ump }
Ende der Vorlesung am 11. Juni 2026
Pointwise Equality of Functions
module Pointwise-Equality {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} where _≐_ : (X → Y) → (X → Y) → Set (ℓ L.⊔ ℓ') _≐_ f g = ∀ x → f x ≡ g x ≡→≐ : ∀ f g → f ≡ g → f ≐ g ≡→≐ f g ≡.refl x = ≡.refl FunctionalExtensionality : Set (ℓ L.⊔ ℓ') FunctionalExtensionality = ∀ f g → f ≐ g → f ≡ g ≐-equiv : IsEquivalence _≐_ ≐-equiv = record { refl = λ { f → ≡.refl } ; sym = λ {f} {g} eq x → ≡.sym (eq x) ; trans = λ {f} {g} {h} eq1 eq2 x → ≡.trans (eq1 x) (eq2 x) } module example where open import Data.Nat open import Data.Unit open Pointwise-Equality postulate ext : FunctionalExtensionality {L.0ℓ} {L.0ℓ} {⊤} {⊤} context : (⊤ → ⊤) → Set context _ = ℕ two : ℕ two = ≡.subst context (ext (λ x → tt) (λ x → tt) λ x → ≡.refl) 2 -- test : two ≡ 2 -- test = ≡.refl -- ≡.subst context (ext (λ x → tt) (λ x → tt) (λ x → ≡.refl)) 2 != 2 -- of type ℕ -- when checking that the expression ≡.refl has type two ≡ 2
Coequalizer
open import Data.Product using (∃!) rel-well-def : ∀ {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} (R : Rel X ℓ) (q : X → Y) → Set _ rel-well-def R q = ∀ x₁ x₂ → R x₁ x₂ → q x₁ ≡ q x₂ record _coequalizes_ {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} (q : X → Y) (R : Rel X ℓ) : Set (L.suc ℓ L.⊔ ℓ') where field q∘R : rel-well-def R q ump : ∀ (Z : Set ℓ) (h : X → Z) → rel-well-def R h → ∃! _≗_ λ f → f ∘ q ≡ h module coequ-prop {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} (q : X → Y) (R : Rel X ℓ) where -- equiv-closure-coequalizes : q coequalizes R → q coequalizes (Equiv-Closure R) -- equiv-closure-coequalizes q-coeq-R = {!!}
Kernel
ker : ∀ {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} (f : X → Y) → Rel X ℓ' ker f x₁ x₂ = f x₁ ≡ f x₂ ker-IsEquivalence : ∀ {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} (f : X → Y) → IsEquivalence (ker f) ker-IsEquivalence f = record { refl = ≡.refl ; sym = λ {x} {y} f[x]≡f[y] → ≡.sym f[x]≡f[y] ; trans = λ xy yz → ≡.trans xy yz }
Setoids
record Setoid : Set (L.suc L.0ℓ) where field Carrier : Set _≈_ : Rel Carrier L.0ℓ ≈-isEquivalence : IsEquivalence _≈_ open IsEquivalence ≈-isEquivalence public record Func (X Y : Setoid) : Set L.0ℓ where field to : (Setoid.Carrier X) → (Setoid.Carrier Y) cong : ∀ {x} {x'} → (Setoid._≈_ X x x') → (Setoid._≈_ Y (to x) (to x')) open import Data.Product ker' : ∀ {X} {Y} → Func X Y → Rel (Setoid.Carrier X) L.0ℓ ker' {X} {Y} f = λ x x' → f.to x Y.≈ f.to x' where module f = Func f module Y = Setoid Y -- ker'-equiv : ∀ {X} {Y} → (f : Func X Y) → IsEquivalence (ker' f) -- ker'-equiv = {!!} Im[_] : ∀ {X Y : Setoid} → Func X Y → Setoid Im[_] {X} {Y} f = record { Carrier = Σ[ y ∈ Y.Carrier ] ∃[ x ] f.to x ≡ y ; _≈_ = λ y-x-eq y'-x'-eq' → proj₁ y-x-eq Y.≈ proj₁ y'-x'-eq' ; ≈-isEquivalence = record { refl = Y.refl ; sym = Y.sym ; trans = Y.trans } } where module f = Func f module Y = Setoid Y -- zweimal f im Kontext surj[_] : ∀ {X Y : Setoid} → (f : Func X Y) → Func X Im[ f ] surj[_] {X} {Y} f = record { to = λ x → f.to x , x , ≡.refl ; cong = λ x≈x' → f.cong x≈x' } where module f = Func f module X = Setoid X module Y = Setoid Y inj[_] : ∀ {X Y : Setoid} → (f : Func X Y) → Func Im[ f ] Y inj[_] f = record { to = proj₁ ; cong = λ { eq → eq } }
Ende der Vorlesung am 15. Juni 2026
Stdlib
import Relation.Binary.Bundles using (Setoid) -- Functional Extensionality: import Axiom.Extensionality.Propositional using (Extensionality) -- Pointwise equality of functions: import Relation.Binary.PropositionalEquality using ( _≗_)