Abstract: (Note the unusual day, time, and room.) I will talk about homotopy type theoretic proofs of a well known topological fact that the fundamental group of the circle is the set of integers. There are two closely related proofs. The homotopy-theoretic proof follows a similar reasoning used in the classical proof in topology, whereas the encode-decode proof is more type theoretic.