open import Cat.Displayed.Fibre
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Univalent
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

module Cat.Displayed.Univalence
  {o ℓ o′ ℓ′}
  {B : Precategory o ℓ}
  (E : Displayed B o′ ℓ′)
  where

Univalence for displayed categories🔗

We provide equivalent characterisations of univalence for categories E\ca{E} which are displayed over a univalent category B\ca{B}. The first thing we define is a type of displayed isomorphisms. If we have an isomorphism f:x≅yf : x \cong y in B\ca{B}, we may define a type of isomorphisms over ff to consist of maps g:A→fBg : A \to_f B and g−1:B→f−1Ag^{-1} : B \to_{f^{-1}} A which are inverses.

record _≅[_]_ {x y : B.Ob} (A : Ob[ x ]) (f : x B.≅ y) (B : Ob[ y ]) : Type ℓ′ where
  field
    to′   : Hom[ B.to f ] A B
    from′ : Hom[ B.from f ] B A
    invr  : PathP (λ i → Hom[ B.invr f i ] A A) (from′ ∘′ to′) id′
    invl  : PathP (λ i → Hom[ B.invl f i ] B B) (to′ ∘′ from′) id′

open _≅[_]_

Since isomorphisms over the identity map will be of particular importance, we also define their own type: they are the vertical isomorphisms.

_≅↓_ : {x : B.Ob} (A B : Ob[ x ]) → Type ℓ′
_≅↓_ = _≅[ B.id-iso ]_

We say a displayed category E\ca{E} is univalent when, for any f:x≅yf : x \cong y in B\ca{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\ca{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
  private
    piece-together
      : ∀ {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 .B.to) (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.

    contract-vertical-iso
      : ∀ {x} {A : Ob[ x ]} (B : Ob[ x ]) (f : A ≅↓ B)
      → Path (Σ _ ((x , A) ∫E.≅_)) ((x , A) , ∫E.id-iso)
          ((x , B) , piece-together B.id-iso 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′))
      where
        pair = disp-c B.id-iso A
          (A , record { to′ = id′; from′ = id′; invr = idl′ id′; invl = idl′ id′ })
          (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\ca{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 A .centre = A , ∫E.id-iso
  is-category-total A .paths (B , isom) = wrapper _ _ _ _ where
    wrapper
      : ∀ {x y} (p : x B.≅ y) (A : Ob[ x ]) (B : Ob[ y ]) (f : A ≅[ p ] B)
      → Path (Σ _ ((x , A) ∫E.≅_)) _ _
    wrapper p A =
      J-iso _ base-c
        (λ y p → (B : Ob[ y ]) (f : A ≅[ p ] B)
               → ((_ , A) , ∫E.id-iso) ≡ (((y , B) , piece-together p f)))
        contract-vertical-iso
        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-fibrewise
  : (∀ {x} (A : Ob[ x ]) → is-prop (Σ[ B ∈ Ob[ x ] ] (A ≅↓ B)))
  → is-category B
  → is-category-displayed
is-category-fibrewise wit base-c f A =
  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-fibrewise′
  : (∀ x → is-category (Fibre E x))
  → is-category B
  → is-category-displayed
is-category-fibrewise′ wit b = is-category-fibrewise wit′ b 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 , record
        { to′   = i .F.to
        ; from′ = i .F.from
        ; invr  = to-pathp (i .F.invr)
        ; invl  = to-pathp (i .F.invl)
        })
      (λ (x , i) → x , F.make-iso (i .to′) (i .from′)
        (from-pathp (i .invl)) (from-pathp (i .invr)))
      (λ (x , i) → Σ-pathp refl (≅[]-path refl refl))
      (wit x A)
    where module F = Cat.Reasoning (Fibre E x)