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.FinCat.Basic public import Geb.Mathlib.CategoryTheory.FinCat.Bicategory public import Geb.Mathlib.CategoryTheory.FinCat.Category public import Geb.Mathlib.CategoryTheory.FinCat.Decidable public import Geb.Mathlib.CategoryTheory.FinCat.FinCategory public import Geb.Mathlib.CategoryTheory.FinCat.Hom public import Geb.Mathlib.CategoryTheory.FinCat.Hom2 public import Geb.Mathlib.CategoryTheory.FinCat.Repr

FinCat — index