Library HoTT.Categories.Functor.Paths

Classification of path spaces of functors

Require Import Category.Core Functor.Core.
Require Import HoTT.Basics HoTT.Types HoTT.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

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 : ∀ s d, morphism C s d → morphism D (OO s) (OO d)
      | { FCO : ∀ 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
        | ∀ 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.
  Proof.
    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 ⇒ ∀ 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.
  Proof.
    intros [? ?].
    destruct F, G; simpl in ×.
    path_induction; simpl.
    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.
  Proof.
    destruct F, G; simpl in ×.
    path_induction_hammer.
  Qed.

Said proof respects idpath

  Lemma path_functor_uncurried_idpath F
  : @path_functor_uncurried F F (idpath; idpath) = idpath.
  Proof.
    destruct F; simpl in ×.
    rewrite !(contr idpath).
    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 ⇒ ∀ 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 ∀ in place of equality of functions

  Definition path_functor_pointwise (F G : Functor C D)
        (HO : object_of F == object_of G)
        (HM : ∀ s d m,
                transport (fun GO ⇒ ∀ 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.
  Proof.
    refine (path_functor F G (path_forall _ _ HO) _).
    repeat (apply path_forall; intro); apply HM.
  Defined.

Classify equality of functors up to equivalence

  #[export] Instance isequiv_path_functor_uncurried (F G : Functor C D)
  : IsEquiv (@path_functor_uncurried F G).
  Proof.
    apply (isequiv_adjointify (@path_functor_uncurried F G)
                              (@path_functor_uncurried_inv F G)).
    - hnf.
      intros [].
      apply path_functor_uncurried_idpath.
    - hnf.
      intros [? ?].
      apply path_sigma_uncurried.
      ∃ (path_functor_uncurried_fst _ _ _).
      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.
  Proof.
    refine ((ap (@path_functor_uncurried F G)^-1)^-1 o _).
    refine ((path_sigma_uncurried _ _ _) o _); simpl.
    exact (pr1^-1).
  Defined.

  #[export] Instance isequiv_path_path_functor_uncurried F G p q
  : IsEquiv (@path_path_functor_uncurried F G p q).
  Proof.
    unfold path_path_functor_uncurried.
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

  #[export] Instance trunc_functor `{IsTrunc n D} `{∀ s d, IsTrunc n (morphism D s d)}
  : IsTrunc n (Functor C D).
  Proof.
    eapply istrunc_equiv_istrunc; [ exact equiv_sig_functor | ].
    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
           | _ ⇒ (∃ idpath)
         end.

Global Arguments path_functor_uncurried : simpl never.

Tactic for pushing ap object_of through other aps.

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'.