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 C\mathcal{C} as being displayed over Sets, regardless of the size of the object- and Hom-spaces of C\mathcal{C}.

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

Family : βˆ€ {β„“} β†’ Displayed (Sets β„“) _ _
Family .Ob[_] S = ∣ S ∣ β†’ Ob

The set of maps over a function f:A→Bf : A \to B (in Sets\sets) is the set of families of morphisms F(x)→G(fx)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→yf : x \to y and a family YY over yy, we must define a family XX over xx and give a universal family of functions X(a)→Y(f(a))X(a) \to Y(f(a)). But we may simply take X(a):=Y(f(a))X(a) := Y(f(a)), and family is constantly the identity map.

open Cartesian-fibration
open Cartesian-lift
open Cartesian

Family-is-cartesian : βˆ€ {β„“} β†’ Cartesian-fibration (Family {β„“ = β„“})
Family-is-cartesian = iscart where
  cart : βˆ€ {x y : Set _} (f : ∣ x ∣ β†’ ∣ y ∣)
           (yβ€² : ∣ y ∣ β†’ Ob)
       β†’ 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β€²

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 C\ca{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₀ = 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 = C} (elimr refl βˆ™ ap to (Univalent.isoβ†’pathβ†’iso isc _))