🔍

Equations Inline Footnotes

open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Closure
open import 1Lab.Reflection
open import 1Lab.Underlying
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type hiding (id ; _∘_)

open import Cat.Base

module Cat.Displayed.Base where

Displayed categories🔗

Any functor $P:\mathcal{E}\to \mathcal{B}$ can be thought of as decomposing the precategory $\mathcal{E}$ into a family $P_{\bullet }$ of categories indexed by the objects $x:\mathcal{B}\text{,}$¹ where the objects of $P_x$ should be those objects of $\mathcal{E}$ sent to $x$ by $P$, in a situation analogous to how functions $f:A\to B$ decompose their domain $A$ as a sum, namely of the fibres of $f$ over the points of $B\text{.}$

Indeed, a literal approach to this decomposition would define the type of objects of $P_x$ to be exactly the type-theoretic fibre $P^{\ast }x\text{.}$ In our setting, this interpretation is problematic for two complementary reasons. First, if $\mathcal{B}$ is an arbitrary precategory, the path types of its type of objects should be regarded as a vestigial structure left over from the encoding of category theory into type theory, and not as an intrinsic property of the category.

This objection is addressed by considering only functors into univalent categories, which are precisely those where identity of objects corresponds coherently to isomorphism in the category. However, even when studying univalent categories, the non-univalent constructions of diagram shapes like the walking isomorphism are often more convenient to formalise with than their univalent versions.²

If we insist on talking about fibres, we might instead work with Street fibrations, or, in greater generality, an equivalent weakening of the notion of isofibration. Talking about essential fibres would be independent of the path types of a presentation of a given category, so our first objection is addressed. However, even this definition has a critical flaw, which is actually common to any definition based on fibres: it is extremely inconvenient to work with in intensional type theory.

For example, the action of $P$ on morphisms has type-theoretic fibres only over maps $\mathcal{B}(P(x),P(y))\text{,}$ so that if we have objects $(x^{\prime },p):P^{\ast }(x)$ and $(y^{\prime },q):P^{\ast }(y)\text{,}$ to talk about maps $x^{\prime }\to y^{\prime }$ lying over $f:\mathcal{B}(x,y)\text{,}$ we must instead consider the fibres of the map $$\mathcal{E}(x^{\prime },y^{\prime })\stackrel{P}{\to }\mathcal{B}(P(x^{\prime }),P(y^{\prime }))\stackrel{{\mathrm{subst}}_2\mathcal{B}(-,-)\dots }{\to }\mathcal{B}(x,y)\text{,}$$ where the elided term in the second map makes explicit reference to the identifications $p:P(x^{\prime })=x\text{,}$ resp. $q:P(y^{\prime })=y\text{,}$ witnessing that $x^{\prime }$ lies over $x$ (resp. $y^{\prime }$ over $y\text{).}$ Any construction on an object $x^{\prime }$ lying over $x$ must regard the manner through which $P(x^{\prime })$ and $x$ were identified, regardless of whether this is a path or an isomorphism.

The gist of these two objections is that, even if we work with a suitably natural weakening of the fibres of $P\text{,}$ the result is still impractical to formalise with. We would prefer to work with a notion of “dependent category” that is as convenient as the native notion of dependent type. Moving from fibrations to families prioritises the decomposition of $\mathcal{E}$ over $\mathcal{B}\text{,}$ by making the notion of being defined over $x:\mathcal{B}$ primitive.

A displayed category $\mathcal{E}\mathcal{B}$ is an equivalent representation of the pair $(\mathcal{E},P)\text{,}$ with one direction of the equivalence being the construction of total categories and the other being that of free isofibrations. Unlike starting with functors, displayed categories bake in the indexing by objects in the base category, so that “an object $x^{\prime }$ over an object $x$” is an atomic notion, needing no witness. Both the construction and study of displayed categories is often simpler than working with functors:

• Every category³ $\mathcal{E}$ whose objects are described in natural language as “an object of $\mathcal{B}\text{,}$ equipped with such-and-such structure”, and whose maps are “such-and-such preserving maps”, is naturally a displayed category, where the type of objects over $x:\mathcal{B}$ is the type of “such-and-such structures” with carrier $x\text{.}$

  A fibre category of $\mathcal{E}\text{-qua-displayed-category}$ over $x$ has, as its type of objects, precisely the type of structures with carrier $x\text{;}$ if we instead considered $(\mathcal{E},U)$ as a category-functor pair, the objects of $U^{\ast }(x)$ would consist of nested triples $((x^{\prime },S),\phi )$ where $x^{\prime }:\mathcal{B}\text{,}$ $S$ is a structure with carrier $x^{\prime }\text{,}$ and $\phi :x^{\prime }\cong x\text{.}$

  Many properties of the forgetful functor, like being faithful, fully faithful, or amnestic, become simpler when phrased as properties of its generating displayed category. For example, it is faithful when each Hom[_] is a proposition, and amnestic when $\mathcal{E}$ is displayed univalent.

• Naturally, focusing on indexing makes displayed categories a great fit for the study of indexed categories, and results in notions that make no reference to identity of objects. Concepts in this direction include Cartesian, right, discrete, and iso-fibrations; concrete examples include the canonical self-indexing, the family fibration, and the externalisations of internal categories.

  Additionally, the notion of section of a displayed category captures the idea that a category $\mathcal{B}$ may be initial among some class of structure categories in terms of an eliminator, so that the values of the section definitionally lie over the inputs in $\mathcal{B}\text{.}$ This rephrasing was instrumental to the formalisation of free Cartesian closed categories.

The definition🔗

private
  variable o ℓ : Level
  lvl : ∀ {o ℓ} → Precategory o ℓ → Level → Level → Level
  lvl {o} {ℓ} _ o' ℓ' = o ⊔ ℓ ⊔ lsuc (o' ⊔ ℓ')

record Displayed (B : Precategory o ℓ) o' ℓ' : Type (lvl B o' ℓ') where

  no-eta-equality
  open Precategory B
  infixr  _∘'_
  infix  _≡[_]_

A displayed category $\mathcal{E}$ is specified in terms of a family Ob[_] of objects, indexed by those of $\mathcal{B}\text{;}$ we write ${\mathcal{E}}_x$ for the value of the family at $x:\mathcal{B}\text{,}$ and if $x^{\prime }:{\mathcal{E}}_x\text{,}$ we may write $x^{\prime }x$ if $\mathcal{E}$ is understood. We then have a family of sets Hom[_], indexed by a map $f:\mathcal{B}(x,y)\text{,}$ and objects $x^{\prime }x$ and $y^{\prime }y\text{;}$ we write $x^{\prime }{\to }_f{y}^{\prime }$ for its values.

  field
    Ob[_]  : ⌞ B ⌟ → Type o'
    Hom[_] : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ] → Type ℓ'

    Hom[_]-set
      : ∀ {a b} (f : Hom a b) (x : Ob[ a ]) (y : Ob[ b ])
      → is-set (Hom[ f ] x y)

A displayed category is also equipped with the algebraic operations of a category — identity and composition — where each is indexed by its corresponding operations in $\mathcal{B}\text{.}$ That is to say, the “identity over”, id', is a map $x^{\prime }{\to }_{\mathrm{id}}{x}^{\prime }\text{,}$ and, given composable $f^{\prime }:y^{\prime }{\to }_f{z}^{\prime }$ and $g^{\prime }:x^{\prime }{\to }_g{y}^{\prime }\text{,}$ their “composite over”, _∘'_, lives in $x^{\prime }{\to }_{f\circ g}{z}^{\prime }\text{.}$

    id' : ∀ {a} {x : Ob[ a ]} → Hom[ id ] x x
    _∘'_
      : ∀ {a b c x y z} {f : Hom b c} {g : Hom a b}
      → Hom[ f ] y z → Hom[ g ] x y → Hom[ f ∘ g ] x z

These operations are required to satisfy the laws analogous to those of a category. However, considering (e.g.) the left identity law, we run into a problem when stating them as equations: The composite $$(\mathrm{id}\circ f^{\prime }):x^{\prime }{\to }_{\mathrm{id}\circ f}{y}^{\prime }$$ is displayed over a map that is not definitionally equal to $f\text{,}$ but only identical to it by a law of the base category. Therefore, the laws of a displayed category $\mathcal{E}\mathcal{B}$ must be dependent on the corresponding laws in $\mathcal{B}\text{.}$ We introduce the notation _≡[_]_, which will be written $f^{\prime }{\equiv }_p{g}^{\prime }$ when necessary, to compare maps $f^{\prime }:x^{\prime }{\to }_f{y}^{\prime }$ and $g^{\prime }:x^{\prime }{\to }_{g}y$ over an identification $p:f\equiv g\text{.}$

  _≡[_]_
    : ∀ {a b x y} {f g : Hom a b} → Hom[ f ] x y → f ≡ g → Hom[ g ] x y → Type ℓ'
  _≡[_]_ {a} {b} {x} {y} f' p g' = PathP (λ i → Hom[ p i ] x y) f' g'

This makes it straightforward to write down the three laws, though they remain quite wordy.

  field
    idr' : ∀ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) → f' ∘' id' ≡[ idr f ] f'
    idl' : ∀ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) → id' ∘' f' ≡[ idl f ] f'
    assoc'
      : ∀ {a b c d w x y z} {f : Hom c d} {g : Hom b c} {h : Hom a b}
      → (f' : Hom[ f ] y z) (g' : Hom[ g ] x y) (h' : Hom[ h ] w x)
      → f' ∘' (g' ∘' h') ≡[ assoc f g h ] ((f' ∘' g') ∘' h')

Finally, we can equip displayed categories with a distinguished transport operation for moving displayed morphisms between equal bases. While in general there may be many such, we can pair the “homwise transport” hom[_] operation with a coherence datum coh[_], and this pair inhabits a contractible type (a centre of contraction being the native subst operation, paired with its filler). Therefore, these fields do not affect the “homotopy type” of Displayed.

Their purpose is strictly as an aid in mechanisation: often (e.g. in the fundamental fibration $\underline{\mathcal{B}}\text{),}$ the type $x{\to }_{f}y$ consists of some “relevant” data together with some “irrelevant” propositions, and, importantly, only the propositions mention the base morphism $f$. This means that a “bespoke” hom[_] implementation can then choose to leave the data fields definitionally unchanged, whereas the native subst would surround them with reflexive transports.

Counterintuitively, this extra field actually increases reusability, despite nominally increasing the amount of data that goes into a displayed category: If another construction needs to transport morphisms in $\underline{\mathcal{B}}$ to work, e.g. the pullback fibration for sconing or Artin gluing, or fibre categories of subobjects, dealing with the leftover substs that arise in (e.g.) composition of morphisms can be quite annoying, and while cleaning them up can be automated, using the “bespoke” transport avoids introducing them in the first place.

  field
    hom[_]
      : ∀ {a b x y} {f g : Hom a b} (p : f ≡ g) (f' : Hom[ f ] x y)
      → Hom[ g ] x y
    coh[_]
      : ∀ {a b x y} {f g : Hom a b} (p : f ≡ g) (f' : Hom[ f ] x y)
      → f' ≡[ p ] hom[ p ] f'

Developer documentation🔗

  private variable
    a b : Ob
    a' b' x y : Ob[ a ]

    e f g h : Hom a b
    e' f' g' h' : Hom[ f ] a' b'
    p q r s : f ≡ g
    p' q' r' s' : f' ≡[ p ] g'

Operators for composing paths-over🔗

Since Mikan often struggles to infer the arguments to the generic displayed composition operator _∙P_ in the setting of displayed categories, we provide variants which specify that the dependency is only on paths in the base category. One variant (∙[-]-syntax) takes the path over which the left argument is displayed explicitly, and the other _∙[]_ does this implicitly.

  ∙[-]-syntax
    : (p : f ≡ g) {q : g ≡ h}
    → f' ≡[ p ] g' → g' ≡[ q ] h' → f' ≡[ p ∙ q ] h'
  ∙[-]-syntax p p' q' = _∙P_ {B = λ f → Hom[ f ] _ _} p' q'

  syntax ∙[-]-syntax p p' q' = p' ∙[ p ] q'

  _∙[]_ : {p : f ≡ g} {q : g ≡ h} → f' ≡[ p ] g' → g' ≡[ q ] h' → f' ≡[ p ∙ q ] h'
  _∙[]_ p' q' = p' ∙[ _ ] q'

  infixr  _∙[]_ ∙[-]-syntax

Equational reasoning in displayed categories🔗

Unlike non-dependent path composition, which elaborates to terms whose size is linear in the number of steps, iterated composition of dependent paths has a quadratic overhead. This comes from the composition operator having to be quantified over the paths over which its arguments are dependent:

  -- Generalisation really doesn't like generalising over the bases here
  module
    _ {a b} {d e f g h : Hom a b} {p : d ≡ e} {q : e ≡ f} {r : f ≡ g} {s : g ≡ h}
    where

    _ : p' ∙[] q' ∙[] r' ∙[] s' ≡
      _∙[]_      {p = p} {q = q ∙ r ∙ s} p'
        (_∙[]_   {p = q} {q = r ∙ s}     q'
          (_∙[]_ {p = r} {q = s}         r'
            s'))
    _ = refl

Predictably, this is quite bad for performance: any part of the proof assistant implementation which needs to traverse terms will spend $O(n^2)$ time going through this information.

Surprisingly, we can alleviate this without having to alter the proof assistant implementation, by working instead with paths in the total space of $x^{\prime }{\to }_{-}{y}^{\prime }\text{,}$ as a family over $x\to y\text{.}$ We introduce an auxiliary type _∫≡_, from which we can project a path in $x^{\prime }{\to }_{-}{y}^{\prime }\text{,}$ either over the constructed path between the base maps, or (because $\mathbf{Hom}\text{-sets}$ are sets) over an arbitrary path in the base.

  _∫≡_ : Hom[ f ] x y → Hom[ g ] x y → Type _
  f' ∫≡ g' = Path (Σ (Hom _ _) λ f → Hom[ f ] _ _) (_ , f') (_ , g')

  begin_ : (p : f' ∫≡ g') → f' ≡[ ap fst p ] g'
  begin_ = ap snd

  begin[]_ : f' ∫≡ g' → f' ≡[ p ] g'
  begin[]_ {f' = f'} {g' = g'} p = subst (f' ≡[_] g') prop! (ap snd p)

  infix  begin_ begin[]_

We can then provide combinators for composing a path in the total space with an ordinary dependent path, with variants for explicitly specifying the base path and for inverting the path to be composed.

  ≡[-]⟨⟩-syntax
    : (f' : Hom[ f ] x y) (p : f ≡ g) → g' ∫≡ h' → f' ≡[ p ] g' → f' ∫≡ h'
  ≡[-]⟨⟩-syntax f' p q' p' = ap₂ _,_ (p ∙ ap fst q') (p' ∙[] ap snd q')

  ≡[]⟨⟩-syntax : (f' : Hom[ f ] x y) → g' ∫≡ h' → f' ≡[ p ] g' → f' ∫≡ h'
  ≡[]⟨⟩-syntax {p = p} f' q' p' = f' ≡[ _ ]⟨ p' ⟩] q'

  ≡[]˘⟨⟩-syntax : (f' : Hom[ f ] x y) → g' ∫≡ h' → g' ≡[ p ] f' → f' ∫≡ h'
  ≡[]˘⟨⟩-syntax f' q' p' = f' ≡[]⟨ symP p' ⟩≡[] q'

  syntax ≡[-]⟨⟩-syntax f' p q' p' = f' ≡[ p ]⟨ p' ⟩ q'
  syntax ≡[]⟨⟩-syntax f' q' p' = f' ≡[]⟨ p' ⟩ q'
  syntax ≡[]˘⟨⟩-syntax f' q' p' = f' ≡[]˘⟨ p' ⟩ q'

  infixr  ≡[-]⟨⟩-syntax ≡[]⟨⟩-syntax ≡[]˘⟨⟩-syntax

Finally, for the final step, we must provide a slight variation on the reflexivity operator which pairs the given displayed map with its base.

  _∎[] : (f' : Hom[ f ] x y) → f' ∫≡ f'
  _∎[] _ = refl

  infix  _∎[]

record Trivially-graded {o ℓ} (B : Precategory o ℓ) (o' ℓ' : Level) : Type (o ⊔ ℓ ⊔ lsuc o' ⊔ lsuc ℓ') where
  open Precategory B
  field
    Ob[_]  : Ob → Type o'
    Hom[_] : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ] → Type ℓ'

    instance
      ⦃ H-Level-Hom[_] ⦄
        : ∀ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
        → H-Level (Hom[ f ] x y) 

    id'  : ∀ {a} {x : Ob[ a ]} → Hom[ id ] x x
    _∘'_ : ∀ {a b c x y z} {f : Hom b c} {g : Hom a b}
         → Hom[ f ] y z → Hom[ g ] x y → Hom[ f ∘ g ] x z

  infixr  _∘'_

  _≡[_]_ : ∀ {a b x y} {f g : Hom a b} → Hom[ f ] x y → f ≡ g → Hom[ g ] x y → Type ℓ'
  _≡[_]_ {a} {b} {x} {y} f' p g' = PathP (λ i → Hom[ p i ] x y) f' g'

  infix  _≡[_]_
  field
    idr' : ∀ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) → (f' ∘' id') ≡[ idr f ] f'
    idl' : ∀ {a b x y} {f : Hom a b} (f' : Hom[ f ] x y) → (id' ∘' f') ≡[ idl f ] f'
    assoc'
      : ∀ {a b c d w x y z} {f : Hom c d} {g : Hom b c} {h : Hom a b}
      → (f' : Hom[ f ] y z) (g' : Hom[ g ] x y) (h' : Hom[ h ] w x)
      → f' ∘' (g' ∘' h') ≡[ assoc f g h ] ((f' ∘' g') ∘' h')

{-# INLINE Displayed.constructor #-}

record Thinly-displayed {o ℓ} (B : Precategory o ℓ) (o' ℓ' : Level) : Type (o ⊔ ℓ ⊔ lsuc o' ⊔ lsuc ℓ') where
  open Precategory B
  field
    Ob[_]  : Ob → Type o'
    Hom[_] : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ] → Type ℓ'

    instance
      ⦃ H-Level-Hom[_] ⦄
        : ∀ {a b} {f : Hom a b} {x : Ob[ a ]} {y : Ob[ b ]}
        → H-Level (Hom[ f ] x y) 

    id'  : ∀ {a} {x : Ob[ a ]} → Hom[ id ] x x
    _∘'_ : ∀ {a b c x y z} {f : Hom b c} {g : Hom a b}
         → Hom[ f ] y z → Hom[ g ] x y → Hom[ f ∘ g ] x z

Constructing displayed categories🔗

We provide helpers for constructing displayed categories in two common cases.

The with-trivial-grading helper fills in the grading fields, hom[_] and coh[_], with their canonical implementations in terms of transport.

with-trivial-grading
  : ∀ {o ℓ} {B : Precategory o ℓ} {o' ℓ' : Level} → Trivially-graded B o' ℓ'
  → Displayed B o' ℓ'
{-# INLINE with-trivial-grading #-}
with-trivial-grading triv = record
  { Trivially-graded triv
  ; Hom[_]-set = λ f x y → hlevel 
  ; hom[_]     = subst (λ e → Hom[ e ] _ _)
  ; coh[_]     = λ p → transport-filler _
  }
  where open Trivially-graded triv using (Hom[_] ; H-Level-Hom[_])

The with-thin-display helper additionally automatically derives the displayed category laws from a mechanical proof that the given Hom[_] family is propositional.

with-thin-display
  : ∀ {o ℓ} {B : Precategory o ℓ} {o' ℓ' : Level} → Thinly-displayed B o' ℓ'
  → Displayed B o' ℓ'
{-# INLINE with-thin-display #-}
with-thin-display triv = with-trivial-grading record where
  open Thinly-displayed triv
    using (Ob[_] ; Hom[_] ; id' ; _∘'_) renaming (H-Level-Hom[_] to i)
  H-Level-Hom[_] = basic-instance  $ is-prop→is-set (hlevel )
  idr'   f     = prop!
  idl'   f     = prop!
  assoc' f g h = prop!

open hlevel-projection

private
  Hom[]-set
    : ∀ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') {x y} {f : B .Precategory.Hom x y} {x' y'}
    → is-set (E .Displayed.Hom[_] f x' y')
  Hom[]-set E = E .Displayed.Hom[_]-set _ _ _

instance
  Hom[]-hlevel-proj : hlevel-projection (quote Displayed.Hom[_])
  Hom[]-hlevel-proj .has-level   = quote Hom[]-set
  Hom[]-hlevel-proj .get-level _ = pure (lit (nat ))
  Hom[]-hlevel-proj .get-argument = first-visible

  Funlike-Displayed : ∀ {o ℓ o' ℓ'} {B : Precategory o ℓ} → Funlike (Displayed B o' ℓ') ⌞ B ⌟ λ _ → Type o'
  Funlike-Displayed = record { _·_ = Displayed.Ob[_] }

module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} {E : Displayed B o' ℓ'} where
  _ : ∀ {x y} {f : B .Precategory.Hom x y} {x' y'} → is-set (E .Displayed.Hom[_] f x' y')
  _ = hlevel