(** * Classification of path spaces of functors *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Basics HoTT.Types HoTT.Tactics.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope path_scope.
Local Open Scope morphism_scope.
Local Open Scope functor_scope.

Section path_functor.
  Context `{Funext}.

  Variables C D : PreCategory.



  Local Notation functor_sig_T :=
    { OO : C -> D
    | { MO : forall s d, morphism C s d -> morphism D (OO s) (OO d)
      | { FCO : forall s d d' (m1 : morphism C s d) (m2 : morphism C d d'),
                  MO _ _ (m2 o m1) = MO d d' m2 o MO s d m1
        | forall x,
            MO x x (identity x) = identity (OO x) } } }
      (only parsing).

  (** ** Equivalence between the record and sigma-type versions of a functor *)
  Lemma equiv_sig_functor
  : functor_sig_T <~> Functor C D.
H: Funext
C, D: PreCategory
{OO : C -> D &
{MO
: forall s d : C,
  morphism C s d -> morphism D (OO s) (OO d) &
{_
: forall (s d d' : C) (m1 : morphism C s d)
  (m2 : morphism C d d'),
  MO s d' (m2 o m1) = MO d d' m2 o MO s d m1 &
forall x : C, MO x x 1 = 1}}} <~> Functor C D
  Proof.
H: Funext
C, D: PreCategory
{OO : C -> D &
{MO
: forall s d : C,
  morphism C s d -> morphism D (OO s) (OO d) &
{_
: forall (s d d' : C) (m1 : morphism C s d)
  (m2 : morphism C d d'),
  MO s d' (m2 o m1) = MO d d' m2 o MO s d m1 &
forall x : C, MO x x 1 = 1}}} <~> Functor C D
    issig.
  Defined.

  (** We could leave it at that and be done with it, but we want a more convenient form for actually constructing paths between functors.  For this, we write a trimmed down version of something equivalent to the type of paths between functors. *)

  Local Notation path_functor'_T F G
    := { HO : object_of F = object_of G
       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
                   HO
                   (morphism_of F)
         = morphism_of G }
         (only parsing).

  (** We could just go prove that the path space of [functor_sig_T] is equivalent to [path_functor'_T], but unification is far too slow to do this effectively.  So instead we explicitly classify [path_functor'_T], and provide an equivalence between it and the path space of [Functor C D]. *)

  (**
<<
  Definition equiv_path_functor_uncurried_sig (F G : Functor C D)
  : path_functor'_T F G <~> (@equiv_inv _ _ _ equiv_sig_functor F
                              = @equiv_inv _ _ _ equiv_sig_functor G).
  Proof.
    etransitivity; [ | by apply equiv_path_sigma ].
    eapply @equiv_functor_sigma.
    repeat match goal with
             | [ |- context[(@equiv_inv ?A ?B ?f ?H ?F).1] ]
               => change ((@equiv_inv A B f H F).1) with (object_of F)
           end.
    Time exact (isequiv_idmap (object_of F = object_of G)). (* 13.411 secs *)
  Abort.
>>
   *)

  (** ** Classify sufficient conditions to prove functors equal *)
  Definition path_functor_uncurried (F G : Functor C D) : path_functor'_T F G -> F = G.
H: Funext
C, D: PreCategory
F, G: Functor C D
{HO : F = G &
transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d)) HO
  (morphism_of F) = morphism_of G} -> F = G
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
{HO : F = G &
transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d)) HO
  (morphism_of F) = morphism_of G} -> F = G
    intros [? ?].
H: Funext
C, D: PreCategory
F, G: Functor C D
proj1: F = G
proj2: transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d))
  proj1 (morphism_of F) = 
morphism_of G
F = G
    destruct F, G; simpl in *.
H: Funext
C, D: PreCategory
object_of: C -> D
morphism_of: forall s d : C,
morphism C s d ->
morphism D (object_of s) (object_of d)
composition_of: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of s d' (m2 o m1) =
morphism_of d d' m2
o morphism_of s d m1
identity_of: forall x : C, morphism_of x x 1 = 1
object_of0: C -> D
morphism_of0: forall s d : C,
morphism C s d ->
morphism D (object_of0 s)
  (object_of0 d)
composition_of0: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of0 s d' (m2 o m1) =
morphism_of0 d d' m2
o morphism_of0 s d m1
identity_of0: forall x : C, morphism_of0 x x 1 = 1
proj1: object_of = object_of0
proj2: transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d))
  proj1 morphism_of = morphism_of0
{|
  object_of := object_of;
  morphism_of := morphism_of;
  composition_of := composition_of;
  identity_of := identity_of
|} =
{|
  object_of := object_of0;
  morphism_of := morphism_of0;
  composition_of := composition_of0;
  identity_of := identity_of0
|}
    path_induction; simpl.
H: Funext
C, D: PreCategory
object_of: C -> D
morphism_of: forall s d : C,
morphism C s d ->
morphism D (object_of s) (object_of d)
composition_of: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of s d' (m2 o m1) =
morphism_of d d' m2
o morphism_of s d m1
identity_of: forall x : C, morphism_of x x 1 = 1
composition_of0: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
transport
  (fun GO : C -> D =>
   forall s0 d0 : C,
   morphism C s0 d0 ->
   morphism D (GO s0) (GO d0)) 1
  morphism_of s d' (m2 o m1) =
transport
  (fun GO : C -> D =>
   forall s0 d0 : C,
   morphism C s0 d0 ->
   morphism D (GO s0) (GO d0)) 1
  morphism_of d d' m2
o transport
    (fun GO : C -> D =>
     forall s0 d0 : C,
     morphism C s0 d0 ->
     morphism D (GO s0) (GO d0)) 1
    morphism_of s d m1
identity_of0: forall x : C,
transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d ->
   morphism D (GO s) (GO d)) 1
  morphism_of x x 1 = 1
{|
  object_of := object_of;
  morphism_of := morphism_of;
  composition_of := composition_of;
  identity_of := identity_of
|} =
{|
  object_of := object_of;
  morphism_of := morphism_of;
  composition_of := composition_of0;
  identity_of := identity_of0
|}
    f_ap;
      eapply @center; abstract exact _.
  Defined.

  (** *** Said proof respects [object_of] *)
  Lemma path_functor_uncurried_fst F G HO HM
  : ap object_of (@path_functor_uncurried F G (HO; HM)) = HO.
H: Funext
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: (fun HO : F = G =>
 transport
   (fun GO : C -> D =>
    forall s d : C,
    morphism C s d -> morphism D (GO s) (GO d))
   HO (morphism_of F) = morphism_of G) HO
ap object_of (path_functor_uncurried F G (HO; HM)) =
HO
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: (fun HO : F = G =>
 transport
   (fun GO : C -> D =>
    forall s d : C,
    morphism C s d -> morphism D (GO s) (GO d))
   HO (morphism_of F) = morphism_of G) HO
ap object_of (path_functor_uncurried F G (HO; HM)) =
HO
    destruct F, G; simpl in *.
H: Funext
C, D: PreCategory
object_of: C -> D
morphism_of: forall s d : C,
morphism C s d ->
morphism D (object_of s) (object_of d)
composition_of: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of s d' (m2 o m1) =
morphism_of d d' m2
o morphism_of s d m1
identity_of: forall x : C, morphism_of x x 1 = 1
object_of0: C -> D
morphism_of0: forall s d : C,
morphism C s d ->
morphism D (object_of0 s)
  (object_of0 d)
composition_of0: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of0 s d' (m2 o m1) =
morphism_of0 d d' m2
o morphism_of0 s d m1
identity_of0: forall x : C, morphism_of0 x x 1 = 1
HO: object_of = object_of0
HM: transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d)) HO
  morphism_of = morphism_of0
ap Core.object_of
  (match
     HM in (_ = a0)
     return
       (forall
        (composition_of0 : forall (s d d' : C)
                           (m1 : morphism C s d)
                           (m2 : morphism C d d'),
                           a0 s d' (m2 o m1) =
                           a0 d d' m2 o a0 s d m1)
        (identity_of0 : forall x : C, a0 x x 1 = 1),
        {|
          object_of := object_of;
          morphism_of := morphism_of;
          composition_of := composition_of;
          identity_of := identity_of
        |} =
        {|
          object_of := object_of0;
          morphism_of := a0;
          composition_of := composition_of0;
          identity_of := identity_of0
        |})
   with
   | 1%path =>
       fun
         (composition_of0 : forall (s d d' : C)
                            (m1 : morphism C s d)
                            (m2 : morphism C d d'),
                            transport
                              (fun GO : C -> D =>
                               forall s0 d0 : C,
                               morphism C s0 d0 ->
                               morphism D (GO s0)
                                 (GO d0)) HO
                              morphism_of s d'
                              (m2 o m1) =
                            transport
                              (fun GO : C -> D =>
                               forall s0 d0 : C,
                               morphism C s0 d0 ->
                               morphism D (GO s0)
                                 (GO d0)) HO
                              morphism_of d d' m2
                            o transport
                                (fun GO : C -> D =>
                                 forall s0 d0 : C,
                                 morphism C s0 d0 ->
                                 morphism D (GO s0)
                                   (GO d0)) HO
                                morphism_of s d m1)
         (identity_of0 : forall x : C,
                         transport
                           (fun GO : C -> D =>
                            forall s d : C,
                            morphism C s d ->
                            morphism D (GO s) (GO d))
                           HO morphism_of x x 1 = 1)
       =>
       paths_rect (C -> D) object_of
         (fun (object_of0 : C -> D)
            (proj1 : object_of = object_of0) =>
          forall
          (composition_of1 : forall (s d d' : C)
                             (m1 : morphism C s d)
                             (m2 : morphism C d d'),
                             transport
                               (fun GO : C -> D =>
                                forall s0 d0 : C,
                                morphism C s0 d0 ->
                                morphism D (GO s0)
                                  (GO d0)) proj1
                               morphism_of s d'
                               (m2 o m1) =
                             transport
                               (fun GO : C -> D =>
                                forall s0 d0 : C,
                                morphism C s0 d0 ->
                                morphism D (GO s0)
                                  (GO d0)) proj1
                               morphism_of d d' m2
                             o transport
                                 (fun GO : C -> D =>
                                  forall s0 d0 : C,
                                  morphism C s0 d0 ->
                                  morphism D (GO s0)
                                    (GO d0)) proj1
                                 morphism_of s d m1)
          (identity_of1 : forall x : C,
                          transport
                            (fun GO : C -> D =>
                             forall s d : C,
                             morphism C s d ->
                             morphism D (GO s) (GO d))
                            proj1 morphism_of x x 1 =
                          1),
          {|
            object_of := object_of;
            morphism_of := morphism_of;
            composition_of := composition_of;
            identity_of := identity_of
          |} =
          {|
            object_of := object_of0;
            morphism_of :=
              transport
                (fun GO : C -> D =>
                 forall s d : C,
                 morphism C s d ->
                 morphism D (GO s) (GO d)) proj1
                morphism_of;
            composition_of := composition_of1;
            identity_of := identity_of1
          |})
         (fun
            (composition_of1 : forall (s d d' : C)
                               (m1 : morphism C s d)
                               (m2 : morphism C d d'),
                               morphism_of s d'
                                 (m2 o m1) =
                               morphism_of d d' m2
                               o morphism_of s d m1)
            (identity_of1 : forall x : C,
                            morphism_of x x 1 = 1) =>
          ap11
            match
              center
                (composition_of = composition_of1) in
              (_ = a)
              return
                (Build_Functor C D object_of
                   morphism_of composition_of =
                 Build_Functor C D object_of
                   morphism_of a)
            with
            | 1 => 1
            end (center (identity_of = identity_of1)))
         object_of0 HO composition_of0 identity_of0
   end composition_of0 identity_of0) = HO
    path_induction_hammer.
  Qed.

  (** *** Said proof respects [idpath] *)
  Lemma path_functor_uncurried_idpath F
  : @path_functor_uncurried F F (idpath; idpath) = idpath.
H: Funext
C, D: PreCategory
F: Functor C D
path_functor_uncurried F F (1%path; 1%path) = 1%path
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
path_functor_uncurried F F (1%path; 1%path) = 1%path
    destruct F; simpl in *.
H: Funext
C, D: PreCategory
object_of: C -> D
morphism_of: forall s d : C,
morphism C s d ->
morphism D (object_of s) (object_of d)
composition_of: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of s d' (m2 o m1) =
morphism_of d d' m2
o morphism_of s d m1
identity_of: forall x : C, morphism_of x x 1 = 1
ap11
  match
    center (composition_of = composition_of) in
    (_ = a)
    return
      (Build_Functor C D object_of morphism_of
         composition_of =
       Build_Functor C D object_of morphism_of a)
  with
  | 1 => 1
  end (center (identity_of = identity_of)) = 1%path
    rewrite !(contr idpath).
H: Funext
C, D: PreCategory
object_of: C -> D
morphism_of: forall s d : C,
morphism C s d ->
morphism D (object_of s) (object_of d)
composition_of: forall (s d d' : C)
(m1 : morphism C s d)
(m2 : morphism C d d'),
morphism_of s d' (m2 o m1) =
morphism_of d d' m2
o morphism_of s d m1
identity_of: forall x : C, morphism_of x x 1 = 1
ap11 1 1 = 1%path
    reflexivity.
  Qed.

  (** ** Equality of functors gives rise to an inhabitant of the path-classifying-type *)
  Definition path_functor_uncurried_inv (F G : Functor C D) : F = G -> path_functor'_T F G
    := fun H'
       => (ap object_of H';
           (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H')%path.

  (** ** Curried version of path classifying lemma *)
  Definition path_functor (F G : Functor C D)
        (HO : object_of F = object_of G)
        (HM : transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d)) HO (morphism_of F) = morphism_of G)
  : F = G
    := path_functor_uncurried F G (HO; HM).

  (** ** Curried version of path classifying lemma, using [forall] in place of equality of functions *)
  Definition path_functor_pointwise (F G : Functor C D)
        (HO : object_of F == object_of G)
        (HM : forall s d m,
                transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
                          (path_forall _ _ HO)
                          (morphism_of F)
                          s d m
                = G _1 m)
  : F = G.
H: Funext
C, D: PreCategory
F, G: Functor C D
HO: F == G
HM: forall (s d : C) (m : morphism C s d),
transport
  (fun GO : C -> D =>
   forall s0 d0 : C,
   morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  (path_forall F G HO) (morphism_of F) s d m =
G _1 m
F = G
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
HO: F == G
HM: forall (s d : C) (m : morphism C s d),
transport
  (fun GO : C -> D =>
   forall s0 d0 : C,
   morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  (path_forall F G HO) (morphism_of F) s d m =
G _1 m
F = G
    refine (path_functor F G (path_forall _ _ HO) _).
H: Funext
C, D: PreCategory
F, G: Functor C D
HO: F == G
HM: forall (s d : C) (m : morphism C s d),
transport
  (fun GO : C -> D =>
   forall s0 d0 : C,
   morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  (path_forall F G HO) (morphism_of F) s d m =
G _1 m
transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d))
  (path_forall F G HO) (morphism_of F) = morphism_of G
    repeat (apply path_forall; intro); apply HM.
  Defined.

  (** ** Classify equality of functors up to equivalence *)
  Global Instance isequiv_path_functor_uncurried (F G : Functor C D)
  : IsEquiv (@path_functor_uncurried F G).
H: Funext
C, D: PreCategory
F, G: Functor C D
IsEquiv (path_functor_uncurried F G)
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
IsEquiv (path_functor_uncurried F G)
    apply (isequiv_adjointify (@path_functor_uncurried F G)
                              (@path_functor_uncurried_inv F G)).
H: Funext
C, D: PreCategory
F, G: Functor C D
(fun x : F = G =>
 path_functor_uncurried F G
   (path_functor_uncurried_inv x)) == idmap
H: Funext
C, D: PreCategory
F, G: Functor C D
(fun
   x : {HO : F = G &
       transport
         (fun GO : C -> D =>
          forall s d : C,
          morphism C s d -> morphism D (GO s) (GO d))
         HO (morphism_of F) = morphism_of G} =>
 path_functor_uncurried_inv
   (path_functor_uncurried F G x)) == idmap
    -
H: Funext
C, D: PreCategory
F, G: Functor C D
(fun x : F = G =>
 path_functor_uncurried F G
   (path_functor_uncurried_inv x)) == idmap hnf.
H: Funext
C, D: PreCategory
F, G: Functor C D
forall x : F = G,
path_functor_uncurried F G
  (path_functor_uncurried_inv x) = x
      intros [].
H: Funext
C, D: PreCategory
F, G: Functor C D
path_functor_uncurried F F
  (path_functor_uncurried_inv 1) = 1%path
      apply path_functor_uncurried_idpath.
    -
H: Funext
C, D: PreCategory
F, G: Functor C D
(fun
   x : {HO : F = G &
       transport
         (fun GO : C -> D =>
          forall s d : C,
          morphism C s d -> morphism D (GO s) (GO d))
         HO (morphism_of F) = morphism_of G} =>
 path_functor_uncurried_inv
   (path_functor_uncurried F G x)) == idmap hnf.
H: Funext
C, D: PreCategory
F, G: Functor C D
forall
x : {HO : F = G &
    transport
      (fun GO : C -> D =>
       forall s d : C,
       morphism C s d -> morphism D (GO s) (GO d)) HO
      (morphism_of F) = morphism_of G},
path_functor_uncurried_inv
  (path_functor_uncurried F G x) = x
      intros [? ?].
H: Funext
C, D: PreCategory
F, G: Functor C D
proj1: F = G
proj2: transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d))
  proj1 (morphism_of F) = 
morphism_of G
path_functor_uncurried_inv
  (path_functor_uncurried F G (proj1; proj2)) =
(proj1; proj2)
      apply path_sigma_uncurried.
H: Funext
C, D: PreCategory
F, G: Functor C D
proj1: F = G
proj2: transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d))
  proj1 (morphism_of F) = 
morphism_of G
{p
: (path_functor_uncurried_inv
     (path_functor_uncurried F G (proj1; proj2))).1 =
  (proj1; proj2).1 &
transport
  (fun HO : F = G =>
   transport
     (fun GO : C -> D =>
      forall s d : C,
      morphism C s d -> morphism D (GO s) (GO d)) HO
     (morphism_of F) = morphism_of G) p
  (path_functor_uncurried_inv
     (path_functor_uncurried F G (proj1; proj2))).2 =
(proj1; proj2).2}
      exists (path_functor_uncurried_fst _ _ _).
H: Funext
C, D: PreCategory
F, G: Functor C D
proj1: F = G
proj2: transport
  (fun GO : C -> D =>
   forall s d : C,
   morphism C s d -> morphism D (GO s) (GO d))
  proj1 (morphism_of F) = 
morphism_of G
transport
  (fun HO : F = G =>
   transport
     (fun GO : C -> D =>
      forall s d : C,
      morphism C s d -> morphism D (GO s) (GO d)) HO
     (morphism_of F) = morphism_of G)
  (path_functor_uncurried_fst F G proj2)
  (path_functor_uncurried_inv
     (path_functor_uncurried F G (proj1; proj2))).2 =
(proj1; proj2).2
      exact (center _).
  Defined.

  Definition equiv_path_functor_uncurried (F G : Functor C D)
  : path_functor'_T F G <~> F = G
    := Build_Equiv _ _ (@path_functor_uncurried F G) _.

  Local Open Scope function_scope.

  Definition path_path_functor_uncurried (F G : Functor C D) (p q : F = G)
  : ap object_of p = ap object_of q -> p = q.
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
ap object_of p = ap object_of q -> p = q
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
ap object_of p = ap object_of q -> p = q
    refine ((ap (@path_functor_uncurried F G)^-1)^-1 o _).
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
ap object_of p = ap object_of q ->
(path_functor_uncurried F G)^-1 p =
(path_functor_uncurried F G)^-1 q
    refine ((path_sigma_uncurried _ _ _) o _); simpl.
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
ap object_of p = ap object_of q ->
{p0 : ap object_of p = ap object_of q &
transport
  (fun HO : F = G =>
   transport
     (fun GO : C -> D =>
      forall s d : C,
      morphism C s d -> morphism D (GO s) (GO d)) HO
     (morphism_of F) = morphism_of G) p0
  ((transport_compose
      (fun GO : C -> D =>
       forall s d : C,
       morphism C s d -> morphism D (GO s) (GO d))
      object_of p (morphism_of F))^ @
   apD (morphism_of (D:=D)) p) =
(transport_compose
   (fun GO : C -> D =>
    forall s d : C,
    morphism C s d -> morphism D (GO s) (GO d))
   object_of q (morphism_of F))^ @
apD (morphism_of (D:=D)) q}
    refine (pr1^-1).
  Defined.

  Global Instance isequiv_path_path_functor_uncurried F G p q
  : IsEquiv (@path_path_functor_uncurried F G p q).
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
IsEquiv (path_path_functor_uncurried p q)
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
IsEquiv (path_path_functor_uncurried p q)
    unfold path_path_functor_uncurried.
H: Funext
C, D: PreCategory
F, G: Functor C D
p, q: F = G
IsEquiv
  (fun x : ap object_of p = ap object_of q =>
   (ap (path_functor_uncurried F G)^-1)^-1
     (path_sigma_uncurried
        (fun HO : F = G =>
         transport
           (fun GO : C -> D =>
            forall s d : C,
            morphism C s d -> morphism D (GO s) (GO d))
           HO (morphism_of F) = morphism_of G)
        ((path_functor_uncurried F G)^-1 p)
        ((path_functor_uncurried F G)^-1 q) (pr1^-1 x)))
    (** N.B. [exact _] is super-slow here.  Not sure why. *)
    repeat match goal with
             | [ |- IsEquiv (_ o _) ] => eapply @isequiv_compose
             | [ |- IsEquiv (_^-1) ] => eapply @isequiv_inverse
             | [ |- IsEquiv (path_sigma_uncurried _ _ _) ] => eapply @isequiv_path_sigma
             | _ => apply @isequiv_compose
           end.
  Defined.

  (** ** If the objects in [D] are n-truncated, then so is the type of functors [C → D] *)
  Global Instance trunc_functor `{IsTrunc n D} `{forall s d, IsTrunc n (morphism D s d)}
  : IsTrunc n (Functor C D).
H: Funext
C, D: PreCategory
n: trunc_index
IsTrunc0: IsTrunc n D
H0: forall s d : D, IsTrunc n (morphism D s d)
IsTrunc n (Functor C D)
  Proof.
H: Funext
C, D: PreCategory
n: trunc_index
IsTrunc0: IsTrunc n D
H0: forall s d : D, IsTrunc n (morphism D s d)
IsTrunc n (Functor C D)
    eapply istrunc_equiv_istrunc; [ exact equiv_sig_functor | ].
H: Funext
C, D: PreCategory
n: trunc_index
IsTrunc0: IsTrunc n D
H0: forall s d : D, IsTrunc n (morphism D s d)
IsTrunc n
  {OO : C -> D &
  {MO
  : forall s d : C,
    morphism C s d -> morphism D (OO s) (OO d) &
  {_
  : forall (s d d' : C) (m1 : morphism C s d)
    (m2 : morphism C d d'),
    MO s d' (m2 o m1)%morphism =
    (MO d d' m2 o MO s d m1)%morphism &
  forall x : C, MO x x 1 = 1}}}
    induction n;
    simpl; intros;
    typeclasses eauto.
  Qed.
End path_functor.

(** ** Tactic for proving equality of functors *)
Ltac path_functor :=
  repeat match goal with
           | _ => intro
           | _ => reflexivity
           | _ => apply path_functor_uncurried; simpl
           | _ => (exists idpath)
         end.

Global Arguments path_functor_uncurried : simpl never.

(** ** Tactic for pushing [ap object_of] through other [ap]s.

    This allows lemmas like [path_functor_uncurried_fst] to apply more
    easily. *)
Ltac push_ap_object_of' :=
  idtac;
  match goal with
    | [ |- context[ap object_of (ap ?f ?p)] ]
      => rewrite <- (ap_compose' f object_of p); simpl
    | [ |- context G[ap (fun F' x => object_of F' (@?f x)) ?p] ]
      => let P := context_to_lambda G in
         refine (transport P (ap_compose' object_of (fun F' x => F' (f x)) p)^ _)
    | [ |- context G[ap (fun F' x => ?f (object_of F' x)) ?p] ]
      => let P := context_to_lambda G in
         refine (transport P (ap_compose' object_of (fun F' x => f (F' x)) p)^ _)
  end.
Ltac push_ap_object_of := repeat push_ap_object_of'.