🔍

Equations Inline Footnotes

open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Morphism
import Cat.Morphism

module Cat.Displayed.Isofibration where

private
  variable
    ob ℓb oe ℓe : Level
    B : Precategory ob ℓb

  level : {B : Precategory ob ℓb} → Displayed B oe ℓe → Level
  level {ob = ob} {ℓb = ℓb} {oe = oe} {ℓe = ℓe} _ = ob ⊔ ℓb ⊔ oe ⊔ ℓe

Isofibrations🔗

record Isofibration (E : Displayed B oe ℓe) : Type (level E) where

  no-eta-equality

  open Cat.Displayed.Morphism E
  open Cat.Morphism B
  open Displayed E

An isofibration $\mathcal{E}\mathcal{B}$ is a displayed category admitting a notion of transport between fibres over isomorphic objects. Explicitly, this means that every lifting diagram of the form below can be extended to one with the dotted arrows, where both $u$ is an isomorphism and $u^{\prime }$ an isomorphism over $u\text{.}$

  field
    _^*_     : ∀ {a b} (u : a ≅ b) (a' : Ob[ a ]) → Ob[ b ]
    ^*-lifts : ∀ {a b} (u : a ≅ b) (a' : Ob[ a ]) → a' ≅[ u ] (u ^* a')

  private
    open module ^*-lifts {a b} {f : a ≅ b} {x : Ob[ a ]} = _≅[_]_ (^*-lifts f x)
      public using ()
      renaming (to' to π* ; from' to ι!)

We write the components of the displayed isomorphism ^*-lifts as π* and ι!: these are, respectively, maps $u^{\ast }{b}^{\prime }\to b^{\prime }$ and $b^{\prime }\to u^{\ast }{b}^{\prime }\text{.}$ Since they are invertible, they provide cartesian (respectively cocartesian) lifts of $b^{\prime }$ along $u\text{.}$

  π*-is-cartesian   : ∀ {a b} (u : a ≅ b) b' → is-cartesian   E (u .to)   π*
  ι!-is-cocartesian : ∀ {a b} (u : a ≅ b) b' → is-cocartesian E (u .from) ι!

  π*-is-cartesian u x = invertible→cartesian E _ $
    iso[]→invertible[] (^*-lifts u x)

  ι!-is-cocartesian u x = invertible→cocartesian E _ $
    iso[]→invertible[] (^*-lifts u x Iso[]⁻¹)

Over categories🔗

{-# INLINE Isofibration.constructor #-}

module _ {B : Precategory ob ℓb} (E : Displayed B oe ℓe) (bcat : is-category B) where
  open Cat.Displayed.Morphism E
  open Displayed E

  open Univalent bcat
  open Isofibration

If $\mathcal{B}$ is univalent, then every category $\mathcal{E}\mathcal{B}$ displayed over it is an isofibration. This follows by a simple argument using isomorphism induction. We first rearrange the data of Isofibration into a family of products that manifestly depends on the objects $a,b:\mathcal{B}$ and the isomorphism $a\cong b\text{.}$ It is easy to rearrange a section of this family into an instance of Isofibration.

  private
    Lifts : ∀ {a} b (u : a ≅ b) → Type _
    Lifts {a} b u = (a' : E ʻ a) → Σ[ b' ∈ E ʻ b ] (a' ≅[ u ] b')

    from-lifts : (∀ {a b} u → Lifts {a} b u) → Isofibration E
    from-lifts l ._^*_     u b' = l u b' .fst
    from-lifts l .^*-lifts u b' = l u b' .snd

The reason for this rephrasing is that Lifts is precisely a motive for isomorphism induction. Accordingly, to obtain a section of this family, it suffices to give isomorphic lifts along the identity; for which we may take the identity isomorphism, completing the proof.

  is-category→isofibration : Isofibration E
  is-category→isofibration = from-lifts $ J-iso Lifts λ b' →
    b' , id-iso↓