building types from scratch

[juan_gandhi]

https://docs.google.com/presentation/d/1HVrs-uhe2N9jQopA5eE41PIFMOzGry69b2CrUArOnsg/edit?usp=sharing

(toposes lurking behind the scene)

Comments

[sassa-nf.livejournal.com]

Here it goes.

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.