index ∙ source

module ObjectClassifiers where

open import 1Lab.Type hiding (⊤)
open import 1Lab.Type.Pointed
open import 1Lab.Type.Sigma
open import 1Lab.Path
open import 1Lab.Equiv
open import 1Lab.HLevel
open import 1Lab.HLevel.Closure
open import 1Lab.Extensionality
open import Data.Id.Base

open import 1Lab.Univalence
  using (Fibre-equiv) -- this does not use univalence

-- The (homotopy) pullback, defined using the inductive identity type to
-- make some things easier
record
  Pullback
    {ℓ ℓ' ℓ''} {B : Type ℓ} {C : Type ℓ'} {D : Type ℓ''}
    (s : B → D) (q : C → D)
  : Type (ℓ ⊔ ℓ' ⊔ ℓ'') where
  constructor pb
  field
    pb₁ : B
    pb₂ : C
    pbeq : s pb₁ ≡ᵢ q pb₂

open Pullback

-- A universe-polymorphic unit type to avoid Lift noise
record ⊤ {u} : Type u where
  constructor tt

It is well-known that univalent universes in type theory correspond to object classifiers in higher topos theory. However, there are a few different ways to make sense of this internally to type theory itself.

In what follows, we fix a (Russell) universe $\mathcal{U}$ and call types in $\mathcal{U}$ small. We write $\mathcal{U}^\mathsf{p} : \mathcal{U}^\bullet \to \mathcal{U}$ for the universal projection from pointed small types to small types. We assume function extensionality (implicitly by working in Cubical Agda), but not univalence.

module _ {u} where

  U  = Type u
  U∙ = Type∙ u
  U⁺ = Type (lsuc u)

  Uᵖ : U∙ → U
  Uᵖ (A , _) = A

We define univalence for $\mathcal{U}$ as the statement that the type $(Y : \mathcal{U}) \times X \simeq Y$ is contractible for all $X : \mathcal{U}$ (thus that equivalences form an identity system on $\mathcal{U}$). We will also refer to $n$-univalence, the restriction of that statement to the sub-universe of $n$-types in $\mathcal{U}$.

  univalence = {X : U} → is-contr (Σ U λ Y → X ≃ Y)

Given a “base” type $B : \mathcal{U}$, there are two main ways we can express “type families over $B$” in type theory: as maps into $B$ from a small domain (this is often called the “fibred” perspective, and such maps may be called “fibrations” or “bundles” over $B$), or as maps out of $B$ into the universe (the “indexed” perspective). We thus define:

$$\begin{align*} \mathsf{Bun}(B) &= (A : \mathcal{U}) \times \begin{matrix}A \\ \downarrow \\ B\end{matrix}\\ \mathsf{Fam}(B) &= B \to \mathcal{U} \end{align*}$$

  module _ (B : U) where

    Bun : U⁺
    Bun = Σ[ A ∈ U ] (A → B)

    Fam : U⁺
    Fam = B → U

We have maps between those in both directions: the map $\chi_B : \mathsf{Bun}(B) \to \mathsf{Fam}(B)$ assigns to a bundle $A \to B$ its family of fibres, while the map $\phi_B : \mathsf{Fam}(B) \to \mathsf{Bun}(B)$ assigns to a $B$-indexed family the first projection out of its total space.

    χ : Bun → Fam
    χ (A , p) = fibre p

    φ : Fam → Bun
    φ a = Σ B a , fst

The HoTT book proves (theorem 4.8.3) that $\chi_B$ and $\phi_B$ are inverses, assuming that $\mathcal{U}$ is univalent. This is also formalised in the 1Lab:

    _ : is-equiv χ
    _ = 1Lab.Univalence.Fibration-equiv {ℓ' = u} .snd

    _ : is-equiv φ
    _ = (1Lab.Univalence.Fibration-equiv {ℓ' = u} e⁻¹) .snd

A partial converse to this result was formalised independently by Martín Escardó (in TypeTopology) and by Amélia Liao (in this math.SE answer): both of them show that univalence follows from $\chi_B$ being a fibrewise equivalence if one also assumes $(-2)$-univalence, i.e. that any two contractible types are equal¹ (as well as function extensionality). In this Mastodon post I gave an example of a Tarski universe containing two distinct unit types and which can be closed under $\Sigma$- and identity types in such a way that $\chi_B$ and $\phi_B$ are both fibrewise equivalences, but which is not $n$-univalent for any $n$, thus suggesting that one cannot get rid of the $(-2)$-univalence assumption.

In this note I would like to suggest an explanation for why the converse of theorem 4.8.3 fails. The key is to notice that $\mathsf{Bun}(B)$ and $\mathsf{Fam}(B)$ can be thought of as the endpoints of a span of types whose apex is the type of pullback squares with bottom-left corner $B$ and right-hand side map $\mathcal{U}^\mathsf{p}$:

Let us call such a pullback square a classification over $B$: it consists of a fibration over $B$ that is classified by a given map $a : B \to \mathcal{U}$.

To define the type $\mathsf{Cls}(B)$ of classifications, we take a shortcut: instead of recording three maps and a universal property, we only record the top-left corner $A$ and the bottom map $a$, and ask for an equivalence between $A$ and a given pullback of $\mathcal{U}^\mathsf{p}$ along $a$. This fully determines the projection maps out of $A$, so we are justified in leaving them out by function extensionality and contractibility of singletons. Note that we cannot similarly contract $A$ away as that would implicitly assume univalence.

    record Cls : U⁺ where
      constructor cls
      field
        A : U
        a : B → U
        classifies : A ≃ Pullback a Uᵖ

      module c = Equiv classifies

      p : A → B
      p = pb₁ ∘ c.to

      a⁺ : A → U∙
      a⁺ = pb₂ ∘ c.to

We obtain the span promised above by projecting the left and bottom maps of the pullback square, respectively.

    π↓ : Cls → Bun
    π↓ p = _ , Cls.p p

    π→ : Cls → Fam
    π→ = Cls.a

Observe that both $\pi_\downarrow$ and $\pi_\to$ have sections, given by taking fibres and total spaces respectively, and that composing one section with the other projection recovers the maps $\chi_B$ and $\phi_B$.

    σ↓ : Bun → Cls
    σ↓ (A , p) = λ where
      .Cls.A → A
      .Cls.a → fibre p
      .Cls.classifies .fst a → pb (p a) (fibre p (p a) , a , refl) reflᵢ
      .Cls.classifies .snd → is-iso→is-equiv λ where
        .is-iso.from (pb b (_ , (a , _)) reflᵢ) → a
        .is-iso.rinv (pb b (_ , (a , eq)) reflᵢ) i →
          pb (eq i) (fibre p (eq i) , a , λ j → eq (i ∧ j)) reflᵢ
        .is-iso.linv _ → refl

    section↓ : is-right-inverse σ↓ π↓
    section↓ (A , p) = refl

    _ : π→ ∘ σ↓ ≡ χ
    _ = refl

    σ→ : Fam → Cls
    σ→ a = λ where
      .Cls.A → Σ B a
      .Cls.a → a
      .Cls.classifies .fst (b , x) → pb b (a b , x) reflᵢ
      .Cls.classifies .snd → is-iso→is-equiv λ where
        .is-iso.from (pb b (_ , x) reflᵢ) → b , x
        .is-iso.rinv (pb b (_ , x) reflᵢ) → refl
        .is-iso.linv _ → refl

    section→ : is-right-inverse σ→ π→
    section→ a = refl

    _ : π↓ ∘ σ→ ≡ φ
    _ = refl

We now come to the main point of this post: each of $\pi_\downarrow$ and $\pi_\to$ is an equivalence if and only if univalence holds. This is reflected in the proof of Fibration-equiv, which uses univalence twice, once in the left inverse proof and once in the right inverse proof. This suggests that the two uses of univalence cancel each other out in a certain sense, so that we lose information if we only ask for a composite equivalence between $\mathsf{Bun}(B)$ and $\mathsf{Fam}(B)$.

In more detail, the statement that $\pi_\downarrow$ is an equivalence says that every bundle $A \to B$ is classified by a unique² pullback square into $\mathcal{U}^\mathsf{p}$; this looks a lot like the definition of an object classifier in higher topos theory! On the other hand, the statement that $\pi_\to$ is an equivalence says that every map $B \to \mathcal{U}$ has a unique pullback along $\mathcal{U}^\mathsf{p}$; in other words, that this pullback is determined uniquely up to identity rather than just equivalence. Notice that both statements are roughly of the form “there is a unique pullback square”, but that they quantify over different parts of the pullback square.

The easiest way to substantiate our claim is to specialise $B$ to the unit type; in this case, the span simplifies to the two projections out of the type of equivalences in $\mathcal{U}$:

  Equiv : U⁺
  Equiv = Σ[ X ∈ U ] Σ[ Y ∈ U ] X ≃ Y

  π₁≃ : Equiv → U
  π₁≃ (X , Y , e) = X

  π₂≃ : Equiv → U
  π₂≃ (X , Y , e) = Y

  Fam⊤≃U : Fam ⊤ ≃ U
  Fam⊤≃U .fst a = a _
  Fam⊤≃U .snd = is-iso→is-equiv λ where
    .is-iso.from X _ → X
    .is-iso.rinv X → refl
    .is-iso.linv a → refl

  Bun⊤≃U : Bun ⊤ ≃ U
  Bun⊤≃U .fst (A , _) = A
  Bun⊤≃U .snd = is-iso→is-equiv λ where
    .is-iso.from X → X , _
    .is-iso.rinv _ → refl
    .is-iso.linv _ → refl

  Pullback≃a : {a : ⊤ {u} → U} → Pullback a Uᵖ ≃ a _
  Pullback≃a .fst (pb _ (_ , b) reflᵢ) = b
  Pullback≃a .snd = is-iso→is-equiv λ where
    .is-iso.from b → pb _ (_ , b) reflᵢ
    .is-iso.rinv _ → refl
    .is-iso.linv (pb _ (_ , b) reflᵢ) → refl

  Cls⊤≃Equiv : Cls ⊤ ≃ Equiv
  Cls⊤≃Equiv .fst (cls A a e) = A , a _ , e ∙e Pullback≃a
  Cls⊤≃Equiv .snd = is-iso→is-equiv λ where
    .is-iso.from (X , Y , e) → cls X (λ _ → Y) (e ∙e Pullback≃a e⁻¹)
    .is-iso.rinv (X , Y , e) → refl ,ₚ refl ,ₚ ext λ _ → refl
    .is-iso.linv (cls A a e) →
      let
        h : (e ∙e Pullback≃a) ∙e Pullback≃a e⁻¹ ≡ e
        h = ext λ _ → Equiv.η Pullback≃a _
      in λ i → cls A a (h i)

  _ : π₁≃ ≡ Equiv.to Bun⊤≃U ∘ π↓ ⊤ ∘ Equiv.from Cls⊤≃Equiv
  _ = refl

  _ : π₂≃ ≡ Equiv.to Fam⊤≃U ∘ π→ ⊤ ∘ Equiv.from Cls⊤≃Equiv
  _ = refl

This makes the proof immediate after noting that the fibre of $\pi^\simeq_1$ at $X$ is equivalent to $(Y : \mathcal{U}) \times X \simeq Y$ (a general fact that does not require univalence or even function extensionality), and symmetrically for $\pi^\simeq_2$.

  π₁≃-equiv→univalence : is-equiv π₁≃ → univalence
  π₁≃-equiv→univalence h {X} = Equiv→is-hlevel 
    (Fibre-equiv (λ X → Σ U λ Y → X ≃ Y) X e⁻¹)
    (h .is-eqv X)

  π↓-equiv→univalence : is-left-inverse (σ↓ ⊤) (π↓ ⊤) → univalence
  π↓-equiv→univalence h = π₁≃-equiv→univalence $
    ∘-is-equiv (Bun⊤≃U .snd)
      (∘-is-equiv π↓-is-equiv
        ((Cls⊤≃Equiv e⁻¹) .snd))
    where
      π↓-is-equiv : is-equiv (π↓ ⊤)
      π↓-is-equiv = is-iso→is-equiv (iso (σ↓ _) (section↓ _) h)

  sym≃ : Equiv ≃ Equiv
  sym≃ .fst (X , Y , e) = Y , X , e e⁻¹
  sym≃ .snd = is-involutive→is-equiv λ (X , Y , e) →
    refl ,ₚ refl ,ₚ ext λ _ → refl

  π→-equiv→univalence : is-left-inverse (σ→ ⊤) (π→ ⊤) → univalence
  π→-equiv→univalence h = π₁≃-equiv→univalence $
    ∘-is-equiv (Fam⊤≃U .snd)
      (∘-is-equiv π→-is-equiv
        (∘-is-equiv ((Cls⊤≃Equiv e⁻¹) .snd)
          (sym≃ .snd)))
    where
      π→-is-equiv : is-equiv (π→ ⊤)
      π→-is-equiv = is-iso→is-equiv (iso (σ→ _) (section→ _) h)

It also makes it easy to see the complete loss of information in assuming an equivalence $\mathsf{Bun}(\top) \simeq \mathsf{Fam}(\top)$, since this amounts to the trivial $\mathcal{U} \simeq \mathcal{U}$! Assuming that $\chi_\top$ or $\phi_\top$ is an equivalence doesn’t get us very far either, as in both cases we just get that forming products with a contractible type is an equivalence.

  _ : Equiv.to Bun⊤≃U ∘ π↓ ⊤ ∘ σ→ ⊤ ∘ Equiv.from Fam⊤≃U
    ≡ λ X → ⊤ × X
  _ = refl

  _ : Equiv.to Fam⊤≃U ∘ π→ ⊤ ∘ σ↓ ⊤ ∘ Equiv.from Bun⊤≃U
    ≡ λ X → X × tt ≡ tt
  _ = refl