open import Cat.Displayed.Instances.Pullback
open import Cat.Displayed.Instances.Slice
open import Cat.Displayed.Composition
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Functor
open import Cat.Diagram.Pullback
open import Cat.Displayed.Total
open import Cat.Instances.Slice
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

module Cat.Displayed.Instances.DisplayedFamilies
  {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ')
  where

open Cat.Reasoning B
open Displayed E
open Cat.Displayed.Reasoning E
open is-fibred-functor
open Functor

open Total-hom
open /-Obj
open Slice-hom

The displayed family fibration🔗

The family fibration is a critical part of the theory of fibrations, as it acts as a stepping off point for generalizing structure found in 1-categories to structures in fibrations. However, it is deeply entangled in the meta-theory, as it uses the fact that the type of objects of a precategory is, well, a type.

If we wish to generalize some 1-categorical phenomena, we will need a version of the family fibration that represents families internal to a fibration, where objects should be $\mathcal{B}\text{-indexed}$ families of $\mathcal{E}$ objects. To construct such a fibration, we recall that every family $P:X\to \mathrm{Type}$ is equivalent to the total space of its fibres (see here for more details). It’s quite rare for $\mathcal{B}$ to have something that looks like a universe, but it does have enough structure to talk about fibres! We can consider a morphism $\mathcal{B}(a,x)$ to be a sort of “generalized family” over $x\text{,}$ where $a$ is playing the role of the total space. Objects $a^{\prime }:{\mathcal{E}}_a$ over $a$ then encode an $x\text{-indexed}$ family of $\mathcal{E}$ objects.

This is all quite abstract, so let’s look at an example. Consider some category $\mathcal{E}$ fibred over $\mathbf{Sets}\text{.}$ There is already a natural notion of an $I\text{-indexed}$ family of $\mathcal{E}\text{-objects}$ here; namely, a map $P:I\to \mathrm{Set}$ and a map $X:(i:I)\to {\mathcal{E}}_{P(i)}\text{.}$ To see that we obtain the definition from before, note that we can turn this family of sets into a map $\mathrm{fst}:\Sigma (i:I)P(i)\to I$ by taking the total space of $P\text{.}$ Furthermore, $\Sigma (i:I)P(i)$ is a set, so we can consider the space of objects ${\mathcal{E}}_{\Sigma (i:I)P(i)}\text{.}$ We can embed each $X(i):E_{P(i)}$ into ${\mathcal{E}}_{\Sigma (i:I)P(i)}$ by reindexing along the second projection $\Sigma (i:I)P(i)\to P(i)$

To show the reverse direction, suppose we have some function $f:A\to I\text{,}$ along with an object ${\mathcal{E}}_A\text{.}$ We can obtain a family of sets $f^{-1}:I\to \mathrm{Set}$ by taking the fibres of $f\text{.}$ Furthermore, note that for each $i:I\text{,}$ we have a map $f^{-1}(i)\to A$ from the fibre of $f$ at $A$ to $A\text{;}$ reindexing along this map yields an object ${\mathcal{E}}_{f^{-1}(i)}$ as desired.

Now that we are armed with the intuition, on with the construction! Recall that the object objects over $x:\mathcal{B}$ shall be triples $(a:\mathcal{B})\times \mathcal{B}(a,x)\times {\mathcal{E}}_a\text{,}$ and morphisms $f:(a,f,a^{\prime })\to (b,g,b^{\prime })$ over $u:x\to y$ are given by triples $(k:\mathcal{B}(a,b))\times (u\circ f=g\circ k)\times {\mathcal{E}}_k(a^{\prime },b^{\prime })\text{.}$ The first portion of this data can be obtained by using the codomain fibration over $\mathcal{B}\text{.}$ The remaining data involving $\mathcal{E}$ is then added by composing the codomain fibration with the base change of $\mathcal{E}$ along the functor $\mathrm{Dom}:\int B^{\to }\to B$ that takes the domain of a morphism in the arrow category (which is the total category of the codomain fibration).

Dom : Functor (∫ (Slices B)) B
Dom .F₀ f = f .snd .domain
Dom .F₁ sq = sq .preserves .to
Dom .F-id = refl
Dom .F-∘ _ _ = refl

Disp-family : Displayed B (o ⊔ ℓ ⊔ o') (ℓ ⊔ ℓ')
Disp-family = Slices B D∘ Change-of-base Dom E

private
  module Disp-family = Displayed Disp-family

Now, that was quite a bit of abstract nonsense, so let’s verify that the nonsense actually makes sense by characterizing the objects and morphisms of our category. As expected, objects consist of the triples described above.

fam-over : ∀ {x} → (a : Ob) → Hom a x → Ob[ a ] → Disp-family.Ob[ x ]
fam-over a f a' .fst .domain = a
fam-over a f a' .fst .map = f
fam-over a f a' .snd = a'

module Fam-over {x} (P : Disp-family.Ob[ x ]) where

  tot : Ob
  tot = P .fst .domain

  fam : Hom tot x
  fam = P .fst .map

  tot' : Ob[ tot ]
  tot' = P .snd

open Fam-over

We glossed over the morphisms above, so let’s go more into detail here. A morphism between displayed families $P,Q$ is given by a map between $\mathcal{B}\text{-valued}$ total spaces; this map must commute with the family structure on $P$ and $Q\text{.}$ Finally, we have a map between the $\mathcal{E}\text{-valued}$ total spaces.

module Fam-over-hom
  {x y} {u : Hom x y} {P : Disp-family.Ob[ x ]} {Q : Disp-family.Ob[ y ]}
  (fᵢ : Disp-family.Hom[ u ] P Q)
  where

  map-tot : Hom (tot P) (tot Q)
  map-tot = fᵢ .fst .to

  fam-square : u ∘ fam P ≡ fam Q ∘ map-tot
  fam-square = fᵢ .fst .commute

  map-tot' : Hom[ map-tot ] (tot' P) (tot' Q)
  map-tot' = fᵢ .snd

open Fam-over-hom

fam-over-hom
  : ∀ {x y} {u : Hom x y} {P : Disp-family.Ob[ x ]} {Q : Disp-family.Ob[ y ]}
  → (f : Hom (tot P) (tot Q))
  → u ∘ fam P ≡ fam Q ∘ f
  → Hom[ f ] (tot' P) (tot' Q)
  → Disp-family.Hom[ u ] P Q
fam-over-hom f p f' .fst .to = f
fam-over-hom f p f' .fst .commute = p
fam-over-hom f p f' .snd = f'

As a fibration🔗

If $\mathcal{E}$ is a fibration, and $\mathcal{B}$ has all pullbacks, then the category of displayed families is also a fibration. This follows by more abstract nonsense. In fact, this proof is why we defined it using abstract nonsense!

module _
  (fib : Cartesian-fibration E)
  (pb : ∀ {x y z} (f : Hom x y) (g : Hom z y) → Pullback B f g)
  where

  Disp-family-fibration : Cartesian-fibration Disp-family
  Disp-family-fibration =
    fibration-∘ (Codomain-fibration B pb) (Change-of-base-fibration Dom E fib)

Constant families🔗

There is a vertical functor from $\mathcal{E}$ to the category of $\mathcal{E}\text{-valued}$ families that takes each ${\mathcal{E}}_x$ to the constant family.

ConstDispFam : Vertical-functor E Disp-family
ConstDispFam .Vertical-functor.F₀' {x = x} x' =
  fam-over x id x'
ConstDispFam .Vertical-functor.F₁' {f = f} f' =
  fam-over-hom f id-comm f'
ConstDispFam .Vertical-functor.F-id' =
  Slice-pathp B refl refl ,ₚ sym (transport-refl _)
ConstDispFam .Vertical-functor.F-∘' =
  Slice-pathp B refl refl ,ₚ sym (transport-refl _)

This functor is in fact fibred, though the proof is somewhat involved!

ConstDispFam-fibred : is-fibred-functor ConstDispFam
ConstDispFam-fibred .F-cartesian {a = a} {b} {a'} {b'} {f} {f'} f'-cart = cart where
  open Vertical-functor ConstDispFam
  module f' = is-cartesian f'-cart
  open is-cartesian

We begin by fixing some notation for the constant family on b'.

  Δb' : Disp-family.Ob[ b ]
  Δb' = fam-over b id b'

Next, a short yet crucial lemma: if we have a displayed family over $x\text{,}$ a map $m:\mathcal{B}(x,a)\text{,}$ and a morphism of displayed families from $P$ to the constant family on $b^{\prime }\text{,}$ then we can construct a map from the displayed total space of $P$ to $a^{\prime }\text{.}$ This is constructed via the universal map of the cartesian morphism $f^{\prime }\text{.}$

  coh : ∀ {x : Ob} {P : Disp-family.Ob[ x ]}
      → (m : Hom x a) (h' : Disp-family.Hom[ f ∘ m ] P Δb')
      → f ∘ (m ∘ fam P) ≡ map-tot h'
  coh m h' = assoc _ _ _ ∙ fam-square h' ∙ idl _

  tot-univ : {x : Ob} {P : Disp-family.Ob[ x ]} (m : Hom x a)
    → (h' : Disp-family.Hom[ f ∘ m ] P Δb')
    → Hom[ m ∘ fam P ] (tot' P) a'
  tot-univ {P = P} m h' =
    f'.universal (m ∘ fam P) $ hom[ coh m h' ]⁻ (map-tot' h')

We can use this lemma to construct a universal map in $\mathcal{E}\text{.}$

  cart : is-cartesian Disp-family f (F₁' f')
  cart .universal {u' = u'} m h' =
    fam-over-hom (m ∘ fam u') (sym (idl _)) (tot-univ m h')

Commutivity and uniqueness follow from the fact that $f^{\prime }$ is cartesian.

  cart .commutes {x} {P} m h' =
    Σ-path (Slice-pathp B _ (coh m h')) $ from-pathp $ cast[] $
      hom[] (f' ∘' map-tot' (cart .universal m h')) ≡[]⟨ ap hom[] (f'.commutes _ _) ⟩
      hom[] (hom[] (map-tot' h'))                   ≡[ coh m h' ]⟨ to-pathp⁻ (hom[]-∙ _ _ ∙ reindex _ _) ⟩
      map-tot' h' ∎
  cart .unique {x} {P} {m = m} {h' = h'} m' p =
    Σ-path (Slice-pathp B refl (sym (fam-square m' ∙ idl _)))
    $ f'.unique _ $ from-pathp⁻ $ cast[] {q = coh m h'} $
      f' ∘' hom[] (map-tot' m') ≡[]⟨ to-pathp (smashr _ (ap (f ∘_) (fam-square m' ∙ idl _)) ∙ reindex _ _) ⟩
      hom[] (f' ∘' map-tot' m') ≡[]⟨ ap map-tot' p ⟩
      map-tot' h'               ∎