The category of bornologies

This defines Born, the category of bornologies.

structure Born : Type (u_1 + 1)

The category of bornologies.

• carrier : Type u_1

  The underlying bornology.

• str : Bornology self.carrier

instance Born.instCoeSortType : CoeSort Born (Type u_1)

Equations

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

@[reducible, inline]

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

Construct a bundled Born from a Bornology.

Equations

• Born.of α = Born.mk α

instance Born.instInhabited : Inhabited Born

Equations

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

instance Born.instLargeCategory : CategoryTheory.LargeCategory Born

Equations

• Born.instLargeCategory = CategoryTheory.Category.mk @Born.instLargeCategory.proof_1 @Born.instLargeCategory.proof_2 @Born.instLargeCategory.proof_3

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.