Type duality

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-09-16.
Last modified on 2024-03-14.

module foundation.type-duality where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.locally-small-types
open import foundation.slice
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.unit-type
open import foundation.univalence
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.embeddings
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.small-types
open import foundation-core.torsorial-type-families

open import trees.polynomial-endofunctors


Given a univalent universe 𝒰, we can define two closely related functors acting on all types. First there is the covariant functor given by

  P_𝒰(A) := Σ (X : 𝒰), X → A.

This is a polynomial endofunctor. Second, there is the contravariant functor given by

  P^𝒰(A) := A → 𝒰.

If the type A is locally 𝒰-small, then there is a map φ_A : P_𝒰(A) → P^𝒰(A). This map is natural in A, and it is always an embedding. Furthermore, the map φ_A is an equivalence if and only if A is 𝒰-small.


The polynomial endofunctor of a universe

type-polynomial-endofunctor-UU :
  (l : Level) {l1 : Level} (A : UU l1)  UU (lsuc l  l1)
type-polynomial-endofunctor-UU l = Slice l

map-polynomial-endofunctor-UU :
  (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  type-polynomial-endofunctor-UU l A  type-polynomial-endofunctor-UU l B
map-polynomial-endofunctor-UU l = map-polynomial-endofunctor (UU l)  X  X)

Type families

type-exp-UU : (l : Level) {l1 : Level}  UU l1  UU (lsuc l  l1)
type-exp-UU l A = A  UU l

map-exp-UU :
  (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  type-exp-UU l B  type-exp-UU l A
map-exp-UU l f P = P  f


If A is locally l-small, then we can construct an embedding type-polynomial-endofunctor l A ↪ type-exp-UU A

map-type-duality :
  {l l1 : Level} {A : UU l1}  is-locally-small l A 
  type-polynomial-endofunctor-UU l A  type-exp-UU l A
map-type-duality H (X , f) a =
  Σ X  x  type-is-small (H (f x) a))

is-emb-map-type-duality :
  {l l1 : Level} {A : UU l1} (H : is-locally-small l A) 
  is-emb (map-type-duality H)
is-emb-map-type-duality {l} {l1} {A} H (X , f) =
    ( is-contr-equiv
      ( Σ ( type-polynomial-endofunctor-UU l A) ((X , f) =_))
      ( equiv-tot
        ( λ (Y , g) 
          ( inv-equiv (extensionality-Slice (X , f) (Y , g))) ∘e
          ( inv-equiv (equiv-fam-equiv-equiv-slice f g)) ∘e
          ( equiv-Π-equiv-family
            ( λ a 
              ( equiv-postcomp-equiv
                ( equiv-tot  y  inv-equiv (equiv-is-small (H (g y) a))))
                ( fiber f a)) ∘e
              ( equiv-precomp-equiv
                ( equiv-tot  x  equiv-is-small (H (f x) a)))
                ( Σ Y  y  type-is-small (H (g y) a)))) ∘e
              ( equiv-univalence))) ∘e
          ( equiv-funext)))
      ( is-torsorial-Id (X , f)))
    ( λ Y  ap (map-type-duality H))

emb-type-duality :
  {l l1 : Level} {A : UU l1}  is-locally-small l A 
  type-polynomial-endofunctor-UU l A  type-exp-UU l A
pr1 (emb-type-duality H) = map-type-duality H
pr2 (emb-type-duality H) = is-emb-map-type-duality H

A type A is small if and only if P_𝒰(A) ↪ P^𝒰(A) is an equivalence

The forward direction

module _
  {l l1 : Level} {A : UU l1} (H : is-small l A)

  map-inv-type-duality :
    type-exp-UU l A  type-polynomial-endofunctor-UU l A
  pr1 (map-inv-type-duality B) =
    type-is-small (is-small-Σ H  a  is-small' {l} {B a}))
  pr2 (map-inv-type-duality B) =
    ( pr1) 
    ( map-inv-equiv (equiv-is-small (is-small-Σ H  a  is-small' {l} {B a}))))

  is-section-map-inv-type-duality :
    map-type-duality (is-locally-small-is-small H)  map-inv-type-duality ~ id
  is-section-map-inv-type-duality B =
      ( λ a 
            ( is-locally-small-is-small H)
            ( map-inv-type-duality B)
            ( a)
            ( ( pr1 {B = B}) 
              ( map-inv-equiv
                ( equiv-is-small
                  ( is-small-Σ H  a  is-small'))))) a
              ( λ x 
                  ( equiv-is-small
                    ( is-locally-small-is-small H
                      ( pr2 (map-inv-type-duality B) x)
                      ( a))))
           Σ ( fiber (pr1 {B = B}) a)
              ( λ b 
                  ( map-inv-equiv
                    ( equiv-is-small
                      ( is-small-Σ H  a  is-small' {l} {B a}))))
                  ( pr1 b))
            by compute-fiber-comp pr1 _ a
           fiber (pr1 {B = B}) a
              ( λ b 
                  ( is-equiv-map-inv-equiv
                    ( equiv-is-small
                      ( is-small-Σ H  a  is-small' {l} {B a}))))
                  ( pr1 b))
           B a
            equiv-fiber-pr1 B a)

  is-retraction-map-inv-type-duality :
    map-inv-type-duality  map-type-duality (is-locally-small-is-small H) ~ id
  is-retraction-map-inv-type-duality X =
      ( is-emb-map-type-duality (is-locally-small-is-small H))
      ( is-section-map-inv-type-duality
        ( map-type-duality (is-locally-small-is-small H) X))

  is-equiv-map-type-duality :
    is-equiv (map-type-duality (is-locally-small-is-small H))
  is-equiv-map-type-duality =

  type-duality : type-polynomial-endofunctor-UU l A  type-exp-UU l A
  pr1 type-duality = map-type-duality (is-locally-small-is-small H)
  pr2 type-duality = is-equiv-map-type-duality

The converse direction

module _
  {l l1 : Level} {A : UU l1} (H : is-locally-small l A)

  is-small-is-equiv-map-type-duality :
    is-equiv (map-type-duality H)  is-small l A
  pr1 (is-small-is-equiv-map-type-duality E) =
    pr1 (map-inv-is-equiv E  _  raise-unit l))
  pr2 (is-small-is-equiv-map-type-duality E) =
      ( ( pr2 (map-inv-is-equiv E  _  raise-unit l))) ,
        ( is-equiv-is-contr-map
          ( λ a 
              ( raise-unit l)
              ( ( equiv-eq-fam _ _
                  ( is-section-map-inv-is-equiv E  _  raise-unit l))
                  ( a)) ∘e
                ( equiv-tot
                  ( λ x 
                      ( H ( pr2 (map-inv-is-equiv E  _  raise-unit l)) x)
                          ( a)))))
              ( is-contr-raise-unit))))

Type duality formulated using l1 ⊔ l2

Fiber : {l l1 : Level} (A : UU l1)  Slice l A  A  UU (l1  l)
Fiber A f = fiber (pr2 f)

Pr1 : {l l1 : Level} (A : UU l1)  (A  UU l)  Slice (l1  l) A
pr1 (Pr1 A B) = Σ A B
pr2 (Pr1 A B) = pr1

is-section-Pr1 :
  {l1 l2 : Level} {A : UU l1}  (Fiber {l1  l2} A  Pr1 {l1  l2} A) ~ id
is-section-Pr1 B = eq-equiv-fam (equiv-fiber-pr1 B)

is-retraction-Pr1 :
  {l1 l2 : Level} {A : UU l1}  (Pr1 {l1  l2} A  Fiber {l1  l2} A) ~ id
is-retraction-Pr1 {A = A} (X , f) =
    ( Pr1 A (Fiber A (X , f)))
    ( X , f)
    ( equiv-total-fiber f , triangle-map-equiv-total-fiber f)

is-equiv-Fiber :
  {l1 : Level} (l2 : Level) (A : UU l1)  is-equiv (Fiber {l1  l2} A)
is-equiv-Fiber l2 A =
    ( Pr1 A)
    ( is-section-Pr1 {l2 = l2})
    ( is-retraction-Pr1 {l2 = l2})

equiv-Fiber :
  {l1 : Level} (l2 : Level) (A : UU l1)  Slice (l1  l2) A  (A  UU (l1  l2))
pr1 (equiv-Fiber l2 A) = Fiber A
pr2 (equiv-Fiber l2 A) = is-equiv-Fiber l2 A

is-equiv-Pr1 :
  {l1 : Level} (l2 : Level) (A : UU l1)  is-equiv (Pr1 {l1  l2} A)
is-equiv-Pr1 {l1} l2 A =
    ( Fiber A)
    ( is-retraction-Pr1 {l2 = l2})
    ( is-section-Pr1 {l2 = l2})

equiv-Pr1 :
  {l1 : Level} (l2 : Level) (A : UU l1)  (A  UU (l1  l2))  Slice (l1  l2) A
pr1 (equiv-Pr1 l2 A) = Pr1 A
pr2 (equiv-Pr1 l2 A) = is-equiv-Pr1 l2 A

The type of all function from A → B is equivalent to the type of function Y : B → 𝒰 with an equivalence A ≃ Σ B Y

fiber-Σ :
  {l1 l2 : Level} (X : UU l1) (A : UU l2) 
  (X  A)  Σ (A  UU (l2  l1))  Y  X  Σ A Y)
fiber-Σ {l1} {l2} X A =
  ( equiv-Σ
    ( λ Z  X  Σ A Z)
    ( equiv-Fiber l1 A)
    ( λ s  inv-equiv ( equiv-postcomp-equiv (equiv-total-fiber (pr2 s)) X))) ∘e
  ( equiv-right-swap-Σ) ∘e
  ( inv-left-unit-law-Σ-is-contr
    ( is-contr-is-small-lmax l2 X)
    ( is-small-lmax l2 X)) ∘e
  ( equiv-precomp (inv-equiv (equiv-is-small (is-small-lmax l2 X))) A)

See also

Recent changes