 Agda UALib ↑

### Relation Extensionality

This section presents the Relations.Extensionality module of the Agda Universal Algebra Library.

```
{-# OPTIONS --without-K --exact-split --safe #-}

module Relations.Extensionality where

open import Relations.Truncation public
open import MGS-MLTT using (𝟙) public

```

The principle of proposition extensionality asserts that logically equivalent propositions are equivalent. That is, if `P` and `Q` are propositions and if `P ⊆ Q` and `Q ⊆ P`, then `P ≡ Q`. For our purposes, it will suffice to formalize this notion for general predicates, rather than for propositions (i.e., truncated predicates).

```
pred-ext : (𝓤 𝓦 : Universe) → (𝓤 ⊔ 𝓦) ⁺ ̇
pred-ext 𝓤 𝓦 = ∀ {A : 𝓤 ̇}{P Q : Pred A 𝓦 } → P ⊆ Q → Q ⊆ P → P ≡ Q

```

Note that `pred-ext` merely defines an extensionality principle. It does not postulate that the principle holds. If we wish to postulate `pred-ext`, then we do so by assuming that type is inhabited (see `block-ext` below, for example).

#### Quotient extensionality

We need an identity type for congruence classes (blocks) over sets so that two different presentations of the same block (e.g., using different representatives) may be identified. This requires two postulates: (1) predicate extensionality, manifested by the `pred-ext` type; (2) equivalence class truncation or “uniqueness of block identity proofs”, manifested by the `blk-uip` type defined in the Relations.Truncation module. We now use `pred-ext` and `blk-uip` to define a type called `block-ext|uip` which we require for the proof of the First Homomorphism Theorem presented in Homomorphisms.Noether.

```
module _ {𝓤 𝓦 : Universe}{A : 𝓤 ̇}{R : Rel A 𝓦} where

block-ext : pred-ext 𝓤 𝓦 → IsEquivalence R → {u v : A} → R u v → [ u ]{R} ≡ [ v ]{R}
block-ext pe Req {u}{v} Ruv = pe (/-subset Req Ruv) (/-supset Req Ruv)

to-subtype|uip : blk-uip A R → {C D : Pred A 𝓦}{c : IsBlock C {R}}{d : IsBlock D {R}}
→               C ≡ D → (C , c) ≡ (D , d)

to-subtype|uip buip {C}{D}{c}{d}CD = to-Σ-≡(CD , buip D(transport(λ B → IsBlock B)CD c)d)

block-ext|uip : pred-ext 𝓤 𝓦 → blk-uip A R → IsEquivalence R
→              ∀ {u v : A}  →  R u v  →  ⟪ u ⟫ ≡ ⟪ v ⟫

block-ext|uip pe buip Req Ruv = to-subtype|uip buip (block-ext pe Req Ruv)

```

#### Question: prop vs pred extensionality

Is predicate extensionality stronger than proposition extensionality? That is, does `pred-ext 𝓤 𝓦` imply the following?

``````  ∀(A : 𝓤 ̇)(P : Pred A 𝓦)(x : A)(p q : P x) → p ≡ q
``````

We could also define relation extensionality principles which generalize the predicate extensionality principle (`pred-ext`) defined above

```
cont-rel-ext : (𝓤 𝓥 𝓦 : Universe) → (𝓤 ⊔ 𝓥 ⊔ 𝓦) ⁺ ̇
cont-rel-ext 𝓤 𝓥 𝓦 = ∀ {I : 𝓥 ̇}{A : 𝓤 ̇}{P Q : ContRel I A 𝓦 } → P ⊆ Q → Q ⊆ P → P ≡ Q

dep-rel-ext : (𝓤 𝓥 𝓦 : Universe) → (𝓤 ⊔ 𝓥 ⊔ 𝓦) ⁺ ̇
dep-rel-ext 𝓤 𝓥 𝓦 = ∀ {I : 𝓥 ̇}{𝒜 : I → 𝓤 ̇}{P Q : DepRel I 𝒜 𝓦 } → P ⊆ Q → Q ⊆ P → P ≡ Q

```

These types are not used in other modules of the UALib and we pose the same question about them as the one above. That is, we ask whether these general relation extensionality principles are stonger than proposition extensionality.