This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
371
stars
22
forks
source link
Expand App. B.1 to discuss principles compatible with decidable equality and program extraction #173
See title. Mention the solution to Voevodsky's conjecture on homotopy canonicity, cubical type theories, etc., as well as the still-open question of constructive status of propositional resizing.
See title. Mention the solution to Voevodsky's conjecture on homotopy canonicity, cubical type theories, etc., as well as the still-open question of constructive status of propositional resizing.