Paths.v

(** * Classify the path space of natural transformations *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Equivalences HoTT.Types Trunc Basics.Tactics.

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

Local Open Scope morphism_scope.
Local Open Scope natural_transformation_scope.

Section path_natural_transformation.
  Context `{Funext}.

  Variables C D : PreCategory.
  Variables F G : Functor C D.



  (** ** Equivalence between record and sigma versions of natural transformation *)
  Lemma equiv_sig_natural_transformation
  : { CO : forall x, morphism D (F x) (G x)
    | forall s d (m : morphism C s d),
        CO d o F _1 m = G _1 m o CO s }
      <~> NaturalTransformation F G.H: Funext
C, D: PreCategory
F, G: Functor C D
{CO
: forall x : C,
  morphism D (F _0 x)%object (G _0 x)%object &
forall (s d : C) (m : morphism C s d),
CO d o F _1 m = G _1 m o CO s} <~>
NaturalTransformation F G
  Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
{CO
: forall x : C,
  morphism D (F _0 x)%object (G _0 x)%object &
forall (s d : C) (m : morphism C s d),
CO d o F _1 m = G _1 m o CO s} <~>
NaturalTransformation F G
    let build := constr:(@Build_NaturalTransformation _ _ F G) in
    let pr1 := constr:(@components_of _ _ F G) in
    let pr2 := constr:(@commutes _ _ F G) in
    apply (equiv_adjointify (fun u => build u.1 u.2)
                            (fun v => (pr1 v; pr2 v)));
      hnf;
      [ intros []; intros; simpl; expand; f_ap; exact (center _)
      | intros; apply eta_sigma ].
  Defined.

  (** ** The type of natural transformations is an hSet *)
  Global Instance trunc_natural_transformation
  : IsHSet (NaturalTransformation F G).H: Funext
C, D: PreCategory
F, G: Functor C D
IsHSet (NaturalTransformation F G)
  Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
IsHSet (NaturalTransformation F G)
    eapply istrunc_equiv_istrunc; [ exact equiv_sig_natural_transformation | ].H: Funext
C, D: PreCategory
F, G: Functor C D
IsHSet
  {CO
  : forall x : C,
    morphism D (F _0 x)%object (G _0 x)%object &
  forall (s d : C) (m : morphism C s d),
  CO d o F _1 m = G _1 m o CO s}
    typeclasses eauto.
  Qed.

  Section path.
    Variables T U : NaturalTransformation F G.

    (** ** Equality of natural transformations is implied by equality of components *)
    Lemma path'_natural_transformation
    : components_of T = components_of U
      -> T = U.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
T = U -> T = U
    Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
T = U -> T = U
      intros.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
X: T = U
T = U
      destruct T, U; simpl in *.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
components_of: forall c : C,
morphism D (F _0 c)%object
  (G _0 c)%object
commutes: forall (s d : C) (m : morphism C s d),
components_of d o F _1 m =
G _1 m o components_of s
commutes_sym: forall (s d : C) (m : morphism C s d),
G _1 m o components_of s =
components_of d o F _1 m
components_of0: forall c : C,
morphism D (F _0 c)%object
  (G _0 c)%object
commutes0: forall (s d : C) (m : morphism C s d),
components_of0 d o F _1 m =
G _1 m o components_of0 s
commutes_sym0: forall (s d : C) (m : morphism C s d),
G _1 m o components_of0 s =
components_of0 d o F _1 m
X: components_of = components_of0
{|
  components_of := components_of;
  commutes := commutes;
  commutes_sym := commutes_sym
|} =
{|
  components_of := components_of0;
  commutes := commutes0;
  commutes_sym := commutes_sym0
|}
      path_induction.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
components_of: forall c : C,
morphism D (F _0 c)%object
  (G _0 c)%object
commutes: forall (s d : C) (m : morphism C s d),
components_of d o F _1 m =
G _1 m o components_of s
commutes_sym: forall (s d : C) (m : morphism C s d),
G _1 m o components_of s =
components_of d o F _1 m
commutes0: forall (s d : C) (m : morphism C s d),
components_of d o F _1 m =
G _1 m o components_of s
commutes_sym0: forall (s d : C) (m : morphism C s d),
G _1 m o components_of s =
components_of d o F _1 m
{|
  components_of := components_of;
  commutes := commutes;
  commutes_sym := commutes_sym
|} =
{|
  components_of := components_of;
  commutes := commutes0;
  commutes_sym := commutes_sym0
|}
      f_ap;
        refine (center _).
    Qed.

    Lemma path_natural_transformation
    : components_of T == components_of U
      -> T = U.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
T == U -> T = U
    Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
T == U -> T = U
      intros.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
X: T == U
T = U
      apply path'_natural_transformation.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
X: T == U
T = U
      apply path_forall; assumption.
    Qed.

    Let path_inv
    : T = U -> components_of T == components_of U
      := (fun H _ => match H with idpath => idpath end).

    Lemma eisretr_path_natural_transformation
    : path_inv o path_natural_transformation == idmap.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
path_inv o path_natural_transformation == idmap
    Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
path_inv o path_natural_transformation == idmap
      repeat intro.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
x: T == U
path_inv (path_natural_transformation x) = x
      refine (center _).
    Qed.

    Lemma eissect_path_natural_transformation
    : path_natural_transformation o path_inv == idmap.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
path_natural_transformation o path_inv == idmap
    Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
path_natural_transformation o path_inv == idmap
      repeat intro.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
x: T = U
path_natural_transformation (path_inv x) = x
      refine (center _).
    Qed.

    Lemma eisadj_path_natural_transformation
    : forall x,
        @eisretr_path_natural_transformation (path_inv x)
        = ap path_inv (eissect_path_natural_transformation x).H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
forall x : T = U,
eisretr_path_natural_transformation (path_inv x) =
ap path_inv (eissect_path_natural_transformation x)
    Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
forall x : T = U,
eisretr_path_natural_transformation (path_inv x) =
ap path_inv (eissect_path_natural_transformation x)
      repeat intro.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
x: T = U
eisretr_path_natural_transformation (path_inv x) =
ap path_inv (eissect_path_natural_transformation x)
      refine (center _).
    Qed.

    (** ** Equality of natural transformations is equivalent to equality of components *)
    Lemma equiv_path_natural_transformation
    : T = U <~> (components_of T == components_of U).H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
T = U <~> T == U
    Proof.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
T = U <~> T == U
      econstructor.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
IsEquiv ?equiv_fun econstructor.H: Funext
C, D: PreCategory
F, G: Functor C D
T, U: NaturalTransformation F G
path_inv:= fun (H : T = U) (x : C) =>
match H in (_ = n) return (T x = n x) with
| 1%path => 1%path
end: T = U -> T == U
forall x : T = U,
?eisretr (?equiv_fun x) = ap ?equiv_fun (?eissect x) exact eisadj_path_natural_transformation.
    Defined.
  End path.
End path_natural_transformation.

(** ** Tactic for proving equality of natural transformations *)
Ltac path_natural_transformation :=
  repeat match goal with
           | _ => intro
           | _ => apply path_natural_transformation; simpl
         end.