diff --git a/Gardner1997Type-theoretic.pdf b/Gardner1997Type-theoretic.pdf new file mode 100644 index 0000000000000000000000000000000000000000..cc8d5e9540b542c592c2b392fd04521e8b841f2f Binary files /dev/null and b/Gardner1997Type-theoretic.pdf differ