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

import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Reasoning

module Cat.Displayed.Univalence
{o β o' β'}
{B : Precategory o β}
(E : Displayed B o' β')
where

private
module B = Cat.Reasoning B
module β«E = Cat.Reasoning (β« E)
open Cat.Displayed.Morphism E
open Displayed E
open Total-hom


# Univalence for displayed categoriesπ

We provide equivalent characterisations of univalence for categories which are displayed over a univalent category

We say a displayed category is univalent when, for any in and object over the space of βobjects over isomorphic to over β 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 to be univalent, if 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 in is equivalent to the type

consisting of an isomorphism in the base category and an isomorphism 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 is vertical, i.e.Β  and 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 s.t. over 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 , 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 is an arbitrary isomorphism (in it suffices to consider the case where and is the identity. Here, is the isomorphism of first components coming from the isomorphism in

  is-category-total : is-category (β« E)
is-category-total = total-cat where
wrapper
: β {x y} (p : x B.β y) (A : Ob[ x ]) (B : Ob[ y ]) (f : A β[ p ] B)
β Path (Ξ£ _ ((x , A) β«E.β_))
((x , A) , β«E.id-iso)
((y , B) , piece-together p f)
wrapper p A =
Univalent.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

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-fibrewise
: 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-fibrewise'
: 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[ B.id-iso ]
(i .F.to)
(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)