(** * Category of sections *)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 Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. 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 }.H: Funext
C, D: PreCategory
R: Functor C D{section_of_functor_morphism : Functor D C & R o section_of_functor_morphism = 1} <~> SectionOfFunctorissig. Defined. Local Open Scope natural_transformation_scope. (** ** Definition of category of sections of a functor *)H: Funext
C, D: PreCategory
R: Functor C D{section_of_functor_morphism : Functor D C & R o section_of_functor_morphism = 1} <~> SectionOfFunctorH: Funext
C, D: PreCategory
R: Functor C DPreCategoryrefine (@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.H: Funext
C, D: PreCategory
R: Functor C DPreCategoryH: Funext
C: PreCategory
IsStrictCategory0: IsStrictCategory C
D: PreCategory
IsStrictCategory1: IsStrictCategory D
F: Functor C DIsStrictCategory (category_of_sections F)H: Funext
C: PreCategory
IsStrictCategory0: IsStrictCategory C
D: PreCategory
IsStrictCategory1: IsStrictCategory D
F: Functor C DIsStrictCategory (category_of_sections F)typeclasses eauto. Qed.H: Funext
C: PreCategory
IsStrictCategory0: IsStrictCategory C
D: PreCategory
IsStrictCategory1: IsStrictCategory D
F: Functor C DIsHSet {section_of_functor_morphism : Functor D C & (fun x : D => (F _0 (section_of_functor_morphism _0 x))%object) = 1}