What is the universal property of dependent product / dependent sum? (I want to see a diagrams) They are must be different from usual ones, aren't they?
(i'm trying to understand category theory after I learned homotopy type theory. Is there a possibility to learn a category theory without learning some mathematical foundations like ZFC or HoTT?)
Short answer: dependent sum, dependent product. It's certainly not necessary to learn a foundation in order to learn category theory; there are now several good books on category theory out there, like Awodey's and Leinster's.