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]

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