mathlib documentation

order.category.omega_complete_partial_order

Category of types with a omega complete partial order

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

Main definitions

def ωCPO  :
Type (u+1)

The category of types with a omega complete partial order.

Equations
def ωCPO.of (α : Type u_1) [omega_complete_partial_order α] :

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

Equations
def ωCPO.has_products.product {J : Type v} (f : J → ωCPO) :

The pi-type gives a cone for a product.

Equations

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

Equations
def ωCPO.has_equalizers.equalizer_ι {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) :
{a // f a = g a} →𝒄 α

The equalizer inclusion function as a continuous_hom.

Equations