Blog Archive 2015 Equivalence of Types Mar 30 2015 Homotopy Type Theory Mar 30 2015 Exercises for Midterm Feb 09 2015 Logic From Types Feb 02 2015 Fin Type Family Jan 30 2015 Rooted Trees and General Induction Jan 25 2015 Constructing Dependent Functions Jan 23 2015 Dependent Function Types: Sections of a Bundle Jan 22 2015 Recursion Functions and Inductive Types Jan 21 2015 A Program : Lattice Points in a Circle Jan 20 2015 Products and Sums Jan 16 2015 Fun With Lists Jan 13 2015 Inductive Types: Natural Numbers, Lists Jan 08 2015 Notation for Universes Jan 07 2015 Foundations: Mathematical Objects, Types, Rules Jan 06 2015 Types and First-order Languages Jan 04 2015 2014 Sets and Types Dec 29 2014 Language, Logic, Types Dec 17 2014 Welcome to the Course: Logic, Types, Spaces Dec 12 2014