module Cat.Displayed.Instances.Family {o h} (C : Precategory o h) where

The family fibration🔗

We can canonically treat any Precategory as being displayed over Sets, regardless of the size of the object- and Hom-spaces of

In a neutral presentation of displayed category theory, the collection of objects over would be given by the space of functors regarding as a discrete category. This is essentially an family of objects of hence the name “family fibration”. To reduce the noise, however, in HoTT we can (ab)use the fact that all precategories have a space of objects, and say that the objects over are precisely the families

Family :  {}  Displayed (Sets ) _ _
Family .Ob[_] S =  S   Ob

The set of maps over a function (in is the set of families of morphisms Here we are abusing that, for functors between discrete categories, naturality is automatic.

Family .Hom[_] {A} {B} f F G =
   x  Hom (F x) (G (f x))
Family .Hom[_]-set f x y = hlevel 2

The identity and composition operations are as for natural transformations, but without the requirement for naturality.

Family .id' x = id
Family ._∘'_ {f = f} {g = g} f' g' x = f' (g x)  g' x
Family .idr' _ = funext λ x  idr _
Family .idl' _ = funext λ x  idl _
Family .assoc' _ _ _ = funext λ _  assoc _ _ _

The family fibration is a Cartesian fibration, essentially by solving an associativity problem. Given a function and a family over we must define a family over and give a universal family of functions But we may simply take and family is constantly the identity map.

open Cartesian-fibration
open Cartesian-lift
open is-cartesian

Family-is-cartesian :  {}  Cartesian-fibration (Family { = })
Family-is-cartesian = iscart where
  cart :  {x y : Set _} (f :  x    y )
           (y' :  y   Ob)
        is-cartesian Family f λ _  id
  cart f y' .universal m nt = nt
  cart f y' .commutes m h' = funext λ _  idl _
  cart f y' .unique m' p = funext λ _  introl refl  happly p _

  iscart : Cartesian-fibration Family
  iscart .has-lift f y' .x' z = y' (f z)
  iscart .has-lift f y' .lifting x = id
  iscart .has-lift {x = x} {y} f y' .cartesian = cart {x = x} {y} f y'

Morphisms in the family fibration are cartesian if and only if they are pointwise isomorphisms. Showing the forward direction is a matter of using the inverse to construct the factorisation, and then applying the isomorphism equations to show that we’ve actually constructed the unique factorisation.

pointwise-iso→cartesian
  :  {} {X Y : Set } {f :  X    Y }
   {P :  X   Ob} {Q :  Y   Ob} {fₓ :  x  Hom (P x) (Q (f x))}
   (∀ x  is-invertible (fₓ x))
   is-cartesian Family {X} {Y} {P} {Q} f fₓ
pointwise-iso→cartesian {fₓ = fₓ} fₓ-inv = fₓ-cart where
  module fₓ-inv x = is-invertible (fₓ-inv x)

  fₓ-cart : is-cartesian Family _ fₓ
  fₓ-cart .universal m h' x =
    fₓ-inv.inv (m x)  h' x
  fₓ-cart .commutes m h' =
    funext λ x  cancell (fₓ-inv.invl (m x))
  fₓ-cart .unique {m = m} m' p =
    funext λ x  introl (fₓ-inv.invr (m x))  pullr (happly p x)

Showing the backwards direction requires using the usual trick of factorizing the identity morphism; this is an isomorphism due to the fact that the factorisation is unique.

cartesian→pointwise-iso
  :  {} {X Y : Set } {f :  X    Y }
   {P :  X   Ob} {Q :  Y   Ob} {fₓ :  x  Hom (P x) (Q (f x))}
   is-cartesian Family {X} {Y} {P} {Q} f fₓ
   (∀ x  is-invertible (fₓ x))
cartesian→pointwise-iso {X = X} {f = f} {P = P} {Q = Q} {fₓ = fₓ} fₓ-cart x =
  make-invertible
    fₓ⁻¹
    (happly (fₓ-cart.commutes _ _) x)
    (happly (fₓ-cart.unique {u = X}  _  fₓ⁻¹  fₓ x) (funext λ _  cancell (happly (fₓ-cart.commutes _ _) x))) x 
     sym (happly (fₓ-cart.unique  _  id) (funext λ _  idr _)) x))
  where
    module fₓ-cart = is-cartesian fₓ-cart

    fₓ⁻¹ : Hom (Q (f x)) (P x)
    fₓ⁻¹ = fₓ-cart.universal {u = X}  x  x)  _  id) x

Fibres🔗

We now prove that the fibres of the family fibration are indeed the expected functor categories. This involves a bit of annoying calculation, but it will let us automatically prove that the family fibration is fibrewise univalent whenever is.

module _ {} (X : Set ) where
  private
    lift-f = Disc-adjunct {C = C} {iss = is-hlevel-suc 2 (X .is-tr)}
    module F = Cat.Reasoning (Fibre Family X)

  Families→functors : Functor (Fibre Family X) Cat[ Disc' X , C ]
  Families→functors .F₀ = Disc-adjunct
  Families→functors .F₁ f .η = f
  Families→functors .F₁ {X} {Y} f .is-natural x y =
    J  y p  f y  lift-f X .F₁ p  lift-f Y .F₁ p  f x)
      (ap (f x ∘_) (lift-f X .F-id) ·· id-comm ·· ap (_∘ f x) (sym (lift-f Y .F-id)))
  Families→functors .F-id = trivial!
  Families→functors .F-∘ f g =
    ap (Families→functors .F₁) (transport-refl _)  trivial!

  Families→functors-is-ff : is-fully-faithful Families→functors
  Families→functors-is-ff = is-iso→is-equiv
    (iso η  x  trivial!) λ x  refl)

  open is-precat-iso
  Families→functors-is-iso : is-precat-iso Families→functors
  Families→functors-is-iso .has-is-ff = Families→functors-is-ff
  Families→functors-is-iso .has-is-iso = is-iso→is-equiv $ iso F₀
     x  Functor-path  _  refl)
      (J  _ p  lift-f (x .F₀) .F₁ p  x .F₁ p)
          (lift-f (x .F₀) .F-id  sym (x .F-id))))
     x  refl)

  Families-are-categories : is-category C  is-category (Fibre Family X)
  Families-are-categories isc .to-path im = funext λ x 
    isc .to-path $ make-iso (im .F.to x) (im .F.from x)
      (happly (sym (transport-refl  y  im .F.to y  im .F.from y))  im .F.invl) x)
      (happly (sym (transport-refl  y  im .F.from y  im .F.to y))  im .F.invr) x)
  Families-are-categories isc .to-path-over im = F.≅-pathp refl _ $ funextP λ a 
    Hom-pathp-reflr C (elimr refl  ap to (Univalent.iso→path→iso isc _))

Generic objects🔗

The family fibration on has a generic object if and only if is equivalent to a strict, small category. We begin by showing the forward direction.

Family-generic-object→Strict-equiv
  : Globally-small (Family {h})
   Σ[ Strict  Precategory h h ]
    (is-set  Strict  × Equivalence Strict C)
Family-generic-object→Strict-equiv small =
  Strict , hlevel! , eqv module Family-generic-object-strict where
  open Globally-small small

The main idea of the proof is that we can replace the type of objects of with the base component of the generic object which is a small set. The displayed component of the generic object gives us a family of objects over which we use to define morphisms of our strict category.

  Strict : Precategory h h
  Strict .Precategory.Ob =  U 
  Strict .Precategory.Hom x y = Hom (Gen x) (Gen y)
  Strict .Precategory.Hom-set _ _ = Hom-set _ _
  Strict .Precategory.id = id
  Strict .Precategory._∘_ = _∘_
  Strict .Precategory.idr = idr
  Strict .Precategory.idl = idl
  Strict .Precategory.assoc = assoc

We can use the family of objects over to construct an embedding from the strict category into

  To : Functor Strict C
  To .F₀ = Gen
  To .F₁ f = f
  To .F-id = refl
  To .F-∘ _ _ = refl

  To-ff : is-fully-faithful To
  To-ff = id-equiv

Moreover, this embedding is split essentially surjective on objects. To show this, note that we can construct a map from the objects of back into by classifying the constant family that lies over the set of endomorphisms of This yields a map to which we apply the identity morphism.

  reflect : Ob   U 
  reflect x = classify {x = el! (Hom x x)}  _  x) id

Next, we note that we can construct a morphism from any object to it’s it’s reflection in as seen through the generic object. Furthermore, this morphism is cartesian, and thus invertible.

  η* : (x : Ob)  Hom x (Gen (reflect x))
  η* x = classify'  _  x) id

  η*-invertible :  {x}  is-invertible (η* x)
  η*-invertible {x} =
    cartesian→pointwise-iso (classify-cartesian λ _  x) id

This implies that the embedding from our strict category into is split eso, and thus an equivalence of categories.

  To-split-eso : is-split-eso To
  To-split-eso y =
    reflect y , (invertible→iso (η* y) η*-invertible Iso⁻¹)

  eqv : Equivalence Strict C
  eqv .Equivalence.To = To
  eqv .Equivalence.To-equiv =
    ff+split-eso→is-equivalence id-equiv To-split-eso

On to the backwards direction! The key insight here is that we can use the set of objects of the strict category as the base of our generic object, and the forward direction of the equivalence as the displayed portion.

Strict-equiv→Family-generic-object
  :  (Small : Precategory h h)
   is-strict Small
   Equivalence Small C
   Globally-small (Family {h})
Strict-equiv→Family-generic-object Small ob-set eqv = gsmall where
  module Small = Precategory Small
  open Equivalence eqv
  open Globally-small
  open Generic-object

  gsmall : Globally-small Family
  gsmall .U = el Small.Ob ob-set
  gsmall .Gen = To .F₀

Classifying objects in the family fibration is just a matter of chasing the equivalence around.

  gsmall .has-generic-ob .classify f x = From .F₀ (f x)
  gsmall .has-generic-ob .classify' f x = counit⁻¹ .η (f x)
  gsmall .has-generic-ob .classify-cartesian f .universal m h' x =
    counit .η (f (m x))  h' x
  gsmall .has-generic-ob .classify-cartesian f .commutes m h' =
    funext λ _  cancell (is-invertible.invr (counit-iso _))
  gsmall .has-generic-ob .classify-cartesian f .unique {m = m} {h' = h'} m' p =
    funext λ x 
      m' x                                                 ≡⟨ introl (is-invertible.invl (counit-iso _)) 
      (counit .η (f (m x))  counit⁻¹ .η (f (m x)))  m' x ≡⟨ pullr (p $ₚ x) 
      counit .η (f (m x))  h' x 

If is itself strict, then the set of objects of forms a generic object.

Strict→Family-generic-object
  : (ob-set : is-strict C)
   Generic-object (Family {o}) {el Ob ob-set}  x  x)
Strict→Family-generic-object ob-set = gobj where
  open Generic-object

  gobj : Generic-object Family  x  x)
  gobj .classify f = f
  gobj .classify' _ _ = id
  gobj .classify-cartesian _ .universal _ h' = h'
  gobj .classify-cartesian _ .commutes _ h' = funext λ _  idl _
  gobj .classify-cartesian _ .unique m' p = funext λ x 
    sym (idl _)  p # x

Skeletal generic objects🔗

Let be a strict category, and recall that the set of objects of forms a generic object. This generic object is a skeletal generic object if and only if is a skeletal precategory.

Family-skeletal-generic-object→Skeletal
  : (ob-set : is-strict C)
   is-skeletal-generic-object Family (Strict→Family-generic-object ob-set)
   is-skeletal C
Family-skeletal-generic-object→Skeletal ob-set skel-gobj = skel where

We shall prove the forward direction first. Let be an isomorphism. From this, we can construct a pair of set maps that pick out the source and target of the isomorphism. We then construct a pair of cartesian morphisms that lie over and resp.

  src :  {a b}  a  b  Ob
  src {a = a} _ = a

  tgt :  {a b}  a  b  Ob
  tgt {b = b} _ = b

  h₀ :  {a b}  a  b  Hom a a
  h₀ _ = id

  h₁ :  {a b}  a  b  Hom a b
  h₁ f = f .to

  h₀-cartesian
    :  {a b}  (f : a  b)
     is-cartesian Family {a = el! (Lift _ )}  _  src f)  _  h₀ f)
  h₀-cartesian f = pointwise-iso→cartesian λ _  id-invertible

  h₁-cartesian
    :  {a b}  (f : a  b)
     is-cartesian Family {a = el! (Lift _ )}  _  tgt f)  _  h₁ f)
  h₁-cartesian f = pointwise-iso→cartesian λ _  iso→invertible f

Since is a skeletal generic object, any 2 cartesian morphisms into must have the same underlying map. Therefore, and must be equal, which in turn implies that

  skel : is-skeletal C
  skel = path-from-has-iso→is-skeletal C λ f 
    ∥-∥-rec (ob-set _ _)
       f 
        skel-gobj (h₀-cartesian f) $ₚ _
         sym (skel-gobj (h₁-cartesian f) $ₚ _))
      f

The reverse direction is much simpler. Let be a family of objects, and be a cartesian map lying above some cartesian map. Recall that every cartesian map in the family fibration is a pointwise isomorphism. However, is skeletal, so each of these isomorphisms must be an automorphism, yielding a path between the classifying map of the generic object and

Skeletal→Family-skeletal-generic-object
  : (skel : is-skeletal C)
   is-skeletal-generic-object Family
      (Strict→Family-generic-object (skeletal→strict C skel))
Skeletal→Family-skeletal-generic-object skel {f' = f'} cart =
  funext λ x 
    skel .to-path $
      inc (invertible→iso (f' x) (cartesian→pointwise-iso cart x) Iso⁻¹)

Gaunt generic objects🔗

Let be a strict category, and again recall that the set of objects of forms a generic object. This generic object is a gaunt generic object if and only if is a gaunt precategory.

We begin with the forward direction. Recall that a category is gaunt if it is skeletal and all automorphisms are trivial. Gaunt generic objects are always skeletal, which in turn implies that is skeletal.

Family-gaunt-generic-object→Gaunt
  : (ob-set : is-strict C)
   is-gaunt-generic-object Family (Strict→Family-generic-object ob-set)
   is-gaunt C
Family-gaunt-generic-object→Gaunt ob-set gaunt-gobj =
  skeletal+trivial-automorphisms→gaunt skel trivial-automorphism where
  open is-gaunt-generic-object gaunt-gobj

  skel : is-skeletal C
  skel =
    Family-skeletal-generic-object→Skeletal ob-set
      (gaunt-generic-object→skeletal-generic-object Family gaunt-gobj)

To see that all automorphisms of are trivial, note that any automorphism induces a cartesian morphism Furthermore, this cartesian morphism must be unique, as is a gaunt generic object. However, also yields a cartesian morphism so

  trivial-automorphism :  {x}  (f : x  x)  f  id-iso
  trivial-automorphism {x} f =
    ≅-pathp refl refl (is-set→cast-pathp  x'  Hom x x') ob-set p) where

   f-to-cart : is-cartesian Family {a = el! (Lift _ )}  _  x)  _  f .to)
   f-to-cart = pointwise-iso→cartesian  _  iso→invertible f)

   p : PathP  i  Hom x (classify-unique f-to-cart i _)) (f .to) id
   p i = classify-unique' f-to-cart i _

To show the reverse direction, we can appeal to the fact that isomorphisms form an identity system to contract down cartesian maps to the identity morphism.

Gaunt→Family-gaunt-generic-object
  : (gaunt : is-gaunt C)
   is-gaunt-generic-object Family
      (Strict→Family-generic-object (is-gaunt.has-strict gaunt))
Gaunt→Family-gaunt-generic-object gaunt = gaunt-gobj where
  open is-gaunt gaunt hiding (from)
  open is-gaunt-generic-object

  Ob-set : Set o
  Ob-set = el Ob has-strict

  gaunt-gobj : is-gaunt-generic-object Family _
  gaunt-gobj .classify-unique cart =
    funext λ x  has-category .to-path $
      invertible→iso _ (cartesian→pointwise-iso cart x) Iso⁻¹
  gaunt-gobj .classify-unique' {x' = x'} {u = u} {f' = f'} cart =
    funextP λ x 
      IdsJ has-category
         b h  PathP  i  Hom b (has-category .to-path h i)) (h .from) id)
        (is-set→cast-pathp {p = refl}  x'  Hom (u x) x') has-strict refl)
        (invertible→iso _ (cartesian→pointwise-iso cart x) Iso⁻¹)