module Cat.Functor.Univalence  where

Our previous results about paths between functors, componentwise invertibility, and general reasoning in univalent categories assemble into the following very straightforward proof that [C,D][\mathcal{C},\mathcal{D}] is univalent whenever D\mathcal{D} is.

Functor-is-category : is-category D → is-category Cat[ C , D ]
Functor-is-category {D = D} {C = C} d-cat .to-path {F} {G} im =
  Functor-path (λ x → d-cat .to-path (isoⁿ→iso im x)) coh
  where
    open Univalent d-cat using (Hom-pathp-iso ; pulll ; cancelr)
    abstract
      coh : ∀ {x y : C .Ob} (f : C .Hom x y)
          → PathP (λ i → D .Hom (d-cat .to-path (isoⁿ→iso im x) i) (d-cat .to-path (isoⁿ→iso im y) i))
              (F .F₁ f) (G .F₁ f)
      coh f = Hom-pathp-iso ( pulll (Isoⁿ.to im .is-natural _ _ _)
                            ∙ cancelr (Isoⁿ.invl im ηₚ _))
Functor-is-category {D = D} d-cat .to-path-over p =
  ≅ⁿ-pathp _ _ (λ x → Hom-pathp-reflr-iso (Precategory.idr D (Isoⁿ.to p .η x)))
  where open Univalent d-cat