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