# Category of types with an omega complete partial order #

In this file, we bundle the class OmegaCompletePartialOrder into a concrete category and prove that continuous functions also form an OmegaCompletePartialOrder.

## Main definitions #

• ωCPO
• an instance of Category and ConcreteCategory
def ωCPO :
Type (u + 1)

The category of types with an omega complete partial order.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
def ωCPO.of (α : Type u_1) :

Construct a bundled ωCPO from the underlying type and typeclass.

Equations
Instances For
@[simp]
theorem ωCPO.coe_of (α : Type u_1) :
() = α
Equations
Equations
• α.instOmegaCompletePartialOrderα = α.str
def ωCPO.HasProducts.product {J : Type v} (f : JωCPO) :

The pi-type gives a cone for a product.

Equations
Instances For
def ωCPO.HasProducts.isProduct (J : Type v) (f : JωCPO) :

The pi-type is a limit cone for the product.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance ωCPO.HasProducts.instHasProduct (J : Type v) (f : JωCPO) :
Equations
• =
instance ωCPO.omegaCompletePartialOrderEqualizer {α : Type u_1} {β : Type u_2} (f : α →𝒄 β) (g : α →𝒄 β) :
OmegaCompletePartialOrder { a : α // f a = g a }
Equations
def ωCPO.HasEqualizers.equalizerι {α : Type u_1} {β : Type u_2} (f : α →𝒄 β) (g : α →𝒄 β) :
{ a : α // f a = g a } →𝒄 α

The equalizer inclusion function as a ContinuousHom.

Equations
Instances For
def ωCPO.HasEqualizers.equalizer {X : ωCPO} {Y : ωCPO} (f : X Y) (g : X Y) :

A construction of the equalizer fork.

Equations
Instances For
def ωCPO.HasEqualizers.isEqualizer {X : ωCPO} {Y : ωCPO} (f : X Y) (g : X Y) :

The equalizer fork is a limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
instance ωCPO.instHasLimitWalkingParallelPairParallelPair {X : ωCPO} {Y : ωCPO} (f : X Y) (g : X Y) :
Equations
• =
Equations
Equations