The category of bornologies

This defines Born, the category of bornologies.

def Born : Type (u_1 + 1)

The category of bornologies.

Equations

• Born = CategoryTheory.Bundled Bornology

instance Born.instCoeSortBornType : CoeSort Born (Type u_1)

Equations

• Born.instCoeSortBornType = CategoryTheory.Bundled.coeSort

instance Born.instBornologyα (X : Born) : Bornology ↑X

Equations

• Born.instBornologyα X = X.str

def Born.of (α : Type u_1) [Bornology α] : Born

Construct a bundled Born from a Bornology.

Equations

• Born.of α = CategoryTheory.Bundled.of α

instance Born.instInhabitedBorn : Inhabited Born

Equations

• Born.instInhabitedBorn = { default := Born.of PUnit.{u_1 + 1} }

instance Born.instBundledHomTypeBornologyLocallyBoundedMap : CategoryTheory.BundledHom LocallyBoundedMap

Equations

• One or more equations did not get rendered due to their size.

instance Born.instLargeCategoryBorn : CategoryTheory.LargeCategory Born

Equations

• Born.instLargeCategoryBorn = CategoryTheory.BundledHom.category LocallyBoundedMap

instance Born.instConcreteCategoryBornInstLargeCategoryBorn : CategoryTheory.ConcreteCategory Born

Equations

• Born.instConcreteCategoryBornInstLargeCategoryBorn = CategoryTheory.BundledHom.concreteCategory LocallyBoundedMap