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 is univalent whenever 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
    open Univalent d-cat using (Hom-pathp-iso ; pulll ; cancelr)
      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