# 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 ( _≗_)
```