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
ωCPO- an instance of
categoryandconcrete_category
- an instance of
The category of types with a omega complete partial order.
@[instance]
Equations
- ωCPO.category_theory.bundled_hom = {to_fun := omega_complete_partial_order.continuous_hom.to_fun, id := omega_complete_partial_order.continuous_hom.id, comp := omega_complete_partial_order.continuous_hom.comp, hom_ext := omega_complete_partial_order.continuous_hom.coe_inj, id_to_fun := ωCPO.category_theory.bundled_hom._proof_1, comp_to_fun := ωCPO.category_theory.bundled_hom._proof_2}
Construct a bundled ωCPO from the underlying type and typeclass.
Equations
@[instance]
Equations
@[instance]