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_reducible]

instance Born.instCoeSortType : CoeSort Born (Type u_1)

Equations

• Born.instCoeSortType = { coe := Born.carrier }

@[instance_reducible]

instance Born.instInhabited : Inhabited Born

Equations

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

@[instance_reducible]

instance Born.instLargeCategory : CategoryTheory.LargeCategory Born

Equations

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

@[instance_reducible]

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

Equations

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

def Born.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints Born.of X as ↧X.

Equations

• Born.delabOf = CategoryTheory.delabOf