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.instCoeSortType : CoeSort Born (Type u_1)

Equations

• Born.instCoeSortType = CategoryTheory.Bundled.coeSort

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

Equations

• X.instBornologyα = 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.instInhabited : Inhabited Born

Equations

• Born.instInhabited = { default := Born.of PUnit.{?u.3 + 1} }

instance Born.instBundledHomBornologyLocallyBoundedMap : CategoryTheory.BundledHom LocallyBoundedMap

Equations

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

instance Born.instLargeCategory : CategoryTheory.LargeCategory Born

Equations

• Born.instLargeCategory = CategoryTheory.BundledHom.category LocallyBoundedMap

instance Born.instConcreteCategory : CategoryTheory.ConcreteCategory Born

Equations

• Born.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory LocallyBoundedMap