Structured equality duality

Content created by Fredrik Bakke.

Created on 2025-02-10.
Last modified on 2025-02-10.

module foundation.structured-equality-duality where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.maps-in-subuniverses
open import foundation.separated-types-subuniverses
open import foundation.structure
open import foundation.subuniverses
open import foundation.universe-levels

open import foundation-core.equivalences

Idea

Given a structure 𝒫 on types that transfers along equivalences in the sense that 𝒫 comes equipped with a family of maps

  {X Y : 𝒰} → (X ≃ Y) → 𝒫 X → 𝒫 Y,

then for every type A and type family B : A → 𝒰 there is a mutual correspondence between the following:

  1. 𝒫-structured families of maps f : (y : A) → (x ＝ y) → B y for every x : A.
  2. 𝒫-structures on the equality of Σ A B.

We refer to this as structured equality duality.

Note. by the univalence axiom, every structure transfers along equivalences. However, we maintain this as an assumption, since for most common notions of structure this property is independent of the univalence axiom.

One potential but crude justification for using the term “duality” for this principle is as follows. The principle gives a correspondence between structures on families of maps mapping into the type family B, and structures on the binary family of equality over the dependent sum Σ A B, and so, in a certain sense, one is trading one straightened dimension for another.

Duality

Structured equality duality

module _
  {l1 l2 l3 : Level} {𝒫 : UU (l1 ⊔ l2) → UU l3}
  (tr-𝒫 : {X Y : UU (l1 ⊔ l2)} → X ≃ Y → 𝒫 X → 𝒫 Y)
  {A : UU l1} {B : A → UU l2}
  where

  forward-implication-structured-equality-duality :
    ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) →
    structure-equality 𝒫 (Σ A B)
  forward-implication-structured-equality-duality
    K (x , b) (x' , b') =
    tr-𝒫
      ( compute-fiber-map-out-of-identity-type (ind-Id x (λ u _ → B u) b) x' b')
      ( K x (ind-Id x (λ u _ → B u) b) x' b')

  backward-implication-structured-equality-duality :
    structure-equality 𝒫 (Σ A B) →
    ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y))
  backward-implication-structured-equality-duality K x f y b =
    tr-𝒫
      ( inv-compute-fiber-map-out-of-identity-type f y b)
      ( K (x , f x refl) (y , b))

  structured-equality-duality :
    ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) ↔
    ( structure-equality 𝒫 (Σ A B))
  structured-equality-duality =
    ( forward-implication-structured-equality-duality ,
      backward-implication-structured-equality-duality)

Subuniverse equality duality

Given a subuniverse 𝒫 then the following are logically equivalent:

  1. For every x : A, every family of maps f : (y : A) → (x ＝ y) → B y is a family of 𝒫-maps.
  2. The dependent sum Σ A B is 𝒫-separated.
module _
  {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3)
  {A : UU l1} {B : A → UU l2}
  where

  forward-implication-subuniverse-equality-duality :
    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
      (y : A) → is-in-subuniverse-map 𝒫 (f y)) →
    is-separated 𝒫 (Σ A B)
  forward-implication-subuniverse-equality-duality =
    forward-implication-structured-equality-duality
      ( is-in-subuniverse-equiv 𝒫)

  backward-implication-subuniverse-equality-duality :
    is-separated 𝒫 (Σ A B) →
    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
      (y : A) → is-in-subuniverse-map 𝒫 (f y))
  backward-implication-subuniverse-equality-duality =
    backward-implication-structured-equality-duality
      ( is-in-subuniverse-equiv 𝒫)

  subuniverse-equality-duality :
    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
      (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔
    is-separated 𝒫 (Σ A B)
  subuniverse-equality-duality =
    structured-equality-duality (is-in-subuniverse-equiv 𝒫)

See also

This duality is applied in

Recent changes