Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Geb.Mathlib.CategoryTheory.DiscreteFibration.Basic public import Geb.Mathlib.CategoryTheory.DiscreteFibration.Elements public import Geb.Mathlib.CategoryTheory.DiscreteFibration.FiberPresheaf public import Geb.Mathlib.CategoryTheory.DiscreteFibration.Packaged public import Geb.Mathlib.CategoryTheory.DiscreteFibration.Pullback

Discrete fibrations — index