The category of bornologies

This defines Born, the category of bornologies.

structure Born : Type (u_1 + 1)

The category of bornologies.

• of :: (
• carrier : Type u_1

  The underlying bornology.

• str : Bornology self.carrier
• )

instance Born.instCoeSortType : CoeSort Born (Type u_1)

instance Born.instInhabited : Inhabited Born

instance Born.instLargeCategory : CategoryTheory.LargeCategory Born

instance Born.instConcreteCategoryLocallyBoundedMapCarrier : CategoryTheory.ConcreteCategory Born fun (x1 x2 : Born) => LocallyBoundedMap x1.carrier x2.carrier