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.

← Relations.Truncation Algebras β†’