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.Data.PFunctor.IndRec.Basic public import Geb.Mathlib.Data.PFunctor.IndRec.Hom public import Geb.Mathlib.Data.PFunctor.IndRec.Functor public import Geb.Mathlib.Data.PFunctor.IndRec.Naturality public import Geb.Mathlib.Data.PFunctor.IndRec.Category public import Geb.Mathlib.Data.PFunctor.IndRec.Universes public import Geb.Mathlib.Data.PFunctor.IndRec.Container public import Geb.Mathlib.Data.PFunctor.IndRec.Slice public import Geb.Mathlib.Data.PFunctor.IndRec.W public import Geb.Mathlib.Data.PFunctor.IndRec.Indexed public import Geb.Mathlib.Data.PFunctor.IndRec.Language public import Geb.Mathlib.Data.PFunctor.IndRec.BoveCapretta

IndRec — index