module Cat.Displayed.Univalence.Reasoning
  {o β„“ o' β„“'} {B : Precategory o β„“} (E : Displayed B o' β„“')
  where

Remarks about displayed univalenceπŸ”—

Note that, over a univalent base, univalence of displayed categories is equivalent to fibrewise univalence; Over a precategorical base, displayed univalence is a stronger condition, but it still implies that each fibre is univalent. Moreover, since isomorphisms in fibres are equivalent to vertical isomorphisms, if is a displayed univalent category, then vertical isomorphism is an identity system on each type of objects-over.

≅↓-identity-system
  : βˆ€ {x} β†’ is-category-displayed
  β†’ is-identity-system (_≅↓_ {x = x}) (Ξ» _ β†’ id-iso↓)
≅↓-identity-system e-cat .to-path {a} {b} i =
  ap fst $ e-cat B.id-iso a (a , id-iso↓) (b , i)
≅↓-identity-system e-cat .to-path-over {a} {b} i =
  ap snd $ e-cat B.id-iso a (a , id-iso↓) (b , i)

Therefore, we have an equivalence between paths of objects-over the same base object and vertical isomorphisms, regardless of whether the base category is univalent or not. Much like in the non-displayed case, this equivalence lets us compute transports of morphisms-over (along their domain and codomain, rather than over their base morphism) in terms of pre/post-composition with a vertical isomorphism.

path→vertical-iso
  : βˆ€ {x} {x₁ xβ‚‚ : Ob[ x ]} β†’ x₁ ≑ xβ‚‚ β†’ x₁ ≅↓ xβ‚‚
pathβ†’vertical-iso {x₁ = x₁} p = transport (Ξ» i β†’ x₁ ≅↓ p i) id-iso↓

vertical-iso→path
  : βˆ€ {x} {x₁ xβ‚‚ : Ob[ x ]}
  β†’ is-category-displayed
  β†’ x₁ ≅↓ xβ‚‚ β†’ x₁ ≑ xβ‚‚
vertical-isoβ†’path e = ≅↓-identity-system e .to-path

The transport and dependent path lemmas are straightforward generalisations of their non-displayed counterparts. Note that while we only need to talk about vertical isomorphisms, the proofs work over an arbitrary morphism in the base. They are also generalised over an arbitrary identification between e.g.Β  in the base.

abstract
  Hom[]-transport
    : (Ξ± : f ≑ B.id B.∘ f B.∘ B.id) (p : x₁ ≑ xβ‚‚) (q : y₁ ≑ yβ‚‚)
    β†’ (f' : Hom[ f ] x₁ y₁)
    β†’ transport (Ξ» i β†’ Hom[ f ] (p i) (q i)) f' ≑[ Ξ± ]
      pathβ†’vertical-iso q .to' ∘' f' ∘' pathβ†’vertical-iso p .from'

  Hom[]-pathp-iso
    : (e-cat : is-category-displayed)
    β†’ (Ξ± : B.id B.∘ f B.∘ B.id ≑ f)
    β†’ (p : x₁ ≅↓ xβ‚‚) (q : y₁ ≅↓ yβ‚‚) (f' : Hom[ f ] x₁ y₁) (g' : Hom[ f ] xβ‚‚ yβ‚‚)
    β†’ q .to' ∘' f' ∘' p .from' ≑[ Ξ± ] g'
    → PathP (λ i → Hom[ f ] (vertical-iso→path e-cat p i)
                            (vertical-iso→path e-cat q i))
        f' g'

  Hom[]-pathp-refll-iso
    : (e-cat : is-category-displayed) (Ξ± : f B.∘ B.id ≑ f)
    β†’ (p : x₁ ≅↓ xβ‚‚) (f' : Hom[ f ] x₁ y') (g' : Hom[ f ] xβ‚‚ y')
    β†’ f' ∘' p .from' ≑[ Ξ± ] g'
    → PathP (λ i → Hom[ f ] (vertical-iso→path e-cat p i) y') f' g'
These lemmas all have scary type signatures and nightmare proofs. Therefore, they’re hidden away down here.
  Hom[]-transport {f = f} {x₁ = x₁} {y₁ = y₁} Ξ± p q f' =
    Jβ‚‚ (Ξ» xβ‚‚ yβ‚‚ p q β†’ transport (Ξ» i β†’ Hom[ f ] (p i) (q i)) f'
               ≑[ Ξ± ] pathβ†’vertical-iso q .to' ∘' f' ∘' pathβ†’vertical-iso p .from')
      (to-pathp⁻ (sym
        (ap hom[] (from-pathp⁻ (eliml' refl (transport-refl _) {q = B.idl _})
                ·· ap hom[] (from-pathp⁻ (elimr' refl (transport-refl _) {q = B.idr f}))
                Β·Β· hom[]-βˆ™ _ _)
        Β·Β· hom[]-βˆ™ _ _
        Β·Β· reindex _ _)))
      p q

  Hom[]-pathp-refll-iso e-cat Ξ± p f' g' Ξ² = to-pathp $
       from-pathp⁻ (Hom[]-transport (sym (B.idl _ βˆ™ Ξ±)) (vertical-isoβ†’path e-cat p) refl f')
    Β·Β· ap hom[] (
        apβ‚‚ (Ξ» a b β†’ a ∘' f' ∘' b) (transport-refl _)
          (from-pathp (Ξ» i β†’ ≅↓-identity-system e-cat .to-path-over p i .from'))
        βˆ™ from-pathp⁻ (idl' (f' ∘' p .from')))
    Β·Β· (hom[]-βˆ™ _ _ Β·Β· reindex _ _ Β·Β· from-pathp Ξ²)

  Hom[]-pathp-iso e-cat Ξ± p q f' g' Ξ² = to-pathp $
       from-pathp⁻ (Hom[]-transport (sym Ξ±) (vertical-isoβ†’path e-cat p) (vertical-isoβ†’path e-cat q) f')
    Β·Β· ap hom[] (apβ‚‚ (Ξ» a b β†’ a ∘' f' ∘' b)
        (from-pathp (Ξ» i β†’ ≅↓-identity-system e-cat .to-path-over q i .to'))
        (from-pathp (Ξ» i β†’ ≅↓-identity-system e-cat .to-path-over p i .from')))
    Β·Β· from-pathp Ξ²