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]

slide 5 - not clear in which case is "in this case" C is called a sub-type of A. I would kind of understand that A is subtype of B, if there is a monomorphism A→B.

slide 9 still uses ⊥

slide 14 - as a side note, equalizer universal property is not mentioned. How do they work without this in type theory? ok, point 2 is the universal property

slide 15: ∈ is defined earlier as A×Ω^A→Ω, yet here it seems to have a incompatible type: Ω×Ω^A→Ω Was it meant to be Ω×Ω^Ω→Ω?

Hmmm... even that looks wrong. From slide 14 it seems Eq(p₁, ∈) must be of type X→Ω×Ω^Ω for some X.

slides 16 onwards look incomplete (or my browser didn't load some pictures)

[juan-gandhi.livejournal.com]

Thanks a lot!!!
Will think about Slide 15... maybe a problem...

I wonder if it works now with the pictures on slide 16 etc

[sassa-nf.livejournal.com]

Now I do see the pictures. (but this is a different computer)

slide 11 - thank you for the pullback diagram! It really clarified it for me. (even though three more arrows are missing, and the definition of the pullback, too)

slide 16 - Disjunction diagram is a bit unexpected - U was not introduced.

slide 15: I do get the idea (p₁ and ∈ interpret A×A^A (can't use A, because ∈ codomain is Ω) Ω×Ω^Ω in an incompatible manner, so there is no Equalizer for this pair, so the type of Equalizers for this pair is empty), but the types are still not right (and I am not sure what the diagram shows).

[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.

[sassa-nf.livejournal.com]

slide 17 - you always used T for Unit, but here one diagram uses 1

Also, a typing problem similar to slide 15: id and ^ cannot be Ω→Ω at the same time. ^ must be Ω×Ω→Ω, but id cannot be that.

[juan-gandhi.livejournal.com]

Thanks a lot! Now I've made tons of changes.
Probably it's more readable now.
Maybe I'll give a talk on it at our BACAT meeting this month.

I feel like it's a little bit revolutionary. Just figured, eh, a monomorphism is a subtype.