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
andConcreteCategory
- an instance of
Construct a bundled ωCPO from the underlying type and typeclass.
Instances For
The pi-type gives a cone for a product.
Instances For
The pi-type is a limit cone for the product.
Instances For
instance
ωCPO.omegaCompletePartialOrderEqualizer
{α : Type u_1}
{β : Type u_2}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
(g : α →𝒄 β)
:
OmegaCompletePartialOrder { a // ↑f a = ↑g a }
def
ωCPO.HasEqualizers.equalizerι
{α : Type u_1}
{β : Type u_2}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
(g : α →𝒄 β)
:
The equalizer inclusion function as a ContinuousHom
.
Instances For
A construction of the equalizer fork.
Instances For
The equalizer fork is a limit.
Instances For
instance
ωCPO.instHasLimitWalkingParallelPairWalkingParallelPairHomCategoryωCPOInstωCPOLargeCategoryParallelPair
{X : ωCPO}
{Y : ωCPO}
(f : X ⟶ Y)
(g : X ⟶ Y)
: