building types from scratch

[juan_gandhi]

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

(toposes lurking behind the scene)

Comments

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