(** * Category of sections *)
Require Import Functor.Core NaturalTransformation.Core.
Require Import Category.Strict.
Require Import Functor.Identity NaturalTransformation.Identity.
Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core.
Require Import Functor.Paths.
Require Import HoTT.Basics HoTT.Types.

Set Implicit Arguments.
Generalizable All Variables.
Local Open Scope functor_scope.

Section FunctorSectionCategory.
  Context `{Funext}.

  Variables C D : PreCategory.
  Variable R : Functor C D.

  (** There is a category [Sect(R)] of sections of [R]. *)

  (** ** Section of a functor *)
  Record SectionOfFunctor :=
    {
      section_of_functor_morphism :> Functor D C;
      section_of_functor_issect : R o section_of_functor_morphism = 1
    }.

  Local Notation section_of_functor_sig :=
    { section_of_functor_morphism : Functor D C
    | R o section_of_functor_morphism = 1 }.

  Lemma section_of_functor_sig'
  : section_of_functor_sig <~> SectionOfFunctor.
H: Funext
C, D: PreCategory
R: Functor C D
{section_of_functor_morphism0 : Functor D C &
R o section_of_functor_morphism0 = 1} <~> SectionOfFunctor
  Proof.
H: Funext
C, D: PreCategory
R: Functor C D
{section_of_functor_morphism0 : Functor D C &
R o section_of_functor_morphism0 = 1} <~> SectionOfFunctor
    issig.
  Defined.

  Local Open Scope natural_transformation_scope.

  (** ** Definition of category of sections of a functor *)
  Definition category_of_sections : PreCategory.
H: Funext
C, D: PreCategory
R: Functor C D
PreCategory
  Proof.
H: Funext
C, D: PreCategory
R: Functor C D
PreCategory
    refine (@Build_PreCategory
              SectionOfFunctor
              (fun F G => NaturalTransformation F G)
              (fun F => 1)
              (fun _ _ _ T U => T o U)
              _
              _
              _
              _);
    abstract (path_natural_transformation; auto with morphism).
  Defined.
End FunctorSectionCategory.

Instance isstrict_category_of_sections `{Funext}
      `{IsStrictCategory C, IsStrictCategory D}
      (F : Functor C D)
: IsStrictCategory (category_of_sections F) | 20.
H: Funext
C: PreCategory
IsStrictCategory0: IsStrictCategory C
D: PreCategory
IsStrictCategory1: IsStrictCategory D
F: Functor C D
IsStrictCategory (category_of_sections F)
Proof.
H: Funext
C: PreCategory
IsStrictCategory0: IsStrictCategory C
D: PreCategory
IsStrictCategory1: IsStrictCategory D
F: Functor C D
IsStrictCategory (category_of_sections F)
  eapply istrunc_isequiv_istrunc; [ | apply section_of_functor_sig' ].
H: Funext
C: PreCategory
IsStrictCategory0: IsStrictCategory C
D: PreCategory
IsStrictCategory1: IsStrictCategory D
F: Functor C D
IsHSet
  {section_of_functor_morphism0 : Functor D C &
  (fun x : D => (F _0 (section_of_functor_morphism0 _0 x))%object) = 1}
  typeclasses eauto.
Qed.