Abstract:
Dependent types are a wonderful way to construct correct functional programming and specify interfaces as Edwin has shown in his nice book on type driven development using a welsh dragon. But shall we go further in the esoteric world of homotopy type theory? I will try to motivate this and I am looking forward to some discussions with people who have a more pragmatic attitude to dependent types.