Binary type duality

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-01-28.

module foundation.binary-type-duality where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-spans
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.multivariable-homotopies
open import foundation.retractions
open import foundation.sections
open import foundation.spans
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.homotopies
open import foundation-core.identity-types

Idea

The principle of binary type duality asserts that the type of binary relations A → B → 𝒰 is equivalent to the type of binary spans from A to B. The binary type duality principle is a binary version of the type duality principle, which asserts that type families over a type A are equivalently described as maps into A, and makes essential use of the univalence axiom.

The equivalence of binary type duality takes a binary relation R : A → B → 𝒰 to the span

  A <----- Σ (a : A), Σ (b : B), R a b -----> B.

and its inverse takes a span A <-f- S -g-> B to the binary relation

  a b ↦ Σ (s : S), (f s ＝ a) × (g s ＝ b).

Definitions

The span associated to a binary relation

Given a binary relation R : A → B → 𝒰, we obtain a span

  A <----- Σ (a : A), Σ (b : B), R a b -----> B.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A → B → UU l3)
  where

  spanning-type-span-binary-relation : UU (l1 ⊔ l2 ⊔ l3)
  spanning-type-span-binary-relation = Σ A (λ a → Σ B (λ b → R a b))

  left-map-span-binary-relation : spanning-type-span-binary-relation → A
  left-map-span-binary-relation = pr1

  right-map-span-binary-relation : spanning-type-span-binary-relation → B
  right-map-span-binary-relation = pr1 ∘ pr2

  span-binary-relation : span (l1 ⊔ l2 ⊔ l3) A B
  pr1 span-binary-relation = spanning-type-span-binary-relation
  pr1 (pr2 span-binary-relation) = left-map-span-binary-relation
  pr2 (pr2 span-binary-relation) = right-map-span-binary-relation

The binary relation associated to a span

Given a span

       f       g
  A <----- S -----> B

we obtain the binary relation a b ↦ Σ (s : S), (f s ＝ a) × (g s ＝ b).

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  where

  binary-relation-span : span l3 A B → A → B → UU (l1 ⊔ l2 ⊔ l3)
  binary-relation-span S a b =
    Σ ( spanning-type-span S)
      ( λ s → (left-map-span S s ＝ a) × (right-map-span S s ＝ b))

Properties

Any span S is equivalent to the span associated to the binary relation associated to S

The construction of this equivalence of span diagrams is simply by pattern matching all the way.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (S : span l3 A B)
  where

  map-equiv-spanning-type-span-binary-relation-span :
    spanning-type-span S →
    spanning-type-span-binary-relation (binary-relation-span S)
  map-equiv-spanning-type-span-binary-relation-span s =
    ( left-map-span S s , right-map-span S s , s , refl , refl)

  map-inv-equiv-spanning-type-span-binary-relation-span :
    spanning-type-span-binary-relation (binary-relation-span S) →
    spanning-type-span S
  map-inv-equiv-spanning-type-span-binary-relation-span (a , b , s , _) = s

  is-section-map-inv-equiv-spanning-type-span-binary-relation-span :
    is-section
      ( map-equiv-spanning-type-span-binary-relation-span)
      ( map-inv-equiv-spanning-type-span-binary-relation-span)
  is-section-map-inv-equiv-spanning-type-span-binary-relation-span
    ( ._ , ._ , s , refl , refl) =
    refl

  is-retraction-map-inv-equiv-spanning-type-span-binary-relation-span :
    is-retraction
      ( map-equiv-spanning-type-span-binary-relation-span)
      ( map-inv-equiv-spanning-type-span-binary-relation-span)
  is-retraction-map-inv-equiv-spanning-type-span-binary-relation-span s = refl

  is-equiv-map-equiv-spanning-type-span-binary-relation-span :
    is-equiv
      ( map-equiv-spanning-type-span-binary-relation-span)
  is-equiv-map-equiv-spanning-type-span-binary-relation-span =
    is-equiv-is-invertible
      ( map-inv-equiv-spanning-type-span-binary-relation-span)
      ( is-section-map-inv-equiv-spanning-type-span-binary-relation-span)
      ( is-retraction-map-inv-equiv-spanning-type-span-binary-relation-span)

  equiv-spanning-type-span-binary-relation-span :
    spanning-type-span S ≃
    spanning-type-span-binary-relation (binary-relation-span S)
  pr1 equiv-spanning-type-span-binary-relation-span =
    map-equiv-spanning-type-span-binary-relation-span
  pr2 equiv-spanning-type-span-binary-relation-span =
    is-equiv-map-equiv-spanning-type-span-binary-relation-span

  equiv-span-binary-relation-span :
    equiv-span S (span-binary-relation (binary-relation-span S))
  pr1 equiv-span-binary-relation-span =
    equiv-spanning-type-span-binary-relation-span
  pr1 (pr2 equiv-span-binary-relation-span) =
    refl-htpy
  pr2 (pr2 equiv-span-binary-relation-span) =
    refl-htpy

Any binary relation R is equivalent to the binary relation associated to the span associated to R

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A → B → UU l3)
  (a : A) (b : B)
  where

  map-equiv-binary-relation-span-binary-relation :
    R a b → binary-relation-span (span-binary-relation R) a b
  map-equiv-binary-relation-span-binary-relation r =
    ((a , b , r) , refl , refl)

  map-inv-equiv-binary-relation-span-binary-relation :
    binary-relation-span (span-binary-relation R) a b → R a b
  map-inv-equiv-binary-relation-span-binary-relation
    ((.a , .b , r) , refl , refl) =
    r

  is-section-map-inv-equiv-binary-relation-span-binary-relation :
    is-section
      ( map-equiv-binary-relation-span-binary-relation)
      ( map-inv-equiv-binary-relation-span-binary-relation)
  is-section-map-inv-equiv-binary-relation-span-binary-relation
    ((.a , .b , r) , refl , refl) =
    refl

  is-retraction-map-inv-equiv-binary-relation-span-binary-relation :
    is-retraction
      ( map-equiv-binary-relation-span-binary-relation)
      ( map-inv-equiv-binary-relation-span-binary-relation)
  is-retraction-map-inv-equiv-binary-relation-span-binary-relation r = refl

  is-equiv-map-equiv-binary-relation-span-binary-relation :
    is-equiv map-equiv-binary-relation-span-binary-relation
  is-equiv-map-equiv-binary-relation-span-binary-relation =
    is-equiv-is-invertible
      map-inv-equiv-binary-relation-span-binary-relation
      is-section-map-inv-equiv-binary-relation-span-binary-relation
      is-retraction-map-inv-equiv-binary-relation-span-binary-relation

  equiv-binary-relation-span-binary-relation :
    R a b ≃ binary-relation-span (span-binary-relation R) a b
  pr1 equiv-binary-relation-span-binary-relation =
    map-equiv-binary-relation-span-binary-relation
  pr2 equiv-binary-relation-span-binary-relation =
    is-equiv-map-equiv-binary-relation-span-binary-relation

Theorem

Binary spans are equivalent to binary relations

module _
  {l1 l2 l3 : Level} (A : UU l1) (B : UU l2)
  where

  is-section-binary-relation-span :
    is-section
      ( span-binary-relation {l3 = l1 ⊔ l2 ⊔ l3} {A} {B})
      ( binary-relation-span {l3 = l1 ⊔ l2 ⊔ l3} {A} {B})
  is-section-binary-relation-span S =
    inv
      ( eq-equiv-span
        ( S)
        ( span-binary-relation (binary-relation-span S))
        ( equiv-span-binary-relation-span S))

  is-retraction-binary-relation-span :
    is-retraction
      ( span-binary-relation {l3 = l1 ⊔ l2 ⊔ l3} {A} {B})
      ( binary-relation-span {l3 = l1 ⊔ l2 ⊔ l3} {A} {B})
  is-retraction-binary-relation-span R =
    inv
      ( eq-multivariable-htpy 2
        ( λ a b → eq-equiv (equiv-binary-relation-span-binary-relation R a b)))

  is-equiv-span-binary-relation :
    is-equiv (span-binary-relation {l3 = l1 ⊔ l2 ⊔ l3} {A} {B})
  is-equiv-span-binary-relation =
    is-equiv-is-invertible
      ( binary-relation-span)
      ( is-section-binary-relation-span)
      ( is-retraction-binary-relation-span)

  binary-type-duality : (A → B → UU (l1 ⊔ l2 ⊔ l3)) ≃ span (l1 ⊔ l2 ⊔ l3) A B
  pr1 binary-type-duality = span-binary-relation
  pr2 binary-type-duality = is-equiv-span-binary-relation

  is-equiv-binary-relation-span :
    is-equiv (binary-relation-span {l3 = l1 ⊔ l2 ⊔ l3} {A} {B})
  is-equiv-binary-relation-span =
    is-equiv-is-invertible
      ( span-binary-relation)
      ( is-retraction-binary-relation-span)
      ( is-section-binary-relation-span)

  inv-binary-type-duality :
    span (l1 ⊔ l2 ⊔ l3) A B ≃ (A → B → UU (l1 ⊔ l2 ⊔ l3))
  pr1 inv-binary-type-duality = binary-relation-span
  pr2 inv-binary-type-duality = is-equiv-binary-relation-span

Recent changes