open import Cat.Displayed.Cartesian open import Cat.Functor.Equivalence open import Cat.Instances.Discrete open import Cat.Instances.Functor open import Cat.Displayed.Fibre open import Cat.Displayed.Base open import Cat.Functor.Base open import Cat.Univalent open import Cat.Prelude import Cat.Reasoning 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 given by the space of functors , regarding as a discrete category. This is essentially an -indexed 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 factorization, and then applying the isomorphism equations to show that weβve actually constructed the unique factorization.
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 factorization 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 = 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 _))