open import Cat.Displayed.GenericObject
open import Cat.Displayed.Cartesian
open import Cat.Functor.Equivalence
open import Cat.Functor.Properties
open import Cat.Instances.Discrete
open import Cat.Instances.Functor
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Skeletal
open import Cat.Prelude
open import Cat.Strict
open import Cat.Gaunt

import Cat.Reasoning

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

open Cat.Reasoning C
open Displayed
open Functor
open _=>_


# The family fibration🔗

We can canonically treat any Precategory $\mathcal{C}$ as being displayed over Sets, regardless of the size of the object- and Hom-spaces of $\mathcal{C}$.

In a neutral presentation of displayed category theory, the collection of objects over $S$ would given by the space of functors $[\mathrm{Disc}(S),C]$, regarding $S$ as a discrete category. This is essentially an $S$-indexed family of objects of $C$, 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 $S$ are precisely the families $S \to \mathrm{Ob}_\mathcal{C}$.

Family : ∀ {ℓ} → Displayed (Sets ℓ) _ _
Family .Ob[_] S = ∣ S ∣ → Ob


The set of maps over a function $f : A \to B$ (in $\mathbf{Sets}$) is the set of families of morphisms $F(x) \to G(fx)$. 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 $f : x \to y$ and a family $Y$ over $y$, we must define a family $X$ over $x$ and give a universal family of functions $X(a) \to Y(f(a))$. But we may simply take $X(a) := Y(f(a))$, 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 $\mathcal{C}$ 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₁ 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 = Nat-path λ x → refl
Families→functors .F-∘ f g =
ap (Families→functors .F₁) (transport-refl _) ∙ Nat-path λ x → refl

Families→functors-is-ff : is-fully-faithful Families→functors
Families→functors-is-ff = is-iso→is-equiv
(iso η (λ x → Nat-path λ _ → refl) λ 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 $\mathcal{C}$ has a generic object if and only if $\mathcal{C}$ 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 (Precategory.Ob 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 $\mathcal{C}$ with the base component of the generic object $U$, which is a small set. The displayed component of the generic object gives us a family of objects over $U$, 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 $U$ to construct an embedding from the strict category into $\mathcal{C}$.

  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 $\mathcal{C}$ back into $U$ by classifying the constant family $_ \mapsto x$ that lies over the set of endomorphisms of $x$. This yields a map $\mathcal{C}(x,x) \to U$, 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 $x : \mathcal{C}$ to it’s it’s reflection in $U$, 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 $\mathcal{C}$ 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 $\mathcal{C}$ is itself strict, then the set of objects of $\mathcal{C}$ 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 $\mathcal{C}$ be a strict category, and recall that the set of objects of $\mathcal{C}$ forms a generic object. This generic object is a skeletal generic object if and only if $\mathcal{C}$ 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 $f : a \cong b$ be an isomorphism. From this, we can construct a pair of set maps $src, tgt : \top \to C_0$ that pick out the source and target of the isomorphism. We then construct a pair of cartesian morphisms $h_0, h_1 : \{ a \} \to Ob$ that lie over $src$ and $tgt$, 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 $Ob$ is a skeletal generic object, any 2 cartesian morphisms into $Ob$ must have the same underlying map. Therefore, $src$ and $tgt$ must be equal, which in turn implies that $a = b$.

  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 $X_i$ be a family of objects, and $f'_i : X_i \to Ob$ be a cartesian map lying above some $u : I \to Ob$. cartesian map. Recall that every cartesian map in the family fibration is a pointwise isomorphism. However, $\mathcal{C}$ is skeletal, so each of these isomorphisms must be an automorphism, yielding a path between the classifying map of the generic object and $u$.

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 $\mathcal{C}$ be a strict category, and again recall that the set of objects of $\mathcal{C}$ forms a generic object. This generic object is a gaunt generic object if and only if $\mathcal{C}$ 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 $\mathcal{C}$ 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 $\mathcal{C}$ are trivial, note that any automorphism $f : x \cong x$ induces a cartesian morphism $\{ x \} \to Ob$. Furthermore, this cartesian morphism must be unique, as $Ob$ is a gaunt generic object. However, $id$ also yields a cartesian morphism $\{ x \} \to Ob$, so $f = id$.  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⁻¹)