indexsource

An improved version of this note is at ObjectClassifiers.
open import 1Lab.Type
open import 1Lab.Type.Sigma
open import 1Lab.Type.Pointed
open import 1Lab.Path
open import 1Lab.HLevel
open import 1Lab.HLevel.Closure
open import 1Lab.Equiv

-- Univalence from object classifiers in the sense of higher topos theory.
module ObjectClassifier where

-- The type of arrows/bundles/fibrations.
Bundle :    Type (lsuc )
Bundle 
  = Σ (Type ) λ A
   Σ (Type ) λ B
   A  B

-- The standard pullback construction (HoTT book 2.15.11).
record Pullback { ℓ'} {B : Type } {C D : Type ℓ'} (s : B  D) (q : C  D) : Type (  ℓ') where
  constructor pb
  field
    pb₁ : B
    pb₂ : C
    pbeq : s pb₁  q pb₂

open Pullback

pb-path :  { ℓ'} {B : Type } {C D : Type ℓ'} {s : B  D} {q : C  D}  {a b : Pullback s q}
         (p1 : a .pb₁  b .pb₁)  (p2 : a .pb₂  b .pb₂)  PathP  i  s (p1 i)  q (p2 i)) (a .pbeq) (b .pbeq)
         a  b
pb-path p1 p2 pe i = pb (p1 i) (p2 i) (pe i)

-- The morphisms of interest between bundles p : A → B and q : C → D are pairs
-- r : A → C, s : B → D that make a *pullback square*:
--                r
--           A ------> C
--           | ⯾       |
--         p |         | q
--           v         v
--           B ------> D
--                s
-- Rather than laboriously state the universal property of a pullback, we take it
-- on faith that the construction above has the universal property (this is
-- exercise 2.11 in the HoTT book) and simply define "being a pullback" as having
-- r and p factor through an equivalence A ≃ Pullback s q.
-- This completely determines r by the factorisation r = pb₂ ∘ e .fst, so we can
-- omit it by contractibility of singletons.
_⇒_ :  {} {ℓ'}  Bundle   Bundle ℓ'  Type (  ℓ')
(A , B , p)  (C , D , q)
  = Σ (B  D) λ s
   Σ (A  Pullback s q) λ e
   p  pb₁  e .fst

-- An object classifier is a *universal* bundle U∙ → U such that any other
-- bundle has a unique map (i.e. pullback square) into it.
-- Categorically, it is a terminal object in the category of arrows and pullback squares.
is-classifier :  {}  Bundle (lsuc )  Type (lsuc )
is-classifier {} u =  (p : Bundle )  is-contr (p  u)

-- The projection from the type of pointed types to the type of types is our
-- universal bundle: the fibre above A : Type ℓ is equivalent to A itself.
Type↓ :    Bundle (lsuc )
Type↓  = Type∙  , Type  , fst

Type↓-fibre :  {} (A : Type )  A  Pullback {B = Lift  } {C = Type∙ }  _  A) fst
Type↓-fibre A = Iso→Equiv λ where
  .fst a  pb _ (A , a) refl
  .snd .is-iso.from (pb _ (A' , a) eq)  transport (sym eq) a
  .snd .is-iso.linv  transport-refl
  .snd .is-iso.rinv (pb _ (A' , a) eq)  pb-path refl (sym (Σ-path (sym eq) refl)) λ i j  eq (i  j)

postulate
  -- We assume that Type↓ is an object classifier in the sense above, and show that
  -- this makes it a univalent universe.
  Type↓-is-classifier :  {}  is-classifier (Type↓ )

-- Every type is trivially a bundle over the unit type.
! :  {}  Type   Bundle 
! A = A , Lift _  , _

-- The key observation is that the type of pullback squares from ! A to Type↓ is
-- equivalent to the type of types equipped with an equivalence to A.
-- Since the former was assumed to be contractible, so is the latter.
lemma :  {} (A : Type )  (! A  Type↓ )  Σ (Type )  B  A  B)
lemma {} A = Iso→Equiv λ where
  .fst (ty , e , _)  ty _ , e ∙e Type↓-fibre (ty _) e⁻¹
  .snd .is-iso.from (B , e)   _  B) , e ∙e Type↓-fibre B , refl
  .snd .is-iso.linv (ty , e , _)  Σ-pathp refl (Σ-pathp (Σ-prop-path is-equiv-is-prop
    (funext λ _  Equiv.ε (Type↓-fibre (ty _)) _)) refl)
  .snd .is-iso.rinv (B , e)  Σ-pathp refl (Σ-prop-path is-equiv-is-prop
    (funext λ _  Equiv.η (Type↓-fibre B) _))

-- Equivalences form an identity system, which is another way to state univalence.
univalence :  {} (A : Type )  is-contr (Σ (Type ) λ B  A  B)
univalence {} A = Equiv→is-hlevel 0 (lemma A e⁻¹) (Type↓-is-classifier (! A))