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)