module Cat.Displayed.Univalence
  {o β„“ oβ€² β„“β€²}
  {B : Precategory o β„“}
  (E : Displayed B oβ€² β„“β€²)

Univalence for displayed categoriesπŸ”—

We provide equivalent characterisations of univalence for categories E\mathcal{E} which are displayed over a univalent category B\mathcal{B}.

We say a displayed category E\mathcal{E} is univalent when, for any f:xβ‰…yf : x \cong y in B\mathcal{B} and object AA over xx, the space of β€œobjects over yy isomorphic to AA over ff” is a proposition.

is-category-displayed : Type _
is-category-displayed =
  βˆ€ {x y} (f : x B.β‰… y) (A : Ob[ x ]) β†’ is-prop (Ξ£[ B ∈ Ob[ y ] ] (A β‰…[ f ] B))

This condition is sufficient for the total category ∫E\int E to be univalent, if B\mathcal{B} is, too. The proof of this is a bit nasty, so we’ll break it down into parts. Initially, observe that the type of isomorphisms (x,A)β‰…(y,B)(x, A) \cong (y, B) in ∫E\int E is equivalent to the type

βˆ‘p:xβ‰…y(Aβ‰…pB), \sum_{p : x \cong y} (A \cong_p B),

consisting of an isomorphism pp in the base category and an isomorphism ff over it.

module _ (base-c : is-category B) (disp-c : is-category-displayed) where
      : βˆ€ {x y} (p : x B.β‰… y) {A : Ob[ x ]} {B : Ob[ y ]} (f : A β‰…[ p ] B)
      β†’ (x , A) ∫E.β‰… (y , B)
    piece-together p f =
      ∫E.make-iso (total-hom (p (f .toβ€²)) (total-hom (p .B.from) (f .fromβ€²))
        (total-hom-path E (p .B.invl) (f .invlβ€²))
        (total-hom-path E (p .B.invr) (f .invrβ€²))

We first tackle the case where f:Aβ‰…Bf : A \cong B is vertical, i.e.Β AA and BB are in the same fibre category. But then, observe that our displayed univalence condition, when applied to the identity morphism, gives us exactly an identification p:A≑Bp : A \equiv B s.t. over pp, ff looks like the identity (vertical) isomorphism.

      : βˆ€ {x} {A : Ob[ x ]} (B : Ob[ x ]) (f : A ≅↓ B)
      β†’ Path (Ξ£ _ ((x , A) ∫E.β‰…_)) ((x , A) , ∫
          ((x , B) , piece-together f)
    contract-vertical-iso {x} {A} B f =
      Ξ£-pathp (Ξ» i β†’ x , pair i .fst)
        (∫E.β‰…-pathp refl _ (total-hom-pathp E _ _ refl Ξ» i β†’ pair i .snd .toβ€²))
        pair = disp-c A
          (A , id-iso↓)
          (B , f)

We can now use isomorphism induction in the base category to reduce the general case to contract-vertical-iso above. To wit: If p:xβ‰…yp : x \cong y is an arbitrary isomorphism (in B\mathcal{B}), it suffices to consider the case where y=xy = x and pp is the identity. Here, pp is the isomorphism of first components coming from the isomorphism in ∫E\int E.

  is-category-total : is-category (∫ E)
  is-category-total = total-cat where
      : βˆ€ {x y} (p : x B.β‰… y) (A : Ob[ x ]) (B : Ob[ y ]) (f : A β‰…[ p ] B)
      β†’ Path (Ξ£ _ ((x , A) ∫E.β‰…_))
        ((x , A) , ∫
        ((y , B) , piece-together p f)
    wrapper p A =
      Univalent.J-iso base-c
        (Ξ» y p β†’ (B : Ob[ y ]) (f : A β‰…[ p ] B)
               β†’ ((_ , A) , ∫ ≑ (((y , B) , piece-together p f)))

    total-cat : is-category (∫ E)
    total-cat .to-path p = ap fst $
        wrapper (total-iso→iso E p) _ _ (total-iso→iso[] E p)
    total-cat .to-path-over p = ap snd $
        wrapper (total-iso→iso E p) _ _ (total-iso→iso[] E p)

Fibrewise univalent categoriesπŸ”—

Using the same trick as above, we can show that a displayed category is univalent everywhere if, and only if, it is univalent when restricted to vertical isomorphisms:

  : is-category B
  β†’ (βˆ€ {x} (A : Ob[ x ]) β†’ is-prop (Ξ£[ B ∈ Ob[ x ] ] (A ≅↓ B)))
  β†’ is-category-displayed
is-category-fibrewise base-c wit f A =
  Univalent.J-iso base-c (Ξ» y p β†’ is-prop (Ξ£[ B ∈ Ob[ y ] ] (A β‰…[ p ] B))) (wit A) f

Consequently, it suffices for each fibre category to be univalent, since a vertical isomorphism is no more than an isomorphism in a particular fibre category.

  : is-category B
  β†’ (βˆ€ x β†’ is-category (Fibre E x))
  β†’ is-category-displayed
is-category-fibrewiseβ€² b wit = is-category-fibrewise b witβ€² where
  witβ€² : βˆ€ {x} (A : Ob[ x ]) β†’ is-prop (Ξ£[ B ∈ Ob[ x ] ] (A ≅↓ B))
  witβ€² {x} A =
    is-contr→is-prop $ retract→is-contr
      (Ξ» (x , i) β†’ x , make-iso[ ]
        (i .F.from)
        (to-pathp (i .F.invl))
        (to-pathp (i .F.invr)))
      (Ξ» (x , i) β†’ x , F.make-iso (i .toβ€²) (i .fromβ€²)
        (from-pathp (i .invlβ€²)) (from-pathp (i .invrβ€²)))
      (Ξ» (x , i) β†’ Ξ£-pathp refl (β‰…[]-path refl))
      (is-contr-Ξ£R (wit x))
    where module F = Cat.Reasoning (Fibre E x)