A Equalizer is a unique pair (object,arrow) with universal property. So when you are talking about Equalizer(p1,∈), need to consider the object from which the arrow goes into Ω×ΩΩ. Since Ω has two instances, all non-empty types will have at least two arrows that equalize p1 and ∈ (and maybe even no universal property).
The only object from which there is a unique arrow, is ⊥, because there is only one arrow from that type to any object. But I don't know how to demonstrate the universal property. Is there such a property? A co-cone definitely exists, but that doesn't make a equalizer.
As to the diagram - the equalizer of course can be drawn as a pullback, but you'd need those three arrows missing from the pullback diagram on the subtyping slide.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2014-09-10 04:36 pm (UTC)A Equalizer is a unique pair (object,arrow) with universal property. So when you are talking about Equalizer(p1,∈), need to consider the object from which the arrow goes into Ω×ΩΩ. Since Ω has two instances, all non-empty types will have at least two arrows that equalize p1 and ∈ (and maybe even no universal property).
The only object from which there is a unique arrow, is ⊥, because there is only one arrow from that type to any object. But I don't know how to demonstrate the universal property. Is there such a property? A co-cone definitely exists, but that doesn't make a equalizer.
As to the diagram - the equalizer of course can be drawn as a pullback, but you'd need those three arrows missing from the pullback diagram on the subtyping slide.