Library HoTT.Categories.CategoryOfSections

Category of sections of a functor

Require CategoryOfSections.Core.

Include CategoryOfSections.Core.